# MechAlign: Evaluating Semantic Alignment at the Project Level in Mathematical Formalization

> MechAlign uses dependency-guided review with LeanTrace to localize semantic gaps between formal Lean statements and informal mathematical claims, outperforming full-project access.

- **Source:** [arXiv](https://arxiv.org/abs/2610.35269)
- **Published:** 2026-10-31
- **Permalink:** https://picx.dev/p/O3uIri
- **Whiteboard:** https://picx.dev/p/O3uIri/image

## Summary

## 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:

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

Inspecting the retained witness type:

```txt
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:

```javascript
| 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

| Collection | Tasks | Median Internal Dependencies | Interquartile Range |
|---|---|---|---|
| OpenAI Math | 201 | 17 | 7–38 |
| Fermat's Last Theorem | 200 | 5 | 0–(upper quartile) |
| Kakeya | 100 | 19 | —41.25 (upper quartile) |

- 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.

---

_Markdown view of https://picx.dev/p/O3uIri, served by PicX — AI-generated visual whiteboard summaries of research papers._