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

• Lean checks that a proof establishes its stated proposition under declared assumptions, not that the proposition faithfully expresses the manuscript’s claim.Source: §1 · p. 1
• A formal result’s meaning depends on its main declaration and the definitions and constraints it references, which can encode hidden assumptions or weaker conclusions.Source: §1 · p. 1
• MechAlign combines LeanTrace’s dependency graph with an LLM reviewer that investigates alignment and reports discrepancies with supporting evidence.LeanTrace follows elaborated declaration types and non-proof definition bodies, retains structural constraints, and stops at an explicit library boundary.Source: §1 · p. 2
• The preliminary application examines 201 main results from 173 OpenAI Math projects, and LeanReviewBench provides 501 review instances across OpenAI Math, Fermat’s Last Theorem, and Kakeya.The benchmark supports controlled comparison of statement-only, full-project, and dependency-guided review.Source: §1 · p. 2
• The project-level review task assesses whether a selected formal result expresses its supplied informal claim through the declarations that determine its meaning.Source: §1 · p. 2

• Autoformalization work includes natural-language annotation and translation, compiler-feedback methods, expert-guided refinement, and agent workflows for formalization and repair [10] [22].These advances increase the need to review completed formalizations.Source: §2 · p. 2
• Faithfulness evaluation resources include synthetic misalignments, human-labeled pairs, annotated examples, and graduate-level formalizations labeled for semantic alignment [14].Source: §2 · p. 2
• Recent alignment evaluations examine error localization, phrase-level correspondence, and whether evaluators recognize insufficient context [19] [4].Source: §2 · p. 2
• MechAlign studies evidence acquisition by extracting selected-result dependencies and having a reviewer inspect the resulting graph for semantic discrepancies.Its full-project comparison is intended to test evidence organization without presuming existing approaches fail.Source: §2 · p. 3

3.1 Task Definition

• Project-level review assesses whether a formal statement expresses an informal claim using the declarations that determine its meaning.Judgments are aligned, misaligned, or undetermined; insufficient evidence is reserved for human review.Source: §3.1 · p. 3

3.2 LeanTrace

• LeanTrace builds a dependency graph from elaborated declarations, following types and non-proof bodies while excluding proof bodies and stopping at library boundaries.It also follows constructors of inductive types, structures, and classes to capture constraints introduced by their fields.Source: §3.2 · pp. 3–4

3.3 MechAlign

• MechAlign combines a Selector, LeanTrace, and a Reviewer that assesses alignment using the supplied claim, formal statement, and extracted context.The Selector can use supplied mappings or search manuscript and Lean sources, recording the claim’s source.Source: §3.3 · p. 4, Figure 1 · p. 4
• The Reviewer supports its three-way judgment with explanations and quotations, but the assessment is not a formal guarantee of semantic equivalence or manuscript fidelity.A deterministic check verifies that quotations occur in supplied sources, not that the informal specification is independently valid.Source: §3.3 · p. 4

4.1 Review Setting and Compared Strategies

• Controlled comparisons of statement-only, full-project, and LeanTrace-assisted review are designed, but their results remain to be completed.The planned comparison holds the model, claim, root, and source revision fixed.Source: §4 · p. 4, §4.1 · p. 5

4.2 Case Study: A Missing Dimensional Constraint

• LeanTrace’s Figure 2 context retains 24 of 4,550 source declarations, with selected paths tracing the witness and disk-filling definitions relevant to the review.The case uses those dependencies to distinguish a triangular disk move from a constraint that would prohibit higher-dimensional simplices.Source: Figure 2 · p. 5, §4.2 · p. 6

4.1 Review Setting and Compared Strategies

• LeanTrace inspected 201 theorems across 173 OpenAI Math projects against existing Lean comments, with paper excerpts and project context used as supplementary evidence.The descriptions were not independently validated against the manuscripts, so manuscript-fidelity findings remain candidates pending verification.Source: §4.1 · p. 5

4.2 Case Study: A Missing Dimensional Constraint

