A Cold Shower for Complex Harnesses: Minimal Loops Are Winning in Theorem Proving
Highlights
In the previous issue, we summarized the architectural shift in agentic proof search as "the model only plans, while execution is left to tools and the kernel." This issue presents a direct counter-thesis—A Taste of the Bitter Lesson in Automated Theorem Proving uses a "minimal harness + the same test-time scaling loop" to match or even Pareto-dominate the complex specialized workflows like Maestro and SCOPE from Issue 11, under matched model and inference cost, and demonstrates that persistent single attempts (pass@1) outperform repeated sampling (pass@k) on open problems. This is a controlled rebuttal to the belief that "complex coordination architectures are indispensable": at least at the difficulty level of existing benchmarks, an unstructured simple loop is a stronger baseline. It directly determines the strategic choice of "whether to continue stacking harness complexity."
The direction itself is expanding. Agents are no longer just "proving"—Agentic Algorithm Design lets LLMs design black-box optimization algorithms and machine-verify their expected runtime bounds (drift certificate) in Lean, pushing formalization from theorems to the concatenation of "algorithm design + complexity guarantees"; Scaling Lean Theorem Proving for Real-World Code Verification transforms competitive programming problems into Lean verification tasks with implementation-level obligations, producing an adversarial benchmark far from saturation. On the evaluation and verification front, semantically aligned evaluation objects are also moving from statement-level to project-level dependency context.
Community dynamics have pushed the scale to unprecedented heights: CFSG's 43.1M lines of formalization and the Lean 100 theorems set have both been officially announced. These milestones redraw the upper bound of "what agentic formalization can do" and also cast the question "at what scale can sorry-free statements be trusted, and how to independently re-verify them" back into the spotlight.
Community and Updates
- CFSG's 43.1M-line formalization of the "Enormous Theorem": Formalizing the Enormous Theorem announces the completion of a sorry-free Lean 4 formalization of the first-generation proof of the Classification of Finite Simple Groups (CFSG) by an AI agent swarm in 24 days (including statements, approximately 43.1 million lines, 2.05 million statements), making it the largest Lean codebase to date; during the process, a counterexample was found in Walter's proof of a certain closure assertion, and a new apex theorem was proposed using Solomon 1976's theory of maximal 2-components to bypass it. Currently, no external team has completed a reconstruction, and the 43M-line sorry-free claim still requires independent verification.
- Lean completes all 100 theorems for the first time: All 100 theorems in Lean announces that all 100 theorems on Freek Wiedijk's list have been proved for the first time in a single proof assistant (Lean), with the last theorem (a strong form of Green's theorem) completed by the automated formalization library Tau Ceti.
- Multi-million-dollar grants funding Mathlib formalization infrastructure: Resolution Grants $1M to Mathlib's Formal Commons funds protocols and tools in the Mathlib ecosystem to cope with the "AI proof flood" (maintaining high standards for definitions and statements, allowing lower-quality proofs); UCL researchers awarded $1 million funds building a searchable database of Mathlib theorems verified by Lean (DTT-DB). Both point to the increasingly pressing bottleneck of "organizing and reusing formalized results."
- Lean 4.36-rc2 automation performance optimizations: perf: share
liaproofs acrossgrindcase splits allowsgrindto reuselialinear arithmetic proofs across case splits, significantly speeding up split-heavy goals; Lean 4.36.0-rc2 release notes also introduce a Sym.simp-based grind normalizer and CEGAR/UF modes for bv_decide with incremental SAT. - Navier-Stokes fidelity debate continues to intensify: Advancing mathematics research with AI-driven formal proof search publishes the peer-reviewed version of AlphaProof Nexus (an evolutionary agent that can call itself as a sub-tool); meanwhile, AI is shaking up math. But can its proofs be trusted? and Mathematicians find two gaps between OpenAI's Navier-Stokes proof and its code continue to characterize the gap between "Lean kernel verification passing" and "correctness of the natural-language proof."
- Prove2Me Fermat's Last Theorem and independent audit resources: Fermat's Last Theorem: a milestone for Prove2Me reports the first Lean formalization of Fermat's Last Theorem completed end-to-end by a single agent (Claude) and independently verified by Kevin Buzzard; the audit site MathVet systematically questions whether AI-generated Lean statements faithfully represent the mathematical claims in the source papers, providing a stable skeptical perspective for automated formalization evaluation.
Open Questions
- CFSG's 43.1M lines are two orders of magnitude larger than the Poincaré conjecture from Issue 10 (2.8M lines). For such a large-scale "AI-generated + kernel-verified" claim, what should independent re-verification actually check—the actual set of axioms in the dependency tree, the fidelity of "the final theorem indeed states the classification," or whether every line actually passes in the kernel? The scale of 43M lines makes spot-checking nearly infeasible; does "verify by trust" reach an impractical boundary here?
- The preliminary "bitter lesson" conclusion may hold only within the difficulty threshold of existing benchmarks—when task complexity advances to the early stages of CFSG or open-problem scale, will the minimal test-time scaling loop hit a "long-horizon failure" threshold that only global coordination like Maestro can cross? Does the complexity benefit have a critical threshold, rather than being unconditionally dominated by simple loops?
- Can structure-aware equivalence from Issue 11 scale to become the default verification gate for automated formalization—MechAlign in this issue advances semantic alignment to project-level dependency context (LeanTrace), which is a step in that direction; but can "honest mapping" versus "fabricated fidelity" at the project level still only be judged by human audit?
- The drift certificate pipeline in Agentic Algorithm Design is currently limited to simplified scenarios (fixed drift quantification, single capability bound). Will machine-verified runtime bounds grow into a formalization subfield independent of theorem proving, or remain a constrained toy of "propose + verify"? Can it in turn provide verifiable heuristics for neural provers?
Papers in this issue
A simple agentic loop with efficient Lean feedback and test-time scaling matches or outperforms specialized theorem-proving workflows, solving eight open problems at lower cost.
Editor's noteDirectly challenges the belief from Issue 11 that complex harnesses (Maestro's global coordination, SCOPE's policy planning) are indispensable: under matched model and inference cost, a minimal test-time scaling loop matches or Pareto-dominates these complex specialized workflows, providing reproducible cost-success curves and ablations. Its increment lies in the first systematic comparison of different simple harness efficiencies (tool interfaces, context reuse) and demonstrating that persistent single attempts (pass@1) outperform repeated attempts (pass@k) on open problems. A sobering contrast for researchers who treat harness complexity as the default path.
This pipeline is the first to have LLMs automatically design black-box optimization algorithms and prove their runtime bounds in Lean, discovering novel algorithms including a quadratic-time solution for CYCLEUNCOVER.
Editor's noteThe first automated pipeline that lets LLMs design black-box optimization algorithms and machine-verify their expected runtime bounds in Lean, without empirical evaluation throughout. Compared to Maestro/SCOPE from Issue 11 (proof search and textual planning), its increment lies in formalizing randomized runtime analysis (drift certificate) for LLM-proposed algorithms, and achieving exponential improvement over (1+1) EA on CycleUncover; the staged pipeline using Lean guards to filter defective designs is directly transferable to trustworthy agentic proof systems. Limitations (only frontier models, simplified drift theorems) are clearly stated in the paper.
EASYPROVER, an untrained agentic harness with recursive delegation and parallel probing, saturates existing benchmarks but proves only 52.7% of new AEGIS code-verification tasks.
Editor's noteTransforms competitive programming problems into Lean verification tasks with implementation-level obligations, producing 11,553 candidate specifications and 2,045 differentially verified Rust–Lean programs, far from saturation (52.7% solve rate vs. near-saturated 99.6% on PutnamBench). Compared to ITPEval (cross-ITP translation) and reuF2F (open conjectures) from Issue 11, its increment lies in automatically generating tasks with implementation-level obligations such as fixed-width arbitrary arithmetic, explicit failures, generative loops, casts, and functionalized mutations, and providing negative labels through counterexamples—something pure proof loops cannot do. The engineering insights of EasyProver (recursive agent, isolated context, InfiniLean stateless elastic elaborator) are also valuable; note its lack of component ablations and use of untrained off-the-shelf frontier models; the benchmark itself is a more lasting contribution.
MechAlign uses dependency-guided review with LeanTrace to localize semantic gaps between formal Lean statements and informal mathematical claims, outperforming full-project access.
Editor's noteAdvances semantic alignment evaluation from statement-level to project-level: LeanTrace builds a statement dependency graph from the elaborated type of a selected theorem along declarations and non-proof definition bodies, truncating at library boundaries, allowing reviewers to locate semantic differences via the dependency graph. Compared to the structure-aware equivalence (statement-level) from Issue 11 and FaithAlign (phrase-level) from Issue 10, this is a clear increment, directly responding to the judgment that "statement-level formalization is saturating"; the HyperbolicObstruction case (missing dimension constraint) demonstrates the practical value of project-level review, and LeanReviewBench (501 fixed triples) provides a reproducible comparison resource.
Count-catcher converts d4's CPOG certificates into Lean theorems, formally proving exact model counts up to 10^28 without enumeration, with terabyte-scale feasibility.
Editor's noteThe first work that converts exact model counting (CPOG) certificates into CNF clauses as Lean theorems, enabling end-to-end machine verification of counts for combinatorial objects like Latin squares without enumeration. Its increment lies in bit-parallel reverse checking, symmetry composition via Burnside's lemma (composition-by-symmetry), and fixing a bug in the CPOG checker. Although it does not involve neural proof or LLM automated formalization, it provides a robust foundation for trustfully integrating computational results into formal libraries, and is a rare fully reproducible artifact in this direction.
Crush proves higher-order Lean goals to SMT solvers via mechanized defunctionalization, achieving 94% verification coverage and outperforming all baselines.
Editor's noteThe first hammer framework in Lean 4 that simultaneously provides an extensible Lean-to-SMT translation interface and an extensible proof replay interface (register_lowering, register_crush_replay), supporting higher-order functions via defunctionalization (function-valued arguments, partial application, lambdas), and formally proving the soundness of the translation in Lean—something not covered by previous lean-smt/lean-auto. It offers a new paradigm for building domain-specific SMT backends for bitvectors, arrays, etc.; although the benchmarks are more program verification than mathematical theorems, its defunctionalization soundness proof has reference value for verifier integration in neural proof search.
The paper proves every 4-coloring of K61 contains a monochromatic triangle, improving the Ramsey number R(3,3,3,3) upper bound from 62 to 61 via SAT solving and Lean verification.
Editor's noteImproves the upper bound of the classical Ramsey number R(3,3,3,3) from 62 to 61, the first improvement since 2004: via global association (ticket) counting and local neighborhood classification, the proof is decomposed into 56,723 SAT formulas, formalizing the mathematical reduction in Lean 4, and verifying unsatisfiability of all formulas with two SAT solvers. This hybrid verification framework of "formalized reduction + external SAT refutation", along with a fully reproducible artifact (code, data, verification scripts), has direct relevance for integrating large combinatorial proofs into trustworthy proof pipelines.
VAMPIRE-HAMMER integrates VAMPIRE with LEAN to solve 96,289 Mathlib theorems, uniquely proving 21,158 problems no other tool handles, with full kernel-verified proof reconstruction.
Editor's noteThe first hammer in Lean 4 with full support for native proof reconstruction of Vampire: extends Vampire to output annotated TSTP proofs (recording substitutions, literal removal positions, commutativity bridges) and reconstructs the entire refutation proof in the Lean kernel without trusting the translation, reconstruction, or Vampire itself. Compared to Teaching Vampire New Tricks from Issue 6 (only clause selection evaluation, no proof reconstruction), its increment lies in an end-to-end native proof production pipeline, covering 21,158 Mathlib theorems unsolved by other tools. Note that its evaluation uses premises extracted from proofs rather than end-to-end premise selection, so results should be treated as relative signals, but the reconstruction mechanism has direct reference value for integrating external reasoners into Lean.
