AI4Math

4core

11adjacent

75downweighted

0warnings

Today's Scan

Start with LeanPlan: Optimal Planning with LLM-Generated Heuristics and Admissibility Proofs, then An AI-Assisted Formalization of the Poincaré Conjecture. 15 fresh useful item(s) are inside the 21-day content window.

Source Mix

arXiv15

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

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

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

Humanize: Judgement Engineering for Agentic Coding

Sihao Liu, Ligeng Zhu, Zijian Zhang et al.

Agentic coding makes code generation cheap, but reliable completion remains difficult: the agent that writes the code is a weak judge of whether it is done. We present Humanize, a multi-agent orchestration workflow for agentic coding built around judgement...

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

Open PDF Semantic Scholar

adjacent score 4.9 2026-10-06 arXiv

Sum of Squares and Non Sum of Squares Regimes for the Toeplitz Bottcher Wenzel Form

Wenqi Zhu, Ping Nie

Toeplitz matrices are among the simplest structured models of translation invariance, arising naturally in convolution, stationary covariance models, and discretizations of translation-invariant operators. For a pair of real matrices, the Böttcher--Wenzel f...

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

Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification

Shuangjie Yao, Nikolaus Holzer, Mark Paul Santolucito et al.

Program verification establishes software correctness through machine-checkable proofs constructed in theorem provers. It's a guarantee especially valuable for code generated by large language models (LLMs), which is fluent but carries no assurance of corre...

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

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

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

When Double Rounding is Correct

Brett Saiki, Bill Zorn, Cynthia Richey et al.

Number libraries, which implement number formats and their arithmetic in software, are used to simulate hardware, making hardware behavior reproducible and thus verifiable and easier to design. However, modern machine learning accelerators are difficult to...

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

SpecGuard: Proving a Task Is Broken Before the Agent Cheats

Param Biyani, Krishnamurthy Dvijotham

As autonomous coding agents get increasingly deployed, the risk that accidental or adversarially injected misspecifications in tasks lead to dangerous agent behavior is critical to address. Prior work has shown that agents given such tasks rarely flag the c...

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

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.

Lean proof agents

Open PDF Semantic Scholar

adjacent score 3.5 2026-10-06 arXiv

More than 83.9% of the zeros of the Riemann zeta function are distinct and more than 67.35% are simple and on the critical line

Kristian Muri Knausgård

Let N(T) count the nontrivial zeros of the Riemann zeta function up to height T with multiplicity, N_d(T) the distinct ones, and N_0^s(T) those that are simple and on the critical line. We prove liminf N_d(T)/N(T) >= 1645064/1960733 = 0.83900...; earlier wo...

Why it matters Infrastructure signal: this may improve premise discovery, dependency retrieval, or library navigation for 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-07 arXiv

The Long Road to the Same Answer: Cognitive Bias Under Escalating Reasoning Budgets in Large Language Models

Obada Kraishan

Reasoning models allocate extra computation at inference time and present their answers as the product of deliberate thought. If this deliberation works the way dual-process accounts of human cognition suggest, longer thinking should weaken the classic deci...

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 task definition, metric, and whether the benchmark has Lean-checkable artifacts.

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

RL or distillation

Open PDF Semantic Scholar

adjacent score 1.9 2026-10-07 arXiv

Network Coding Can Beat Routing in Undirected Multiple-Unicast Networks

Xindan Zhang, Baochun Li, Zongpeng Li

Network coding lets the nodes of a network combine messages rather than merely forward them. In undirected networks, where the two directions of an edge share its capacity, Li and Li conjectured in 2004 that coding offers no advantage over fractional routin...

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

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 reasoning

Open PDF Semantic Scholar

adjacent score 1.9 2026-10-07 arXiv

Local Factors in the BSD Conjecture: A Unified Statistical View

David Kurniadi Angdinata, Kenny Lau, Ken Ono et al.

For elliptic curves $E/\mathbb{Q}$ in short Weierstrass form \[ E=E(a_4,a_6): y^2=x^3+a_4x+a_6, \] we derive a multivariable Euler product generating function which encodes the Tamagawa product $Tam(E)=\prod_p c_p(E)$. Using this generating function, we com...

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

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 reasoning

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

Let the Library Speak: Self-Advertised Method Selection for Formal Proving

Xiaopeng Yuan, Suijin Wang, Yanli Wang et al.

LLM-based formal provers can retrieve relevant lemmas and prior proofs, but relevance alone does not say whether a mathematical method can be used on the current theorem. A method has prerequisites, a target, an intended action, and obligations that its use...

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

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

negative score 0.8 2026-10-08 GitHub

leanprover/lean4: perf: size IR `importedEntries` only for extensions with IR entries (#15538)

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

leanprover/lean4: perf: initialize only what `leanir` imports (#15566)

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

leanprover/lean4: fix: make equation lemma statements independent of the caller's options (#15499)

Marcelo Lynch

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

leanprover/lean4: fix: assorted `compiler.postponeCompile` fixes (#15565)

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

leanprover/lean4: chore: update stage0

Lean stage0 autoupdater

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

leanprover/lean4: chore: update release scripts (#15564)

Garmelon

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

leanprover-community/mathlib4: refactor(RingTheory/FractionalIdeal): make spanSingleton a monoid with zero homomorphism (#44475)

Xavier Roblot

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

leanprover-community/mathlib4: fix(Translate): improve translation heuristic (#44266)

Jovan Gerbscheid

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