• The selected proposition does not explicitly require its witness to be two-dimensional, although the manuscript requires a finite connected two-dimensional aspherical simplicial complex.The retained FiniteComplex fields specify a finite vertex index and an abstract simplicial complex, but do not restrict simplex size.Source: §4.2 · pp. 5–6

5 LeanReviewBench: A Reusable Review Resource

• Each benchmark instance is a fixed claim-statement-context triple, with target selection and LeanTrace extraction completed before reviewers assess semantic judgment.The correspondence and extracted context remain fixed across systems.Source: §5 · p. 6
• The 501 tasks comprise 201 OpenAI Math results, 200 Fermat’s Last Theorem targets, and 100 Kakeya targets.The latter collections include intermediate results and supporting mathematical infrastructure, not only main theorems.Source: §5 · p. 6
• OpenAI Math contexts have a median of 17 internal declarations (middle half 7–38; maximum 1,041), versus medians of 5 for FLT and 19 for Kakeya.Counts exclude the main statement and external-library boundary nodes; 64 FLT tasks have no internal dependencies beyond the root.Source: §5 · p. 7, Figure 3 · p. 7
• Evaluation records aligned, misaligned, or undetermined verdicts with localized evidence, while reporting judgment accuracy, answer coverage, execution success, model usage, latency, and evidence-acquisition cost.Reference labels are provisional model judgments; human-adjudicated accuracy remains to be established.Source: §5 · p. 7

6 Discussion and Conclusion

• MechAlign uses LeanTrace to organize dependencies so a reviewer can investigate semantic discrepancies and cite supporting evidence.The preliminary OpenAI Math review and HyperbolicObstruction case illustrate the process; LeanReviewBench supplies 501 fixed instances across three collections.Source: §6 · p. 7
• Extracted contexts omit proof bodies and stop at the external-library boundary, potentially leaving interpretation evidence unavailable; review does not certify original proofs or axiomatic assumptions.Lean-derived descriptions, provisional labels, shared developments, and possible training exposure also limit generalization claims.Source: §6 · pp. 7–8

A Source Revisions and Interpretation Environment

• The released project metadata pins upstream revisions and records a shared Lean and Mathlib interpretation environment.The appendix identifies specific source revisions and environment versions.Source: A Source Revisions and Interpretation… · p. 10

B HyperbolicObstruction: Complete Statement Context

• The informal witness is a finite connected two-dimensional aspherical simplicial complex with a linear disk-filling bound and a fundamental group admitting no geometric action on a proper complete CAT(0) space.Every edge loop of length ℓ in the universal cover bounds a disk diagram with at most Cℓ triangular faces.Source: B HyperbolicObstruction: Complete… · p. 10
• The stated consequences include a word-hyperbolic fundamental group and no homotopy-equivalent finite simplicial model with a compatible locally CAT(−1) geodesic length metric.The passage also rules out a locally CAT(0) geodesic length metric inducing the given topology on such a model.Source: B HyperbolicObstruction: Complete… · p. 10
• The informal claim requires a two-dimensional witness, but the selected formal statement has no explicit dimension constraint.The review presents this as a discrepancy between the manuscript claim and the formalization.Source: B HyperbolicObstruction: Complete… · p. 12

C LeanReviewBench: Construction and Detailed Statistics

• The appendix says LeanReviewBench target selection and LeanTrace extraction precede evaluation, which uses frozen claim-statement-context triples without repeating those stages.The appendix passage concerns the construction and release of the review triples.Source: C LeanReviewBench: Construction and… · p. 12

C.1 Target Selection and Coverage

