AI4Math

4core

10adjacent

76downweighted

0warnings

Today's Scan

Start with SkillEvoLean: Mutation-enhanced skill evolution for Lean provers, then Second-Order Problem Solving for Recursive Self-Improvement in Formal Verification. 14 fresh useful item(s) are inside the 21-day content window.

Source Mix

arXiv14

Best Use

Open only the first lane during a busy morning. Older recurring seeds are kept below the daily scan instead of competing with fresh items.

Start Here

The top few items most likely to matter for formal proof agents or Lean-facing AI4Math work.

core score 12.3 2026-10-01 arXiv

SkillEvoLean: Mutation-enhanced skill evolution for Lean provers

Kuo Zhou, ZiXion Yang, Lu Zhang

Skill evolution offers a promising way to improve large language model agents without updating their parameters, but its use in formal theorem proving remains underexplored. Existing methods mainly target natural-language reasoning, improving skills by anal...

Why it matters Most relevant if you are tracking proof-search loops that use verifier feedback instead of treating Lean as a binary oracle.

Skim cue Skim the abstract first; open the paper only if the method touches proof agents or formal verification.

Read if Read if you have 5 minutes and want a direct AI4Math signal.

AI math reasoningLean proof agentsverifier feedback

Open PDF Semantic Scholar

core score 9.5 2026-10-05 arXiv

Second-Order Problem Solving for Recursive Self-Improvement in Formal Verification

Yuxuan Jiang, Aditya Vempaty, Ashish Jagmohan

Recursive self-improvement (RSI) enables agents to iteratively optimize their workflows via execution feedback. However, standard RSI typically operates as a first-order optimizer: it repeatedly patches surface-level parameters in response to immediate fail...

Why it matters Most relevant if you are tracking proof-search loops that use verifier feedback instead of treating Lean as a binary oracle.

Skim cue Skim the search loop: proposal source, verifier call, retry strategy, and stopping rule.

Read if Read if you have 5 minutes and want a direct AI4Math signal.

Lean proof agentsverifier feedback

Open PDF Semantic Scholar

core score 6.5 2026-10-02 arXiv

Solving VeriContest with a Lean-Backed Rust Verifier

Traian Serbanuta, Jun Xu, Andrei Stefanescu et al.

VeriContest is a benchmark of 1007 competitive-programming problems in Rust, each with a Verus specification, a judge-accepted solution, and a Verus proof. Its authors report that proof generation is the bottleneck for frontier models: given the specificati...

Why it matters Most relevant if you are tracking proof-search loops that use verifier feedback instead of treating Lean as a binary oracle.

Skim cue Skim the task definition, metric, and whether the benchmark has Lean-checkable artifacts.

Read if Read if you have 5 minutes and want a direct AI4Math signal.

Lean proof agentsverifier feedback

Open PDF Semantic Scholar

Worth Opening

Good candidates after the first three. These are plausible paper-tab opens, not a mandatory reading list.

core score 6.3 2026-10-04 arXiv

AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness

Prithwish Jana, Viet Bach Hoang, Logan Luna et al.

Proof auto-formalization translates natural-language (NL) theorems and proofs into a formal language (FL) such as Lean, enabling mechanical verification. Despite rapid progress, research-level proofs often depend on concepts missing from leading proof assis...

Why it matters Most relevant if you are tracking proof-search loops that use verifier feedback instead of treating Lean as a binary oracle.

Skim cue Skim the search loop: proposal source, verifier call, retry strategy, and stopping rule.

Read if Read if you have 5 minutes and want a direct AI4Math signal.

RL or distillationtool-use agentsverifier feedback

Open PDF Semantic Scholar

adjacent score 4.9 2026-10-05 arXiv

One Extra Dimension Suffices for the Complete-Graph Squared-Stress

Lilin Yan, Hongwei Zhao

