Organizations: State Key Laboratory of Mathematical Sciences, Academy of Mathematics and Systems Science, Chinese Academy of Sciences, and University of Chinese Academy of Sciences.
Lean verifies that a formal proof establishes its stated proposition under declared assumptions, but does not check whether that proposition faithfully expresses the mathematical claim in a manuscript. Assessing this correspondence requires interpreting the main theorem through its project dependencies, which may be scattered throughout a large development. We introduce MechAlign, a framework for project-level semantic alignment review that combines formal dependency extraction with LLM-based assessment. Its extraction tool, LeanTrace, constructs a statement dependency graph from elaborated declarations, retaining definition bodies and structure constraints while excluding proof bodies and stopping at an explicit library boundary. The reviewer uses this context to investigate alignment and report discrepancies with localized evidence. We conduct a preliminary review of 201 main results from 173 OpenAI Math projects, using supplied informal descriptions and available paper context. A hyperbolic-group case illustrates how dependency inspection localizes a missing dimensional constraint relative to the manuscript, consistent with the upstream declaration of formalization scope. We also construct LeanReviewBench, comprising 501 fixed claim-statement-context triples from OpenAI Math, Fermat's Last Theorem, and Kakeya, with description provenance recorded. The resource supports controlled comparisons of more project-level semantic alignment evaluations.
Figures & tables
Figure 1: Overview of MechAlign. The Selector obtains the paper and formal statements, LeanTrace extracts the formal dependency context, and the Reviewer assesses alignment using both formal and paper context.
Figure 2: LeanTrace context for HyperbolicObstruction. All 24 retained source declarations are shown with selected dependency edges; dashed arrows fold paths through auxiliary or constructor nodes. Red nodes and arrows mark the path from main to FiniteComplex through the asphericity and carrier definitions, inspected to determine whether the witness type enforces the manuscript’s two-dimensionality requirement. The shaded sector in the inset represents the retained fraction: 24 of 4,550 source declarations in the main theorem’s project import closure (0.53%), counting the root in both.
Figure 3: LeanReviewBench source composition and context-size distributions. Left: shares of 501 tasks. Right: per-task internal dependency counts, combining selected definitions and other internal declarations. Boxes span the first to third quartile, thick lines mark medians, and whiskers span the minimum to maximum. The horizontal axis uses a logarithmic transformation of count plus one to display zeros and the long tail; tick labels show original counts. Main statements and external-library boundary nodes are excluded.
Appendix figures & tables2 assets
Supplementary material from the paper’s appendix.
Appendix
Table 1: Selected review targets by area in FLT and Kakeya.
Collection
Def.
Structure
Abbrev.
Class
Inductive
Constructor
Recursor
Theorem
Opaque
Total
OpenAI
3,382
260
1,594
12
67
572
49
2,830
1
8,767
FLT
1,039
149
385
39
0
188
0
1,604
0
3,404
Kakeya
900
291
730
1
0
292
0
700
0
2,914
Appendix
Table 2: Internal dependency declaration occurrences by recorded kind, excluding main statements and external-library boundary nodes.
AI-driven autoformalization of mathematics is advancing rapidly. However, the type checker of a proof assistant guarantees only the logical correctness of proofs; it does not verify whether propositions and definitions faithfully capture their intended mathematical content. Consequently, AI-generated formal proofs can exhibit semantic hallucination-passing the type checker yet failing to express the intended mathematics. We propose a human-in-the-loop approach in which human scientists and AI collaboratively produce formal proofs, with humans responsible for the semantic verification of propositions and definitions. To realize this approach, we develop Lean Atlas, a Lean 4 tool that visualizes the dependency graph of a Lean 4 project as an interactive web viewer, enabling human scientists to grasp the overall structure of a formalization efficiently. Its core feature, Lean Compass, is an algorithm that, given a selected theorem set, automatically extracts the project-specific nodes whose semantic correctness can affect those target statements, thereby reducing the candidate set for semantic review in large-scale formalizations. We further define aligned Lean code as formalization code that has undergone human semantic verification, and propose it as a quality standard for AI-generated formalizations. We evaluate the tool on six Lean 4 formalization projects with different structural characteristics; proof-heavy projects (PrimeNumberTheoremAnd, Carleson, Brownian Motion) achieved 94-99% average node reduction, a 6-theorem milestone subset of FLT achieved 59.8%, mixed PhysLib 69.0%, and definition-heavy XMSS 27.3%. Lean Atlas is available as open-source software at https://github.com/NyxFoundation/lean-atlas .
Banri Yanahama, Akiyoshi Sannai
Nyx Foundation · Kyoto University · Large Language Model Research and Development Center, National Institute of Informatics
Formal proofs in Lean 4 that pass the kernel's type checker can nonetheless vary widely in quality. We introduce ProofJudge, an agentic LLM-as-judge system that scores formal proof quality along five dimensions beyond correctness: library leverage, automation fit, structural clarity, statement quality, and Mathlib conventions. We evaluate ProofJudge on a novel dataset of 218 declarations drawn from distinct Mathlib PRs. The judge agent is grounded by tool access to the commit the PR is applied to, enabling it to query the library state when scoring. A judge is considered aligned with human preferences when it rates the version of the PR Mathlib accepted above the initial version that was sent back for revision. All six judge models evaluated recover the reviewers' preference well above chance, from 80.8% to 63.5%, and two open-weight judges reach roughly 70% at a tenth of the best judge's cost. We release the judge harness, evaluation dataset, and evaluation traces as open-source artifacts to support further research.
We introduce a novel method for verifying Lean formalizations that goes beyond LLM-judged faithfulness. Unlike most verification methods, which rely on LLMs or trained models, our method combines LLM-based semantic review with mechanical numerical and vacuity checks, providing checkable feedback and detecting errors missed by LLM judges. We apply this method, along with our Extract-Verify-Proof autoformalization pipeline, to construct the Formalized Library of Mathematical Functions (FLMF), a partial formalization of the NIST Digital Library of Mathematical Functions (DLMF). On three labeled datasets, our method achieves the lowest accepted-error rate among the evaluated methods, measured as the fraction of incorrect statements accepted by the verification method. Expert review of the results also identifies translation and source defects in existing datasets. Code available at https://github.com/annamei1/FLMF-Ch7ErrFunc-Release.git.
Anna Mei, Michael R. Douglas
Harvard University · CMSA, Harvard University and AletheAI, Inc