AI for Formal MathIssue 14Nov 7 – 14, 2026

Prover training shifts toward agent-native data, verification becomes the new bottleneck

Highlights

Last issue, we paused at the route divergence of "whether minimalist test-time scaling unconditionally dominates complex harnesses." This issue, the artillery of prover training has turned to a more upstream question: what data is fed to the model, and how RL reshapes search behavior. daVinci-Prover presents the first Lean 4 agent-native mid-training experiment—explicitly injecting decomposition, search, self-verification, and revision skill priors into the mid-training corpus, along with environment-native agent trajectories; its ablations yield a conclusion worth revisiting: the gain from 8.4B agent-native supervision tokens exceeds that from 25.3B general skill tokens, and the two are complementary. Reap directly implements MCTS as a Lean tactic, sharing the same search and replay verification between training and inference, and is the first to systematically characterize how RL alters proof search behavior—later-stage models tend to use structural macro-actions like have/suffices to compress search depth into fewer but more compound steps. Together, they point to the same judgment: distribution alignment and "organizing proofs by proof statements" macro-actions are becoming new levers on the training side.

Evaluation and library construction are also moving. TCSExam unifies theorem proving, solver engineering, construction, and open conjecture resolution into a single evaluation framework where all tasks are verified by the Lean kernel, and reports independent verification cases of nine-dimensional Alon–Jaeger–Tarsi and other open conjectures; LeanContext provides a controlled benchmark with decoupled mathematical statements and environment instructions for whole-proof generation, using cross-training/inference designs to answer "how statement visibility interacts with training." And Statopia turns the "prover-library ecosystem" into an end-to-end system in statistics: a self-contained proof runtime and a co-designed Statlib library co-evolve, with proof evidence driving library evolution—a full landing of a domain-specific prover.

What sets the scale and tone of this issue are community-side milestones. The Weil Conjectures formalization and the Stacks Project formalization were announced back-to-back—the former reportedly completed in 24 hours by an AI agent, with sorry-free Lean proofs of all four Weil conjectures, directly reusing the Stacks library. Meanwhile, AlphaProof Code pushes verification to AArch64 machine-code level: about 6.5 million lines of Lean proofs for the Signal protocol. Once output scale crosses the threshold where "humans cannot review line by line," a new engineering bottleneck emerges—AI now writes Lean proofs faster than Lean can check them. The optimization goal is shifting from "finding proofs" to "verifying and compiling proofs faster," which might be the most concerning wall ahead for this direction.

