AI4Math

5core

12adjacent

73downweighted

0warnings

Today's Scan

Start with NanoProof: Open and Efficient Automated Theorem Proving in Lean 4, then Verification with Transfer: Exact Information Frontiers and Their Price in Calls. 17 fresh useful item(s) are inside the 21-day content window.

Source Mix

arXiv17

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

NanoProof: Open and Efficient Automated Theorem Proving in Lean 4

Matěj Kripner, Milan Straka

We introduce NanoProof, to our knowledge the first factorized execution-guided theorem prover in Lean 4 whose training data, extraction tooling, training pipeline, and weights are all released, making it end-to-end reproducible using open-source resources....

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

Verification with Transfer: Exact Information Frontiers and Their Price in Calls

Hazar Yueksel

A verifier that accepts or rejects whole answers reveals little: under a flat prior over $k$-bit answers, zero error needs $2^k-1$ verifications. The usual remedy is to solve related source tasks, either all first, as a curriculum does, or interleaved with...

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

Open PDF Semantic Scholar

core score 6.5 2026-10-08 arXiv

LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs

Nihal Jain, Shuangjie Yao, Begum Cicekdag et al.

Mathematicians value proofs for more than correctness: among correct proofs, simplicity, purity and the computational cost of finding them vary widely. Yet LLM-powered theorem provers largely search for any correct proof, and improve its quality only after...

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

Hierarchical Melnikov Realization: Logarithmic Factor Improvement to Hilbert Number Lower Bounds

Chaoyang Qin, Xiaoming Sun

The second part of Hilbert's 16th problem is one of the most fundamental open problems in the qualitative theory of ordinary differential equations and dynamical systems. A central unresolved question is whether the Hilbert number $H(d)$ is finite for arbit...

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

Open PDF Semantic Scholar

core score 6.5 2026-10-07 arXiv

Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation

Srijith Nair, Aditya Vempaty, Jia Liu et al.

When generating verifiable code, natural language requirements are mapped to machine checked code using LLMs and agentic workflows. A crucial component of this pipeline is specification generation (SpecGen), which produces a formal contract against which an...

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.

verifier feedback

Open PDF Semantic Scholar

adjacent score 3.5 2026-10-08 arXiv

Universal Radial Laws for Random Polynomials: Erdős Problem #522 and Non-Universal Fluctuations

Sebastien Kawada

We resolve Erdős Problem #522, posed in 1961, by proving that for random Littlewood polynomials the proportion of zeros in the closed unit disk converges almost surely to $1/2$. More generally, for partial sums of random power series with i.i.d. coefficient...

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

The rank of $3\times 3$ matrix multiplication over $\mathbb{F}_2$ is 23

Tejasvi Singh Tomar

The rank of the tensor of $3\times 3$ matrix multiplication over the field with two elements is at most $23$ by Laderman's algorithm, and Rudich and Rousseau recently proved that it is at least $22$. We prove that it equals $23$. Hence Laderman's algorithm...

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

Natural Language to First-Order Logic LLM-based Autoformalization

Andrea Brunello, Cristian Curaba, Luca Geatti et al.

Large Language Models (LLMs) have renewed interest in autoformalization. Yet, when First-Order Logic (FOL) is considered as the target formalism, the field still lacks a unified task formulation and a systematic survey. This paper addresses this gap: we fir...

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

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.

autoformalization

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

An Explicit Counterexample to Tsirelson's Problem via a Linear System Game

Minbo Gao, Tianshi Yu, Lihong Zhi

We construct an explicit binary linear system game that separates $C_{qa}$, the closure of the set of finite dimensional quantum correlations, from $C_{qc}$, the set of commuting operator correlations. The game admits a perfect commuting operator strategy,...

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

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

Watch Later

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

adjacent score 3.5 2026-10-06 arXiv

An upper bound of 4.268 for the random 3-SAT satisfiability threshold

Fedor Vorobyev

We prove that a random 3-SAT formula with $n$ variables and $\lfloor 4.268n\rfloor$ clauses is unsatisfiable with high probability. The satisfiability threshold has attracted considerable attention: successive upper bounds reached 4.4898 in the work of Díaz...

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

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

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

negative score 0.8 2026-10-10 GitHub

leanprover/lean4: refactor: share error and promise helpers in the libuv bindings (#15594)

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

leanprover/lean4: refactor: embed libuv handles in the uv socket, timer and signal objects (#15545)

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

leanprover/lean4: refactor: add RAII-based scoped lock guard (#15547)

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

leanprover/lean4: chore: lake: clear IR artifacts before `leanir` (#15570)

Mac Malone

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

leanprover-community/mathlib4: refactor(LinearAlgebra/PiTensorProduct/Finite): reduce assumptions for instance PiTensorProduct.finite (#44429)

DanielJHorton

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

leanprover-community/mathlib4: feat(RingTheory/ZMod/LocalRing): add that `ZMod (p ^ r)` is a local ring (#43898)

Nicola Falciola

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

leanprover-community/mathlib4: feat(NumberTheory/LSeries): define Hardy's Z function (#42963)

Thomas Lince

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

leanprover-community/mathlib4: feat(LinearAlgebra): make two `Nontrivial` theorems low priority instances (#44558)

Vlad Tsyrklevich

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