Issue 3: The Kernel as the Trust Chain — AI Attacks the Lean Kernel and the Rise of Open-Weight Proof Engines
Highlights of This Issue
The most central signal this issue comes from the very bottom of the "trust chain": the Lean kernel itself. Leonardo de Moura's postmortem report on the kernel soundness bug hunt documents a coordinated bug hunt led by an internal OpenAI model—AI found real soundness vulnerabilities in the Lean runtime (a reference counting overflow that could prove False, and a defect in an old GMP version), leading to the Lean v4.33.1 fix and multi-kernel verification mechanisms such as lake check. This reminds us that the "statement semantic matching" discussed in the previous issue is only one link in the trust chain; the reliability of formal results ultimately depends on the kernel itself—and the kernel has now also been shown to be a target that AI can attack. de Moura explicitly recommends treating AI-generated proofs as potentially malicious input, setting a new security baseline for all agentic proof systems.
Running parallel to "trust" is the theme of "reproducible open weights." Mistral's Leanstral 1.5 is open-sourced under Apache-2.0, offered via a free API, saturates miniF2F, solves 587/672 on PutnamBench, and found 5 previously unreported bugs across 57 repositories—this is one of the few reproducible AlphaProof-level engines, directly addressing the community's long-standing dissatisfaction with "benchmark score-chasing that is not reproducible." Meanwhile, Axiom Math's PrimeGapsLib formalizes the Maynard sieve method and the Polymath8b result on prime gaps of 246 into a reusable library, accompanied by a comparator formalization challenge for independent verification.
At the methodological level, several works this issue push "faithfulness" and "diagnostic resolution" toward operability. FaithSieve uses Lean as a structured evidence source gated by semantic alignment to locate the first error in natural language proofs; MathForm integrates knowledge retrieval and verification-guided iterative refinement into a closed-loop automated formalization data pipeline, quantifying the 31% contribution of subsequent refinement rounds to data volume; MathAdv uses component-level diagnostics to distinguish knowledge, reasoning, formalization, and robustness failures.
Community and Updates
- Lean kernel soundness bug hunt: The postmortem report documents that an internal OpenAI model found a reference counting overflow and a defect in an old GMP version that could construct a proof of
False; Lean v4.33.1 fixes all issues, and plans to introduce thelake checkmulti-kernel verification command in v4.35.0. de Moura explicitly treats AI-generated proofs as potentially malicious input. - Open-weight proof engine: Leanstral 1.5 is open-sourced under Apache-2.0 (119B total parameters, 6B active), saturates miniF2F, scores 587/672 on PutnamBench, and found 5 previously unreported bugs in real repositories, with a free API available.
- Formalization milestone for prime gaps of 246: PrimeGapsLib formalizes the Maynard sieve method and the Polymath8b bound of 246 (assuming the Bombieri–Vinogradov theorem), accompanied by a comparator formalization challenge; Axiom Math's report documents this multi-agent collaboration process.
- LLM formalization of stochastic homogenization: Scott Armstrong and Tuomo Kuusi report on their blog the first Lean formalization of a quantitative stochastic homogenization theorem, approximately 449,000 lines, with no sorry and no custom axioms, all written by LLMs under human supervision.
- Community snapshot of the trust debate: A MathOverflow discussion revolves around "verifying the kernel vs. semantic correctness," citing comparator/Challenge.lean as a community response to the "mind-reading problem."
Open Questions
- The kernel bug hunt shows that AI can both generate proofs and attack the kernel: when an AI-generated proof is accepted by the official kernel but rejected by an external verifier, which layer should the community treat as the "gold standard"? Can
lake check's multi-kernel verification become the default mandate? - FaithSieve uses semantic alignment gating of Lean evidence for first-error localization, but it relies on frontier models (e.g., GPT-5.4) and the code is not yet public: can this "faithfulness gating" be lowered into a reproducible, ablatable general evaluation pipeline rather than depending on a single closed model?
- MathForm quantifies the complementary contributions of retrieval and iterative refinement to data construction (31%): can this data construction loop be combined with dependency-aware evaluation (e.g., MathAtlas's dependency graphs) to break through the bottleneck of automated formalization in graduate-level mathematics?
Papers in this issue
MathForm's retrieval-augmented, verification-guided iterative refinement framework produces an 8B model that outperforms 32B baselines, achieving 72.37% average semantic consistency on autoformalization benchmarks.
Editor's noteMathForm's increment lies in integrating Mathlib knowledge retrieval and verification-guided iterative refinement into a closed-loop automated formalization data pipeline, and explicitly quantifying the contribution of subsequent refinement rounds to data volume (31%), separating the gains of retrieval and feedback via controlled ablations. Compared with prior retrieval- or feedback-based works (such as DRIFT, ReForm), its core distinction is treating both as complementary components of a data construction pipeline rather than using them only at inference time or for single-round generation. The constructed FormalVerse dataset (approximately 367,000 verified samples) and the significant improvement of an 8B model on FATE-H/X validate the critical role of data quality for semantic faithfulness; code and data are public, making this a must-read for those working on automated formalization data construction.
FaithSieve improves first-error localization in LLM proofs by decomposing steps into local reasoning units and gating Lean verification through semantic faithfulness scoring, achieving 81.43% exact accuracy on Olympiad problems.
Editor's noteFaithSieve introduces a Lean-assisted framework for locating the first error in natural language proofs, handling both types of mismatch: locality (decomposing coarse-grained steps into EdgeUnits of the proof state tree) and semantic faithfulness (gating formal evidence with semantic alignment scores). Its substantive increment over Pistis from the previous issue (#2) is that Pistis enforces faithfulness in formalization but does not use it for proof error localization, whereas FaithSieve systematically uses type-checked obligations and faithfulness-gated formal evaluation agents for fine-grained proof auditing—Lean is not used as a direct judge of the whole proof, but as a structured evidence source gated by semantic alignment. The ProofLoc dataset and ablations clearly separate the contributions of local decomposition and semantic gating, providing an actionable complement connecting LLM mathematical reasoning with formal verification.
This paper presents a complete Lean 4 formalization of "The Set of Primes is Supernatural," proving all 89 experimental table rows and all theorems except the central conjecture, which remains deliberately open.
Editor's noteThis work provides a complete, sorry-free Lean 4 formalization of Mayeux's conjecture that "the set of primes is supernatural": every definition, example, remark, numbered result, and experimental table row in the paper has a machine-checked counterpart, and the central conjecture is precisely stated as a named open problem, with extensions to Knuth arrows, factorial, and truncated subtraction, using kernel-verified Lucas certificates for large primality assertions. Compared with benchmarks such as MathAtlas and Formal Conjectures that only cover statements, it provides a self-contained, kernel-verifiable open proof target through exhaustive coverage of a single paper, making it an ideal artifact for testing proof search systems.
MathAdv reveals formalization, not mathematical knowledge, is the primary bottleneck in theorem proving, with all models scoring zero on topology.
Editor's noteMathAdv's increment lies in unifying diagnostic component evaluation (direct answering, multiple choice, equivalent transformation) with Lean 4 theorem proving in the same benchmark, covering 13 undergraduate/graduate mathematics areas (including topology, Fourier analysis, functional analysis, and other areas not adequately covered by previous benchmarks), and systematically quantifying for the first time the differing impact of natural language prompting on general models versus proof-specialized models (prompting improves general models but harms Goedel-Prover). Compared with FormalMath and PutnamBench, its core novelty is providing component-level diagnostics to distinguish knowledge, reasoning, formalization, and robustness failures, rather than only reporting aggregate proof accuracy. Code and data are public; however, the scale is small (321 problems), and some conclusions are based on small samples, so it is advisable to interpret cautiously alongside the ablation details.
LLM failures in research-level math stem primarily from unjustified load-bearing assertions presented as background knowledge, not hallucinated citations, and current RAG mitigations fail to address this.
Editor's noteThis work provides a systematic taxonomy of four failure modes in LLM-generated research-level proofs, and empirically shows that premise smuggling (F2) dominates citation fabrication (F1)—none of the eight proofs contained a confirmed fabricated citation, but every one contained at least one load-bearing claim asserted with wording like "basic result" or "standard argument" without any proof or citation. This directly challenges the assumption that retrieval-augmented generation (RAG) is the primary mitigation, and introduces a premise audit tool with 100% precision and 50% recall that distinguishes explicit from implicit smuggling. For those designing inference-time verification pipelines rather than post-hoc detection, this is a more actionable diagnostic framework than surface pattern matching.
Codex autoformalized π₃(S²) ≅ ℤ in agda-unimath, but success hinged on translating existing human Coq-HoTT proofs, not independent discovery.
Editor's noteThis is the first recorded case study of an LLM coding agent (Codex) automatically formalizing a substantive homotopy type theory result (π₃(S²)≅ℤ) in the Agda/agda-unimath ecosystem. Its increment lies in showing that cross-library migration (from Coq-HoTT to agda-unimath) is a key success factor, and honestly quantifying the unreliability of the Agda MCP server (290 misleading calls out of 711) and the human prompting bottleneck. Although the target (HoTT in Agda) deviates from the Lean 4 mainstream, the complete session logs and code are public, offering actionable failure-mode insights for anyone building agentic proof pipelines.
