MechAlign checks math claim matches formal proof across projects
MechAlign: Evaluating Semantic Alignment at the Project Level in Mathematical Formalization
Computation and Language
Summary
Formal proof software can tell if a proof is correct but can't say if the formalized statement really matches the math claim in a paper. The authors created MechAlign to review this match by tracing all the linked formal math parts and using AI to spot differences. They tested it on hundreds of math formalization projects, finding cases where details in the formal proof didn't align with the paper. They also built a benchmark dataset to help compare future tools for checking this kind of alignment.
What this means in practice
- •For software verification teams: Identify mismatches between formal proofs and their intended mathematical claims across large verification projects.
- •For automated reasoning tool developers: Use the LeanReviewBench dataset to test and improve project-level semantic alignment evaluations in theorem proving tools.
Authors
Hao Shen, Ruichen Qiu, Lihong Zhi, Xiao-Shan Gao
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.