Summary (Overview)

• Problem addressed: Lean verifies that a formal proof establishes its stated proposition, but does not verify that the formal proposition faithfully expresses the mathematical claim in a manuscript—creating a "semantic gap" in formalization projects.
• Core contribution: MechAlign, a framework for project-level semantic alignment review that combines formal dependency extraction (LeanTrace) with LLM-based assessment to evaluate whether a formal statement expresses its informal claim.
• Key tool: LeanTrace constructs a statement dependency graph from elaborated Lean declarations, retaining definition bodies and structure constraints while excluding proof bodies and stopping at an explicit library boundary.
• Case study finding: A hyperbolic-group case demonstrates how dependency inspection localizes a missing two-dimensionality constraint relative to the manuscript, consistent with the upstream declaration of formalization scope.
• Benchmark resource: LeanReviewBench comprises 501 fixed claim–statement–context triples from OpenAI Math (201), Fermat's Last Theorem (200), and Kakeya (100), enabling controlled comparisons of review strategies.

Introduction and Theoretical Foundation

The research addresses a fundamental gap in automated theorem proving with Lean:

Lean checks that a formal proof establishes its stated proposition under the declared assumptions, but it does not check whether that proposition faithfully expresses the mathematical claim in the manuscript.

The semantic alignment question: Does the statement proved in the Lean project faithfully express the mathematical claim made in the manuscript?

The key insight is that in a Lean project, the meaning of a formal statement is determined not only by the main theorem declaration but also by the definitions and constraints it refers to. A theorem stated using a predicate defined within the project may appear to match the manuscript, even though the predicate encodes additional assumptions or a weaker conclusion. Interpreting the predicate requires tracing its dependencies.

Three review strategies identified:

1. Statement-only review: Sees the main Lean declaration but cannot inspect supporting declarations.
2. Full-project review: Provides full project access but leaves the reviewer to locate and connect relevant evidence.
3. Dependency-guided review (proposed): Organizes declarations around the selected result to support evidence gathering and mathematical assessment.

Related work context: The paper builds on advances in autoformalization (Herald, SAIR-Comb, MASA, LeanMarathon, MechMath), evaluation metrics for faithfulness (FormalAlign, Human Equivalence Benchmark, ProofNetVerif, MA-Align), and semantic alignment evaluation (FormalRx, FaithAlign).

Methodology

Task Definition

For a selected review target in a Lean project, let $I_t$ denote the supplied informal mathematical claim and $F_t$ the corresponding formal statement. A review instance is defined as:

$$x = (I_t, F_t, \mathcal{C}).$$

The context $\mathcal{C}$ is the dependency closure of $F_t$ relative to the extraction policy and library boundary:

$$\begin{array}{c} \mathcal{C}^{(0)} = \mathrm{Dep}(F_t), \\ \mathcal{C}^{(k+1)} = \mathcal{C}^{(k)} \cup \bigcup_{d \in \mathcal{C}^{(k)}} \mathrm{Dep}(d), \\ \mathcal{C} = \bigcup_{k \geq 0} \mathcal{C}^{(k)}. \end{array}$$

The assessment assigns each instance a label:

$$y(x) \in \{\text{aligned, misaligned, undetermined}\}.$$

LeanTrace Extraction Tool

LeanTrace constructs a statement dependency graph from an elaborated Lean project with these key policies:

• Starting from the elaborated type of the selected theorem declaration, iteratively collects dependencies through declaration types and non-proof definition bodies.
• Proof bodies are excluded—only types contribute for theorems and proof-valued declarations.
• For inductive types, structures, and classes, follows constructors and traverses constructor types, capturing dependencies from field types and constraints even without explicit field projections.
• Library boundary: Stops at Mathlib and Lean's core libraries, retaining names and types of referenced declarations as boundary nodes without traversing their dependencies.

MechAlign Reviewer

The Reviewer assesses alignment across six dimensions:

1. Objects and domains (O&D): Formal types represent intended mathematical objects and ranges.
2. Hypotheses (HYP): Missing, additional, or altered assumptions.
3. Quantifiers (QUA): Scope, order, and dependence on previously introduced variables.
4. Constants and bounds (C&B): Numerical factors, inequalities, parameter restrictions.
5. Conclusions (CON): Formal statement covers the claimed result.
6. Definition semantics (DEF): Underlying constructions and predicates express intended meanings.

