AI4Math

5core

10adjacent

75downweighted

0warnings

Today's Scan

Start with NanoProof: Open and Efficient Automated Theorem Proving in Lean 4, then Humanize Olympiad Agents: A Multi-Session Workflow for Olympiad Problem Solving with Solve, Review, Wiki, Verify. 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 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 10.5 2026-10-09 arXiv

Humanize Olympiad Agents: A Multi-Session Workflow for Olympiad Problem Solving with Solve, Review, Wiki, Verify

Zhengyang Zhang, Jing Xiong, Hongzhou Lin et al.

Large language model (LLM) agents are rapidly improving on long-horizon scientific and olympiad tasks. Recent systems have produced a Lean-formalized resolution of the Navier--Stokes problem and autonomous solutions to four open questions in the Erdős Conje...

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.

AI math reasoningseed author: Hongzhou Linverifier 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

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

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

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

adjacent score 4.3 2026-10-09 arXiv

A Lean Formalization of the Hamilton--Perelman Proof of Thurston's Geometrization Conjecture

Yuan Liao, Ziyang Qin, Jui-Hui Chung et al.

We formalize the Hamilton--Perelman Ricci-flow proof of Thurston's geometrization conjecture. The public Lean declaration is reproduced in this paper. Its geometric interpretation follows, and verification is recorded in 4.

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 reasoningseed author: Hongzhou Linseed author: Jui-Hui Chung

Open PDF Semantic Scholar

adjacent score 3.5 2026-10-09 arXiv

SqueezeBench: Saturation-Resilient Evaluation of Mathematical Capability

Pablo Manrique, Hai Xia, Stefan Szeider

AI systems are making rapid progress in mathematics, but this progress is hard to measure. Benchmarks of solved problems saturate, and in benchmarks of open problems each problem can be resolved for the first time only once. We present SqueezeBench, a bench...

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 Save for later unless the title matches your current proof-agent work.

verifier feedback

Open PDF Semantic Scholar

adjacent score 3.5 2026-10-09 arXiv

Exact rational certificates and a Lean formalization of the eleven-variable Vasc inequality

Dakai Guo, Ruichen Qiu, Yichuan Cao et al.

We prove that the cyclic sum $\sum_{i=0}^{10}(x_i-x_{i+1})/(x_{i+1}+x_{i+2})$ is nonnegative for every strictly positive real eleven-tuple, with indices taken modulo eleven. Clearing denominators reduces the problem to a homogeneous polynomial. Subtracting...

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

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

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

Watch Later

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

adjacent score 1.9 2026-10-08 arXiv

Improving the lower bound on the Laughlin gap: An SDP search

Qiang Gao

A recent preprint by OpenAI resolved the spherical fermionic Laughlin spectral-gap conjecture for the full $V_1$ interaction by a Fock-space inequality: $H_Q^2\ge γH_Q$ on the lowest-Landau-level Fock space for all large flux $Q$ and every $γ$ below $0.0461...

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

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.

AI math reasoning

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

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

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

leanprover/lean4: test: shrink `ctor_many_fields` further (#15649)

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

leanprover/lean4: fix: export lemmas from `Init.Data.Int.DivMod.Pow` (#15659)

Julia Markus Himmel

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

leanprover/lean4: fix: `String` memory leak (#15654)

Julia Markus Himmel

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

leanprover/lean4: feat: simprocs for `UIntX`/`IntX` bitwise operations (#15647)

Julia Markus Himmel

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

leanprover/lean4: feat: proper UTF-8 string comparison (#15581)

Julia Markus Himmel

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

leanprover/lean4: feat: add `distrib` option to control product expansion in the `grind` normalizer (#15642)

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

negative score 0.8 2026-10-13 GitHub

leanprover/lean4: feat: add `--add-downstream` and `--add-public-downstream` to `lake shake` (#15630)

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

leanprover/lean4: feat: `String.fromUTF8Lossy` (#15651)

Julia Markus Himmel

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