Community and Updates

  • First complete formalization of the Weil Conjectures in Lean: The Weil Conjectures, Formalized in Lean announces that all four Weil conjectures (rationality, functional equation, Deligne's Riemann hypothesis, and Betti number comparison) are formalized sorry-free, directly on top of the Stacks Project library, reportedly produced by an AI agent in 24 hours across about 980 modules; the README explicitly states "not yet human-reviewed," and independent reconstruction and semantic verification remain open.
  • Full formalization of the Stacks Project library: The Stacks Project, Formalized in Lean reports a whole-library formalization of about 16 million lines of Lean, completed by a coordinated AI-agent swarm, and identifies a set of statements that do not hold under the claimed generality—this "discovery of failure" result goes beyond mere translation.
  • AlphaProof open-source code verification pipeline: Introducing AlphaProof Code and the code-verification repository open-source the first artifact that pushes safety proofs to AArch64 machine-code level for the Signal protocol: about 6.5 million lines of Lean proofs, built on about 26,000 lines of trusted specifications and AArch64 semantics, directly linking protocol-level safety guarantees to unmodified implementations. The open-sourced specifications and semantics of the repository make this AlphaProof-style pipeline reproducible and auditable for the first time.
  • First Mathlib proof of the weak prime number theorem: Feat(NumberTheory/LSeries) connects the Wiener–Ikehara Tauberian theorem to the prime-counting function, giving the first Mathlib formalization of the weak prime number theorem, opening analytic number theory in Lean.
  • LeanDojo-v2 unified infrastructure: lean-dojo/LeanDojo-v2 is released, converging theorem proving, proof search, and AI auto-completion into a single reproducible toolchain—an infrastructure version worth tracking in the neural prover pipeline.
  • Mathlib CI deduplication report: duplicate declarations report introduces a weekly automated CI workflow to detect and report duplicate declarations, adding a small piece to address the growing library maintenance pressure under the "AI proof flood."

Open Questions

  1. This issue's Weil Conjectures and Stacks Project push the "verification as trust" boundary, raised last issue at the CFSG 43M-line scale, into the core of algebraic geometry and whole-library scale. If "human review" fails due to scale, what should independent verification look like—rebuilding the entire library, spot-checking the dependency tree axioms, or verifying the statement fidelity of final theorems?
  2. Reap's "search-interaction compression" observation—that later RL models use fewer but more compound macro-actions (have/suffices) to compress depth and increase per-action cost—does it imply that standard pass@k and budget metrics are distorted when comparing across training stages? Is there a principled metric measuring "proof planning quality" rather than just length?
  3. daVinci-Prover shows that 8.4B agent-native tokens yield greater gains than 25.3B skill tokens. Does this "data distribution alignment over size" effect persist with model/data scale, or is it diluted with larger corpora? How can the risk of overfitting agent trajectory data to a specific harness be measured?
  4. AI writes proofs faster than Lean can check them moves the bottleneck from search to kernel checking. Can the verification/compilation layer achieve scale dividends similar to the search layer—trusted but accelerated elaborators, parallel-replayable checkers, or controlled trade-offs between precision and checking cost—and will this become the next target for GPU acceleration?

Papers in this issue

  1. Reap: Uncovering Monte Carlo proof search with a lightweight model

    Reap's Lean-native MCTS framework with the 1.7B-parameter Reaper-1 model achieves 79.9% on miniF2F-test, revealing RL compresses search into fewer, more powerful tactic steps.

    Editor's note

    Implements MCTS directly as a tactic in Lean 4, enabling training and inference to share the same search and replay verification, achieving 79.9% pass@32 on miniF2F with a 1.7B model; code and weights are open-sourced. Compared to NanoProof (factorized execution-guided search) in issue 12 and SCOPE (strategy planning) in issue 11, its increment lies in the observability design of Lean-native MCTS and the first systematic characterization of how RL reshapes proof search—later models tend to use structured macro-actions like have/suffices to compress search depth into fewer but more compound steps (search-interaction compression). This behavioral analysis is particularly valuable for designing training objectives and search strategies.

  2. daVinci-Prover: Agent-Native Mid-Training for Formal Theorem Proving

    daVinci-Prover's 33.7B-token mid-training corpus, combining skill priors with agent-native trajectories, boosts theorem-proving pass@1 by 13.7 points over SFT baselines.

    Editor's note

    The first work to systematically introduce agent-native mid-training in Lean 4: in a 33.7B-token mid-training corpus, it explicitly injects decomposition, search, self-verification, and revision skill priors, along with environment-native agent trajectories to bridge the distribution gap between static training and interactive reasoning. Compared to NanoProof (publishing proof tree datasets and training pipelines) in issue 12 and OProver (65B mid-training but without agent-native trajectories) in issue 11, its increment lies in clear ablations: the gain from 8.4B agent-native tokens exceeds that from 25.3B general skill tokens, and the two are complementary. The harness design (7 tools, isolated workspaces, strict verification) and memory compression mechanisms are also worth borrowing; note that it relies on frontier closed-source models for data generation and code is not yet public, so results should be treated as relative signals.

  3. TCSExam: Evaluating Frontier LLMs on the Full Range of TCS Research

    TCSExam benchmark shows frontier LLMs can prove research theorems, improve solver references, and exceed construction records, with GPT-6 Astra leading at 71.9 index points.

    Editor's note

    The first to unify theorem proving, solver engineering, construction, and open conjecture resolution into a single evaluation framework, with all tasks verified by the Lean kernel or executable checkers, and introduces the Lite subset (20 tasks) retaining strong rank consistency with Full using 80% fewer attempts (Spearman ρ=0.93). Compared to reuF2F (only open conjecture formalization) in issue 11 and the Annals dataset (only theorem statements) in issue 10, its increment lies in covering the full spectrum of TCS research output types and reporting independent verification progress on open conjectures like nine-dimensional Alon–Jaeger–Tarsi. The theorem proving track's bare/ladder/guided three settings and verification protocol are reusable for proof search evaluation; results partially depend on frontier closed-source models, so they should be treated as relative signals.

  4. Statopia: A Prover--Library Ecosystem for Automated Formalization and Proof Discovery in Statistics

    Statopia's prover-library ecosystem achieves 100% first-run formal proof discovery on 83 statistics benchmarks at $0.57 per problem.

    Editor's note

    An end-to-end 'prover-library ecosystem' in statistics: a self-contained proof runtime (with its own agent loop, context management, tool execution, and acceptance checks, rather than embedding Claude Code/Codex) combined with a co-designed Statlib library, implementing proof-driven library evolution and prover-native retrieval. Compared to Maestro (global coordination) in issue 12 and SCOPE (strategy planning), its uniqueness lies in being domain-specific rather than a general prover, with a dynamic proof DAG supporting parallel and resumable long proof development, and task group organization aligned with statistical paper structures. The benchmark scale is limited and some results depend on specific models, so they should be treated as relative signals, but the architectural paradigm is worth referencing.

  5. LeanContext: Disentangling Mathematical Resources from Local Formal Context in Lean Whole-Proof Generation

    LEANCONTEXT benchmark reveals that mathematical declarations only improve theorem proving when models train with them, boosting Pass@32 by 7-8% after MC-inclusive training.

    Editor's note

    A controlled benchmark of 129,826 Lean whole-proof generation problems that explicitly decouples mathematical statements (MC) from environment instructions (EC), supporting cross-training/inference evaluations and paired replacement tests on statement visibility under fixed targets and verification environments. Compared to previous context benchmarks like miniCTX, its increment lies in a systematic MC/EC split and four aligned input views, using dependency-first selection to improve Pass@32 by 1.4–1.7 percentage points without reference proofs. It provides rigorous evaluation methodology for premise selection and context-aware provers; gains are modest but results are reproducible.

  6. No regular icosahedron has a rational point on every face: a proof checked in Lean

    No regular icosahedron in 3D space has a rational point on every face, proved via exact arithmetic and fully verified in Lean 4.

    Editor's note

    Provides the first complete Lean 4 formalization of a negative answer to the MathOverflow open problem 'Can the icosahedron have rational points on each face?', with all 48 certificates individually verified by decide+kernel using exact arithmetic on Z[φ], without using native_decide or any trusted external solver; the main theorem depends only on standard axioms. Compared to previous combinatorial formalizations relying on external SAT certificates (e.g., Ramsey numbers), its increment lies in a purely kernel-verified geometric impossibility proof—providing a clean benchmark for a trusted proof pipeline that is fully reproducible and free of external trust interfaces; the work is also a beautiful sample of open problem formalization.