Builds LeanTrace, which extracts statement dependency graphs from elaborated Lean 4 declarations, enabling LLM review of semantic alignment and a benchmark from Lean projects.
Abstract
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.
Problem
Lean checks that a proof establishes its stated proposition. It does not check whether that formal statement faithfully expresses the informal claim in a manuscript. Judging this correspondence requires interpreting project-specific definitions and constraints scattered across large developments.
Approach
MechAlign combines formal dependency extraction with LLM-based review. Its extractor, LeanTrace, starts from a theorem's elaborated type and follows declaration types and non-proof definition bodies, including constructors and structure constraints. It excludes proofs and stops at an explicit library boundary. A Reviewer agent navigates the resulting graph to label each target aligned, misaligned, or undetermined, citing localized evidence.
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.
Results
A preliminary review covered 201 main results from 173 OpenAI Math Lean projects. A hyperbolic-group case shows dependency inspection localizing a missing dimensional constraint relative to the manuscript. LeanReviewBench provides 501 fixed claim-statement-context triples from OpenAI Math (201), Fermat's Last Theorem (200), and Kakeya (100). Controlled comparisons of review strategies are still planned.
Collection
Def.
Theorem
Abbrev.
Total
OpenAI
3,382
2,830
1,594
8,767
FLT
1,039
1,604
385
3,404
Kakeya
900
700
730
2,914
Retained declarations by kind per collection (subset of columns)