A deterministic evidence check verifies that quotations occur in the supplied sources; it does not independently validate the informal specification.

Empirical Validation / Results

OpenAI Math Review

The study inspected 201 theorems across 173 projects in openai/math, comparing informal descriptions in Lean comments with formal statements using extracted dependency graphs.

Case Study: Missing Dimensional Constraint

The main theorem of the HyperbolicObstruction manuscript requires a finite connected two-dimensional aspherical simplicial complex with a linear disk-filling bound and a fundamental group admitting no geometric CAT(0) action.

The selected Lean result has the signature:

theorem main : MainStatement.{u}

A statement-only reviewer cannot determine from this declaration whether the witness is required to be two-dimensional. Dependency inspection reveals:

def MainStatement : Prop :=
    ∃ K : FiniteComplex, ∃ x : K.Carrier, ∃ C : R,
    -- Remaining conditions omitted here.

Inspecting the retained witness type:

structure FiniteComplex where
n : N
complex : AbstractSimplicialComplex (Fin n)

Here $n$ specifies the size of the finite vertex index type; it does not specify the dimension of the complex. Neither field restricts simplex size to encode two-dimensionality.

The disk move constructor restricts individual moves to triangular faces but does not prohibit higher-dimensional simplices:

| triangle (1 r) (a b c) (h : {a, b, c} ∈ K.complex.faces)
(hne : ({a, b, c} : Finset K.Vertex).card = 3) :
DiskMove K (1 ++ [a, b, c] ++ r) (1 ++ [a, c] ++ r) 1

Key quantitative finding: LeanTrace retained 24 of 4,550 source declarations (0.53%) in the upstream main theorem's project import closure (417 files), providing a compact context for review.

Contrast with full-project access: An exploratory review using Astra in Codex with full-project access incorrectly reported alignment with the informal claim, overlooking the omission.

LeanReviewBench Statistics

• FLT's first quartile is zero: 64 tasks have no internal dependencies beyond the root, but all retain external-library boundary nodes.
• The largest OpenAI context contains 1,041 internal declarations.
• Counts exclude the main statement and library-boundary declarations.

Theoretical and Practical Implications

• Evidence organization matters: The case study demonstrates that how evidence is organized (dependency-guided vs. full-project) materially affects review outcomes, with full-project access leading to errors that dependency-guided review avoids.
• Compact contexts enable review: Retaining only 0.53% of project declarations (24 of 4,550) while preserving essential semantic information suggests that targeted dependency extraction can make alignment review tractable at scale.
• Scalability: The framework supports review of large developments (FLT, Kakeya) by decomposing them into individual theorem-level review instances.
• Provenance awareness: The paper carefully distinguishes between descriptions derived from manuscripts (independently verified) vs. Lean-derived descriptions (supporting consistency checks but not establishing manuscript fidelity).
• Controlled comparison design: The three-strategy comparison (statement-only, full-project, dependency-guided) provides a reproducible methodology for evaluating the value of evidence organization in semantic alignment.

Conclusion

MechAlign provides a framework for project-level semantic alignment review in mathematical formalization:

• LeanTrace extracts and organizes statement dependencies, enabling reviewers to investigate semantic discrepancies and cite supporting evidence.
• Preliminary OpenAI Math review and the HyperbolicObstruction case illustrate how dependency inspection localizes missing constraints.
• LeanReviewBench provides 501 fixed review instances from OpenAI Math, Fermat's Last Theorem, and Kakeya for reproducible studies.

Limitations acknowledged:

• Extracted context excludes proof bodies and stops at the external-library boundary, potentially leaving essential interpretation evidence unavailable.
• Alignment review does not certify original proofs or axiomatic assumptions.
• Some informal descriptions are Lean-derived; reference labels remain provisional.
• Shared developments and possible training exposure limit generalization claims.

Future work:

• Validate descriptions against independent mathematical sources.
• Obtain human-adjudicated judgments.
• Complete controlled comparisons of statement-only, full-project, and dependency-guided reviews to assess judgment quality, evidence localization, and cost.