• The inventory contains 201 OpenAI Math main-result targets, 200 Fermat’s Last Theorem targets, and 100 Kakeya targets.FLT and Kakeya selections use individual theorem declarations, including intermediate results and supporting infrastructure.Source: §C.1 · p. 12
• Table 1 reports selected FLT and Kakeya review targets by area, including the listed FLT area counts and total of 200.The table’s listed FLT area counts sum to the 200-target total.Source: Table 1 · p. 13, §C.1 · p. 13
• Table 2 reports internal dependency declaration occurrences by recorded kind, excluding main statements and external-library boundary nodes.Occurrences should not be treated as unique definitions because shared declarations can recur across tasks.Source: Table 2 · p. 13
• FLT targets span eight areas, from elementary number theory to modularity lifting, while Kakeya targets cover geometric and dimension-bound topics.The selected areas document coverage and are not a representative sample of Lean mathematics.Source: §C.1 · p. 13

C.2 Review Instance Construction

• Pinned source revisions and interpretation settings define each extraction environment; proof bodies are placeholders while definitions, structure constraints, namespaces, and notation are retained.LeanTrace extracts the selected statement and dependency context under the stated policy, including the external-library boundary.Source: §C.2 · p. 13
• Explicit mappings associate each of 501 targets with a nonempty main description and any scope qualifications, while recording description origins.The 200 FLT descriptions come from upstream HTML; Kakeya descriptions comprise 82 upstream comments and 18 marked model-authored paraphrases, with explicit StickyFrostman hypotheses preserved for all six affected targets.Source: §C.2 · p. 13
• For 32 Kakeya targets, page-linked paper context is background rather than an equivalence claim, and agreement with Lean-derived descriptions is only a supplied-text consistency test.Main Lemma 1 has no exponent loss, whereas the selected Lean result requires β < γ; source-grounded alignment requires a reviewed independent specification.Source: §C.2 · p. 13
• Frozen task packages include Lean artifacts and provenance-rich informal records, while exported evaluation inputs omit description origins, review status, preparation metadata, and reference labels.Evaluation inputs are exported without reparsing Lean files or rebuilding the extraction environment.Source: §C.2 · pp. 13–14

C.3 Context Statistics and Release Validation

• Figure 3(b) summarizes per-task internal dependency counts, excluding main statements and external-library boundary nodes, with quartile boxes, median lines, and full-range whiskers.The counts combine the selected definition/structure inventory with remaining internal declarations.Source: §C.3 · p. 14
• 64 of 200 FLT tasks (32%) have no internal dependency declarations beyond the root, yet each retains 4–130 external-library boundary nodes.A zero internal count does not imply an empty context, and a boundary type may be insufficient when a judgment requires the library implementation.Source: §C.3 · p. 14
• The selected definition/structure inventory totals 5,823 occurrences: 3,477 for OpenAI, 1,155 for FLT, and 1,191 for Kakeya.These are not counts of all internal declarations or unique definitions; shared declarations may occur across tasks, and Table 2 reports retained internal declarations by kind.Source: §C.3 · p. 14
• Compilation, archived closure replay, and release validation check artifacts and extraction records, but do not certify proof correctness or semantic alignment.The checks cover statement types, retained definition bodies, file hashes, target inventories, mappings, graph consistency, and reference/input bindings.Source: §C.3 · p. 14
• All 501 released model judgments are provisional, with descriptions and semantic references awaiting human adjudication.Repeated evaluations should record task and model identities, configuration, budgets, and outcomes; held-out splits must account for shared developments and overlapping dependencies.Source: §C.3 · p. 14

C.4 Code and Data Availability

• The MechAlign implementation, LeanTrace, LeanReviewBench data, and evaluation tools are slated for public release upon publication.The benchmark repository includes frozen review instances, provenance records, provisional reference labels, and evaluation tools.Source: §C.4 · p. 14
• The released system supports supplied claim–declaration mappings, fresh dependency extraction, and six-dimension review with quotation checks.Benchmark evaluation instead uses frozen supplied claims and dependency contexts without repeating selection or extraction.Source: §C.4 · p. 14
• Original-paper locating is limited to pinned OpenAI TeX sources and archived target mappings; general manuscript search and automatic target selection are not implemented.The MechAlign adapter assesses the main claim and encodes undetermined as insufficient_information in protocol submissions.Source: §C.4 · p. 14