Let all pairwise distances of an arbitrary configuration of points in $\mathbb{R}^{\ell}$ be known exactly. We prove that every second-order stationary point of the complete-graph squared-stress objective over configurations in $\mathbb{R}^{k}$ has zero res...

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

AI math reasoningLean proof agents

Open PDF Semantic Scholar

adjacent score 4.9 2026-10-01 arXiv

Fewer Tokens, Better Action: GPT-6 Astra Robot Agents with 14% Higher Success Rate but 65% Fewer Tokens

Ruiyang Si, Jianxin Bi, Shunyu Yang et al.

Vision language model (VLM) agents can control robots through visual feedback and action primitives, but repeated model invocations and redundant observations incur substantial token overhead. We introduce PyRUA-Lean, an interactive code-execution framework...

Why it matters Most relevant if you are tracking proof-search loops that use verifier feedback instead of treating Lean as a binary oracle.

Skim cue Skim the abstract first; open the paper only if the method touches proof agents or formal verification.

Read if Save for later unless the title matches your current proof-agent work.

tool-use agentsverifier feedback

Open PDF Semantic Scholar

adjacent score 4.9 2026-10-01 arXiv

Borcea's 2-variance conjecture

Teng Zhang

In this paper, we prove Borcea's 2-variance conjecture. The Lean 4 formalization of the main results are also provided.

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

AI math reasoningLean proof agents

Open PDF Semantic Scholar

adjacent score 4.9 2026-10-01 arXiv

Baernstein's quasi-norm monotonicity conjecture for polynomials with unimodular zero

Teng Zhang

Let $m$ denote the normalized Haar measure on the unit circle $\mathbb{T}$. For $0<r<\infty$, define $\lVert f\rVert_{r}:=\left(\int_{\mathbb{T}}|f|^{r}\,\mathrm{d} m\right)^{1/r}$, with $\lVert f\rVert_{0}$ and $\lVert f\rVert_{\infty}$ interpreted as the...

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

AI math reasoningLean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-10-04 arXiv

A Dichotomy for Planar Graph Homomorphisms with Nonnegative Weights

Chenghua Liu, Boning Meng

We prove a complete complexity dichotomy for planar graph homomorphism counting with any fixed symmetric nonnegative matrix of arbitrary finite order, giving an explicit criterion for tractability. We also characterize exactly which fixed positive vertex we...

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-10-03 arXiv

Symbolic Search Is Not Exhausted: Persistent Proof-Space Exploration in Lean4

Ruoran Xu

Formal theorem proving increasingly combines learned semantic guidance with verified symbolic execution. The quality of the symbolic search substrate therefore determines how much useful mathematical structure can be accumulated, reused, and exposed under a...

Why it matters Direct Lean signal: likely relevant to the formalization or theorem-proving environment around AI4Math agents.

Skim cue Skim the search loop: proposal source, verifier call, retry strategy, and stopping rule.

Read if Save for later unless the title matches your current proof-agent work.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-10-02 arXiv

Law And Order: Tax Law Autoformalization

Sophia Simeng Han, Yoshiki Takashima, Anjiang Wei et al.

Legal systems are increasingly implemented through software, yet scalable methods for translating legal texts into accurate symbolic representations remain underdeveloped. We study this problem through tax law, where forms and filing instructions define lar...

Why it matters Useful for the informal-to-formal bottleneck: it is about preserving mathematical intent across the translation boundary.

Skim cue Skim which definitions entered Lean and whether the work adds reusable library surface.

Read if Save for later unless the title matches your current proof-agent work.

autoformalization

Open PDF Semantic Scholar

adjacent score 3.5 2026-10-02 arXiv

High-Rate Quantum Codes with Proven Distance and Low-Weight Measurements

Kishor Bharti, Tobias Haug, Runzhou Tao et al.

We study a family of quantum subsystem codes defined on rectangular coordinate grids of any dimension, with even side lengths of at least four. The directly measured operators act along coordinate lines. For every member of the family, we derive the number...

