When Lean Passes but Semantics Are Lost: The Fidelity Crisis of Autoformalization
Highlights of This Issue
The main thread of this issue is that "the verification boundary itself becomes the object under examination." Last issue's Collatz incident revealed that a kernel bug could deceive both checkers simultaneously; this issue turns the spotlight on a more fundamental problem: even if the Lean kernel is completely correct, autoformalization itself may lose semantics in translation. Navier-Stokes lost in translation uses OpenAI's announced Navier-Stokes finite-time blow-up proof as a case study, pointing out specific mistranslations between its Lean formalization and the natural language paper, and proves that "resolving ambiguity in mathematical natural language" lies at infinite height in the Solvability Complexity Index (SCI) hierarchy—strictly harder than the halting problem. Meanwhile, the community's Zulip audit of OpenAI's 722 AI-generated math manuscripts found 76 family-level claims exaggerating Lean coverage, while the independent recheck of ζ(s)≠0 showcased a positive case—two independent kernels both accepted the proof of no zeros in the 7/8 half-plane. Together, these two sides turn "what does machine-verified proof mean" from a philosophical question into an operational research agenda.
On the proof search side, several works this issue advance the "goal" from "finding any correct proof" to "finding a correct proof under user-specified objectives." LEVER turns computational cost, proof length, and topic purity into programmable objectives on AND/OR proof graphs and optimizes them during search; AIProver for the first time uses semantic alignment as a training signal rather than a post-hoc filter; Bolzano pushes proof search to fully automatic open-problem solving. Together, these works point in one direction: proof search is evolving from a "solver" into a "tunable proof engineer."
Community and Updates
- OpenAI releases 722 AI-generated math manuscripts: On October 6, OpenAI released the openai/math repository containing 722 manuscripts and 372 result families, of which 235 families include Lean formalizations and 405 Comparator challenges. The community immediately engaged in intensive auditing: the Zulip audit found 76 family-level claims exaggerating Lean coverage, while the independent recheck of ζ(s)≠0 used two independent kernels, Lean and nanoda, to accept the proof of no zeros in the 7/8 half-plane.
- Mathlib proof graph research: Mathlib as a Geometry of Mathematics constructs a theorem dependency graph with 138k nodes/309k edges and a state-tactic hypergraph from LeanDojo trajectories, finding heavy-tailed degree distributions, 240 Louvain communities, and local structure predicting proof length (R²=0.555), but literal goal matching recovers only 2.5% of dependency edges—suggesting discovery tools need normalized proof state matching.
- Mathlib Set type refactoring: PR #41506 refactors Set from a reducible function to a single-field structure, partially AI-assisted but human-reviewed, an infrastructure change affecting all subsequent formalization work.
Open Questions
- The Navier-Stokes paper proves that "semantically faithful autoformalization" lies at infinite height in the SCI hierarchy (SCI=∞)—does this mean any autoformalization pipeline cannot in principle guarantee fidelity, or does this lower bound only apply to "unrestricted" natural language input, which can be bypassed for restricted mathematical texts (e.g., structured statements)?
- AIProver uses semantic alignment as a training signal, but its validation set's semantic correctness relies on an LLM judge (4-way check)—when "semantic correctness" itself requires LLM judgment, do the training signal and evaluation signal constitute circular reasoning? Can the bidirectional implication check from ShadowBench in Issue 4 replace the LLM judge?
- LEVER incorporates proof quality objectives (length, topic purity) into search goals, but the measure of "topic purity" depends on the definition of "topic"—when proofs borrow tools across domains, is the purity measure too subjective? Can the interestingness measure from Issue 7 (proof length/description length ratio) serve as a more objective quality objective?
- Bolzano's verifier is an LLM rather than a formal kernel, and its "solved" open problems lack machine verification—when open problems themselves have no formal statements, what does "solving" mean? Can the zero-contamination open conjectures from Formal Conjectures in Issue 1 serve as verification carriers for Bolzano-type systems?
Papers in this issue
Autoformalising natural-language proofs into Lean does not validate the original argument, because semantic faithfulness is provably harder than the Halting problem and OpenAI's Navier–Stokes formalisation contains concrete mistranslations.
Editor's noteThis paper uses OpenAI's announced Navier-Stokes finite-time blow-up proof as a case study, pointing out specific mistranslations between its Lean formalization and the natural language paper (e.g., m+4 vs. m+5 order derivatives, pressure-flux bound differences), and proves that "resolving ambiguity in mathematical natural language" lies at infinite height in the Solvability Complexity Index (SCI) hierarchy (SCI=∞), strictly harder than the halting problem. This is the most powerful theoretical rebuttal to the belief that "Lean verification implies proof correctness," and is essential reading for any pipeline that treats Lean verification as a trust signal for AI-generated proofs.
AIPROVER co-evolves an open-weight model and its tool harness via certificate-driven search, achieving 36.7% semantic correctness—a tenfold gain over prior open-weight systems—and a new accuracy–cost Pareto frontier.
Editor's noteAIProver for the first time uses semantic alignment (SAM contrastive learning) as a training signal rather than a post-hoc filter, using a graded reward ladder (type correctness → completeness → semantic correctness → length fidelity) to drive alternating evolution of the model and tool control flow. Compared to Growing an Agent/Prover Interface from Issue 8 (evolving tool design), its increment lies in internalizing NL-FL equivalence into the model representation and using semantic correctness rewards to drive HarnessEvolve's evolutionary search. The systematic comparison of LoCoBench (58.9k instances, including the first large-scale Mizar-to-Lean test) with 39 baselines has direct value for evaluating research-level autoformalization.
LEVER makes proof quality objectives programmable during LLM proof search, cutting cost 34% while raising solve rates from 80% to 96% on PutnamBench.
Editor's noteLEVER turns "objectives for correct proofs" into programmable objectives and optimizes them during search—combining achieved objective values with open subgoal predictions on AND/OR proof graphs, allowing objectives like computational cost, proof length, and topic purity to guide search before proof completion. Compared to LEAP from Issue 7 (AND-OR DAG memoized search), its increment lies in advancing the goal from "finding any correct proof" to "finding a correct proof under user-specified objectives," improving the solve rate on PutnamBench from 80% to 96% at 34% lower cost.
Bolzano, an open-source multi-agent proof-search system, autonomously solved 214 open problems from 3,800 arXiv and STOC papers, including four author-confirmed results.
Editor's noteBolzano upgrades "expert-guided multi-agent proof search" to a fully automatic open-problem solving loop without problem-specific human guidance, solving about 200 open problems in 3,800 attempts, with four problems from STOC 2026 papers confirmed by the original authors. Compared to Magenta from Issue 5 (closed-loop proof search), its increment lies in the end-to-end automated pipeline of "open problem extraction → automated parallel exploration → structured audit → original author confirmation," and it systematically quantifies for the first time the bottleneck of extracting problems from large-scale paper collections. Note that its verifier is an LLM rather than a formal kernel, so results should be treated as relative signals.
- Editor's note
NanoProof is the first fully open-source and reproducible factorized execution-guided Lean 4 prover, releasing the structured proof tree dataset LeanTree (92,927 trees), extraction tools, training pipeline, and weights, making AlphaProof/HTPS-type systems end-to-end reproducible for the first time. Its incremental verification strategy (checking only new assignments) fixes the REPL false positive/false negative issues, and is of practical value to any researcher doing factorized proof search or training data construction.
LeanPlan is the first system to machine-check LLM-generated heuristics for admissibility via Lean 4, solving 281 IPC 2023 tasks—27.1% more than the state-of-the-art optimal planner Scorpion.
Editor's noteLeanPlan is the first planning system that uses Lean 4 to machine-verify the admissibility of LLM-generated heuristic functions: an agentic loop uses planner feedback to iteratively improve domain-specific heuristics and their admissibility proofs, with the Lean kernel responsible for verification. On ten IPC 2023 domains, the planner with machine-verified optimality guarantees solves 27.1% more tasks than the optimal planner Scorpion without guarantees. Although the domain is classical planning rather than mathematical theorem proving, its methodology of "agent-generated code + proofs, kernel-verified" has direct relevance to autoformalization.
Self-advertisement, where each method proposes its own target, action, and conditions, beats similarity-based reranking for theorem-proving method selection, doubling proof success rates on Putnam.
Editor's noteThis paper advances method selection from "relevance retrieval" to "applicability awareness": each candidate method contract generates a problem-specific usage proposal (goal, action, required conditions) before ranking, and formally proves the candidate pool ceiling for the two-stage similarity + reranking selector. Compared to MathForm's knowledge retrieval from Issue 3 and OProver's unified retrieval framework from Issue 2, its increment lies in advancing method selection from relevance retrieval to applicability awareness. On Putnam 2015-2025, it achieves hit@5 of 95.0% (strongest reranking baseline: 84.2%), and in a fixed-budget proof loop, it increases the proportion of proven problems from 5.8% to 12.5%.
