AI4Math

6core

6adjacent

78downweighted

0warnings

Today's Scan

Start with Second-Order Problem Solving for Recursive Self-Improvement in Formal Verification, then LeanPlan: Optimal Planning with LLM-Generated Heuristics and Admissibility Proofs. 12 fresh useful item(s) are inside the 21-day content window.

Source Mix

arXiv12

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 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 7.9 2026-10-06 arXiv

LeanPlan: Optimal Planning with LLM-Generated Heuristics and Admissibility Proofs

André G. Pereira, Augusto B. Corrêa, Felipe Meneguzzi et al.

Frontier large language models (LLMs) can generate heuristic functions that guide search to achieve state-of-the-art performance in satisficing planning, where any plan is acceptable. However, these heuristics are not guaranteed to be admissible and can lea...

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 agentstool-use agentsverifier feedback

Open PDF Semantic Scholar

core score 7.3 2026-10-06 arXiv

An AI-Assisted Formalization of the Poincaré Conjecture

Zhiyuan Zhang, Axel Delaval, Leheng Chen et al.

We present an AI-assisted Lean 4 formalization of the Poincaré conjecture. The project began with limited reusable formal infrastructure for the geometric analysis behind the proof. To organize this work, we combined a proof blueprint prepared by mathematic...

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 Read if you have 5 minutes and want a direct AI4Math signal.

AI math reasoningLean proof agentsseed author: Bin Dongseed author: Jiedong Jiang

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.5 2026-10-06 arXiv

Unimodality of Forest Independence Polynomials

Wei Li, Kevin Vallier, Tong Zhang

For a finite forest $F$ let $i_k(F)$ be the number of independent sets of $F$ with $k$ vertices. Zhang and Li proved that the sequence $i_0(F),i_1(F),\dots,i_{α(F)}(F)$ is unimodal for every finite forest $F$, which answers Erdős Problem 993. We give a seco...

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 Read if you have 5 minutes and want a direct AI4Math signal.

Lean proof agents

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

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 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 1.9 2026-10-06 arXiv

SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner

Hanchao Zhou, Jialei Li

In proof assistants such as Lean, a generated proof must pass machine compilation checks, so evaluation needs no human scoring. Direct generation fails on multi-step numeric propositions: a proof is valid only if every content integer is correct, so the pas...

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.

tool-use agents

Open PDF Semantic Scholar

adjacent score 1.9 2026-10-06 arXiv

Carlet's cyclic-additive conjecture for the Kasami monomials

Gábor P. Nagy, Douglas S. McNeil, Attila Vajda

Let $K$ be a finite field of characteristic two with $|K| = 2^{n}$, let $\gcd(k,n) = 1$, let $d_{k} = 4^{k} - 2^{k} + 1$ be the Kasami exponent, and let $Δ_{k} = \{(b+1)^{d_{k}} + b^{d_{k}} + 1 : b \in K\}$ be the image of the normalised derivative of the K...

Why it matters Infrastructure signal: this may improve premise discovery, dependency retrieval, or library navigation for agents.

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-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

Watch Later

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

No watch-later items in this run.

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 78 low-priority match(es), folded for daily reading.

negative score 0.8 2026-10-07 GitHub

leanprover/lean4: refactor: implement `String.toList` in Lean (#15533)

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-07 GitHub

leanprover/lean4: perf: store imported module names in the environment header (#15543)

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-07 GitHub

leanprover/lean4: perf: read reducibility status of theorems without waiting for their proofs (#15534)

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-07 GitHub

leanprover/lean4: fix: use the RFC 9110 `GMT` date format for the HTTP `Date` header (#15469)

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-07 GitHub

leanprover/lean4: fix: race condition in IR interpreter debug code (#15539)

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-07 GitHub

leanprover/lean4: fix: make timers and signals safe against re-entrant continuations and lost signals - #15191 (#15523)

Sofia Rodrigues

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-07 GitHub

leanprover-community/mathlib4: refactor(Algebra/Lie/Cochain): simplify scalar compatibility proofs (#44514)

Kim Morrison

Recent commit on leanprover-community/mathlib4.

Why it matters Infrastructure signal: this may improve premise discovery, dependency retrieval, or library navigation for agents.

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-07 GitHub

leanprover-community/mathlib4: fix(scripts/dag_traversal.py): kill timed-out builds on Windows (#44403)

Zhi Kai Pong

Recent commit on leanprover-community/mathlib4.

Why it matters Infrastructure signal: this may improve premise discovery, dependency retrieval, or library navigation for agents.

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