Why it matters Most relevant if you are tracking proof-search loops that use verifier feedback instead of treating Lean as a binary oracle.

Skim cue Skim the search loop: proposal source, verifier call, retry strategy, and stopping rule.

Read if Save for later unless the title matches your current proof-agent work.

verifier feedback

Open PDF Semantic Scholar

Watch Later

Adjacent formalization or infrastructure signals. Keep them in peripheral vision unless they match an active project.

adjacent score 1.9 2026-10-05 arXiv

The Lebrun--Salamon conjecture is true in dimension up to 56

Jordi Daura Serrano, Aron Gohr, Marie-Amélie Lawn et al.

We prove the LeBrun--Salamon conjecture for positive quaternionic Kähler manifolds of quaternionic dimension n <= 14. To do so, we first show that the isometry group Isom(M) of any minimal counterexample M has rank at most one, hence dimension at most three...

Why it matters Adjacent signal: scan the abstract for a concrete connection to formal proof, verification, or proof-agent evaluation.

Skim cue Skim the abstract first; open the paper only if the method touches proof agents or formal verification.

Read if Save for later unless the title matches your current proof-agent work.

AI math reasoning

Open PDF Semantic Scholar

adjacent score 1.9 2026-10-01 arXiv

When Do Intrinsic Rewards Lead to Exploration?

Scott W. Viteri, Laura Gomezjurado Gonzalez, Clark Barrett

Intrinsic rewards are designed to guide exploration in reinforcement learning by assigning value to an agent's experience, for example through prediction error or learning progress. However, maximizing these rewards need not produce the most informative exp...

Why it matters Training signal: worth scanning for reward design, experience collection, or process supervision that could transfer to theorem proving.

Skim cue Skim the reward construction and whether failures provide dense learning signal.

Read if Save for later unless the title matches your current proof-agent work.

RL or distillation

Open PDF Semantic Scholar

Older but Useful

0 relevant item(s) are outside the 21-day content window. Keep them for context, but do not let them drive today's scan.

No older useful items were retained in this run.

Downweighted 76 low-priority match(es), folded for daily reading.

negative score 0.8 2026-10-06 GitHub

leanprover/lean4: refactor: index `Lean.Order.iSup` and `iInf` over `Sort` (#15517)

Sebastian Graf

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

negative score 0.8 2026-10-06 GitHub

leanprover/lean4: perf: share server extension entries with the main table outside the server (#15512)

Sebastian Ullrich

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

negative score 0.8 2026-10-06 GitHub

leanprover/lean4: perf: return a pointer into the ir cache (#15520)

Henrik Böving

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

negative score 0.8 2026-10-06 GitHub

leanprover/lean4: perf: make high arity closures pass their arguments linearly if possible (#15131)

Henrik Böving

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

negative score 0.8 2026-10-06 GitHub

leanprover/lean4: fix: split an `∃` or `⨆` over a proposition on the RHS of a `vcgen` entailment (#15515)

Sebastian Graf

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

negative score 0.8 2026-10-06 GitHub

leanprover/lean4: fix: lake: fetch partial facets under their resolved keys (#15474)

Richard Beauchamp

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

negative score 0.8 2026-10-06 GitHub

leanprover/lean4: fix: generate the HTTP `Date` header without the timezone database (#15443)

Carlo Hamalainen

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

negative score 0.8 2026-10-06 GitHub

leanprover/lean4: fix: `grind` runs upward propagation from the `toProcess` queue (#15506)

Leonardo de Moura

Recent commit on leanprover/lean4.

Why it matters Toolchain signal: open only if the commit touches proof search, elaboration, tactics, Lake, or mathlib behavior you depend on.

Skim cue Skim only the changed subsystem and whether it affects your Lean workflow.

Read if Open only if you are debugging Lean or mathlib locally.

Open Semantic Scholar

Source Health

Warnings are preserved so failed sources do not silently disappear from the brief.

None