PaperlayerView exact revision on arXiv

Source-linked AI summary

M2F: Automated Formalization of Mathematical Literature at Scale

Zichen Wang, Wanli Ma, Zhenyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen

arXiv:2602.17016v1cs.AI

TL;DR

Large-scale mathematical autoformalization remains difficult because project dependencies and end-to-end compilation exceed snippet-level methods. M2F addresses this with two-stage, verifier-certified Lean refinement, producing a 153,853-line library from 479 pages and achieving 96% fully automatic proof success on FATE-H. The remaining failures include an inconsistent benchmark statement and two currently unsolved cases without expert lemma maps.

  • Problem

    Existing autoformalization largely handles isolated statements, while textbook- and paper-scale sources require consistent imports, namespaces, dependencies, and end-to-end project compilation.

  • Method

    M2F compiles declaration skeletons before repairing proofs under fixed signatures, accepting localized edits only when Lean feedback certifies improvement.

  • Results

    M2F produces a 153,853-LoC buildable library from 479 pages and solves 96% of FATE-H fully automatically, rising to 97% with a 31-declaration natural-language lemma map.

  • Takeaways & Limitations

    M2F demonstrates project-scale formalization with Lean verification serving both as a prover oracle and as a high-precision signal for evaluating mathematical reasoning.

  • Takeaways & Limitations

    On FATE-H, one benchmark statement was inconsistent and two cases remained unsolved without expert lemma maps.

Abstract

from arXiv · show

Automated formalization of mathematics enables mechanical verification but remains limited to isolated theorems and short snippets. Scaling to textbooks and research papers is largely unaddressed, as it requires managing cross-file dependencies, resolving imports, and ensuring that entire projects compile end-to-end. We present M2F (Math-to-Formal), the first agentic framework for end-to-end, project-scale autoformalization in Lean. The framework operates in two stages. The statement compilation stage splits the document into atomic blocks, orders them via inferred dependencies, and repairs declaration skeletons until the project compiles, allowing placeholders in proofs. The proof repair stage closes these holes under fixed signatures using goal-conditioned local edits. Throughout both stages, M2F keeps the verifier in the loop, committing edits only when toolchain feedback confirms improvement. In approximately three weeks, M2F converts long-form mathematical sources into a project-scale Lean library of 153,853 lines from 479 pages textbooks on real analysis and convex analysis, fully formalized as Lean declarations with accompanying proofs. This represents textbook-scale formalization at a pace that would typically require months or years of expert effort. On FATE-H, we achieve $96\%$ proof success (vs.\ $80\%$ for a strong baseline). Together, these results demonstrate that practical, large-scale automated formalization of mathematical literature is within reach. The full generated Lean code from our runs is available at https://github.com/optsuite/ReasBook.git.

1 Introduction

M2F frames textbook- and paper-scale autoformalization as project-level knowledge compilation and uses verifier-certified refinement across statement compilation and proof repair.

  • 1 Introduction: The two-stage system first compiles declaration skeletons with proof placeholders, then repairs proofs under fixed statement signatures using goal-conditioned local edits.Stage 1 stabilizes dependencies and elaboration before Stage 2 discharges remaining obligations.
  • 1 Introduction: M2F formulates large-scale autoformalization as compiling a buildable Lean project under a fixed environment with span-level provenance.This shifts evaluation beyond isolated snippet correctness to end-to-end project elaboration.
  • 1 Introduction: VeriRefine commits localized edits only when Lean feedback reduces elaboration errors or closes proof holes, preventing regressions during long runs.The rule is applied under verifier-normalized compute budgets.
  • 1 Introduction: 96% proof success on FATE-H makes Stage 2 state-of-the-art among the compared provers under matched statements.The result provides external validation of the verifier-in-the-loop methodology.
  • 1 Introduction: M2F scales to textbook- and paper-length sources while producing buildable Lean projects and systematically reducing remaining proof holes.The authors present this as evidence that large-scale formalization is practically feasible under pinned environments.

2 Related Work

M2F targets the gap between snippet-level autoformalization and end-to-end project buildability by combining dependency-aware formalization with verifier-certified refinement.

  • 2 Related Work: Neural theorem provers generally assume well-typed statements and a buildable project, whereas M2F addresses upstream project- and library-level failures.The distinction separates proving elaborated goals from constructing the surrounding formal project.
  • 2 Related Work: Prior autoformalization systems use tool feedback, structural cues, dependency information, or retrieval, but M2F operationalizes refinement through a verifier-certified accept/revert rule.The paper positions M2F as complementary to these directions.
  • 2 Related Work: M2F makes end-to-end project buildability under a pinned environment the primary objective of autoformalization.Its evaluation tracks buildability, provenance-supported faithfulness, and proof repair under matched statements.
  • 2 Related Work: M2F complements alignment datasets and diagnostic-conditioned repair with project-level evaluation, provenance auditing, and matched-statement proof repair.Compute is reported in verifier-normalized units.

3 Problem Setup and Pipeline Overview

M2F converts long-form mathematical sources into provenance-linked Lean projects through two verifier-in-the-loop stages operating under a pinned environment.

  • 3 Problem Setup and Pipeline Overview: M2F maps a long-form LaTeX source into a Lean project that elaborates end-to-end under a pinned dependency revision.Each bounded edit is accepted only when toolchain feedback certifies objective improvement.
  • 3 Problem Setup and Pipeline Overview: The source is normalized into ordered JSON items supporting deterministic iteration, dependency recovery, and stable provenance links to source spans.Verification occurs under a fixed Lean toolchain and dependency revision.
  • 3 Problem Setup and Pipeline Overview: M2F separates knowledge import from proof discharge because proof repair becomes meaningful only after imports, namespaces, typing, and dependencies stabilize.This ordering makes project-level compilation an upstream prerequisite for proof repair.
  • 3 Problem Setup and Pipeline Overview: Stage 1 creates declaration skeletons and repairs localized compilation failures until a project elaborates while allowing proof placeholders.It assigns each item to a target file and commits patches only after VerifyFile confirms improvement.
  • 3 Problem Setup and Pipeline Overview: Stage 2 reduces remaining proof holes from the compilable project while keeping statement signatures fixed.Edits are restricted to proofs and optional local helpers that do not change existing signatures.

4 Method: VeriRefine for M2F

VeriRefine stabilizes long-running Lean refinement by separating patch proposal from verifier certification and accepting only strict objective improvements.

  • 4 Method: VeriRefine for M2F: VeriRefine applies bounded patches under a fixed Lean environment and commits them only when verification certifies strict improvement.Otherwise, the attempted edit is rolled back.
  • 4 Method: VeriRefine for M2F: Diagnostics are localized to scopes formed from declaration or hole ranges together with bounded file headers.This focuses repair on the relevant declaration while preserving import and namespace context.
  • 4 Method: VeriRefine for M2F: When a file elaborates, M2F can query a hole’s goal type and local context to condition proof planning and patch generation.Unavailable goal states are represented separately rather than treated as successful proof context.
  • 4 Method: VeriRefine for M2F: Stage 1 prioritizes fewer error diagnostics and then fewer localized errors, while Stage 2 prioritizes fewer remaining proof holes after compilation succeeds.The ordering never accepts a patch that increases compilation errors.
  • 4 Method: VeriRefine for M2F: The proposal layer includes skeleton generation, diagnostic-targeted repairs, proof planning, and localized proof patches, with optional splitting of long files.Certification remains enforced by the same verifier-mediated patch operator.
  • 4 Method: VeriRefine for M2F: Stage 1 uses declaration skeletons and typed stubs to stabilize cross-file availability before proof bodies are finalized.Stage 2 then starts from the compilable project and repairs holes under fixed signatures.

5 M2F: Interface Contract

M2F formalizes project-scale refinement as verifier-certified local editing under a pinned Lean environment. Its two stages compile statement skeletons first, then repair proof holes while accepting only strictly improving patches.

  • Statement compilation: Stage 1 inserts declaration skeletons for ordered statement items and repeatedly repairs files until they elaborate, allowing proof placeholders.Each attempted patch is reverified under the fixed environment.
  • Interface contract: The interface returns a compilable project and provenance map while using file-level Lean diagnostics as its minimal verification oracle.Warnings are ignored, and successful verification means zero error-level diagnostics.
  • Proof repair: Stage 2 freezes statement signatures and uses goal-conditioned local proof patches to close remaining holes under bounded verifier-call budgets.Goal states condition proposals but do not serve as the acceptance criterion.
  • Verifier-certified refinement: VeriRefine accepts an edit only when Lean feedback strictly improves the stage objective; otherwise the edit is rolled back.Stage 1 reduces elaboration diagnostics, while Stage 2 reduces diagnostics and remaining proof holes.

6 Experiments

M2F is evaluated on long-form mathematical sources and matched-statement proof tasks using a pinned Lean environment and provenance-based statement audits. It produces buildable textbook-scale artifacts, achieves complete audited long-form proof repair, and reaches 96% on FATE-H, while ablations and failure analysis expose sensitivity to structured conditioning and benchmark limitations.

  • Project artifacts: 153,853 lines of Lean code across 479 pages build end-to-end, with 241 files and 4,116 declarations in the combined long-form artifact.The artifacts cover Real Analysis and Convex Analysis and are produced without axiom declarations.
  • Statement compilation: Stage 1 reaches SCC = 100% and PB true on all long-form corpora, with ARR values of 0.42, 0.08, and 0.20.These values imply that at least 58%, 92%, and 80% of blocks elaborate immediately after insertion, respectively.
  • Proof repair: 100% PSR is achieved on all three long-form corpora under matched statements, with proof repair restricted to proof edits after statement-signature auditing.The audited evaluation set preserves elaboration while replacing target proofs with placeholders.
  • Ablations: On the Paper ablation slice, diagnostics-only falls to 13.85%, and disabling replanning also degrades performance.The result indicates that goal/context conditioning and plan revision matter for heterogeneous exposition and implicit dependencies.
  • Failure analysis: Four FATE-H instances remain unresolved or problematic: one has an inconsistent formal statement, two remain unsolved without expert lemma maps, and one is solved with the lemma map.Verifier-guided investigation localized the inconsistent benchmark statement for expert confirmation.

7 Conclusion

M2F compiles long-form mathematical sources into buildable Lean projects using verifier-certified refinement and provenance-aware statement and proof processing. Its design emphasizes auditable evaluation, recoverable runs, and human-audited statement faithfulness.

  • 7 Conclusion: M2F compiles textbook- and paper-scale sources into Lean projects that build end-to-end under a pinned environment while preserving span-level provenance.The pipeline combines dependency-aware statement compilation with matched-statement proof repair under a toolchain-certified accept/revert rule.
  • A.1 Prompting philosophy: Statement-first prompting favors minimal, canonical, mathlib-aligned declarations because they reduce accidental typeclass obligations, brittle goals, and rewriting overhead.Repeated intermediate facts can trigger revision of statement or helper-lemma shapes rather than continued brittle proof search.
  • Instrumentation: Structured logs, checkpoints, histories, and metrics streams make long runs auditable, resumable, and reconstructable without manual bookkeeping.Resumed segments receive new run identifiers so corpus totals can be aggregated without double counting.
  • Instrumentation: The instrumentation schema defines artifact categories and machine-readable records for datasets, histories, metrics, token usage, and persistent failures.Per-call logs retain detailed model transcripts, while compact JSON/JSONL artifacts support querying and analytics.
  • A.3 Human statement-audit protocol: Stage 2 evaluation uses manually audited Lean signatures matched against provenance-linked source excerpts, with audits checking binders, side conditions, conclusions, and hidden assumptions.The audit is the correctness gate because model-based reviewers may share correlated failure modes.

A.4 Stage 2 ablation slices (section identifiers)

The ablation slices are fixed dataset files with explicitly recorded corpus coverage, so methods within each corpus are compared on the same data.

  • A.4 Stage 2 ablation slices: Each long-form corpus uses a fixed dataset-file slice for all ablation methods, with coverage recorded by chapter and section components.Real Analysis uses data/proof/ch-real-nums.json, while Convex Analysis uses data/section04.json.
  • A.4 Stage 2 ablation slices: The appendix documents semantic artifact categories and stable schema invariants rather than committing to a particular directory layout or filename convention.This keeps preprocessing, resumability, debugging, and metrics reconstruction defined by meaning rather than storage paths.

B.1 Dataset record: a natural-language item

A dataset record represents one extracted mathematical unit and supplies natural-language content to statement generation and, when available, proof completion. JSON-array ordering and index uniqueness define canonical processing order.

  • B.1 Dataset record: A dataset record describes one extracted definition, lemma, theorem, or similar mathematical unit in natural-language or LaTeX-like form.The statement pipeline consumes statement text, while the proof pipeline uses proof text for meaningful proof targets when present.
  • B.1 Dataset record: Datasets are JSON arrays whose unique indices define canonical iteration order for downstream consumers.Records with empty proofs may be skipped by proof-stage consumers depending on configuration.
  • B.1 Dataset record: The semantic schema includes labels, environment type, number components, extracted labels, source context, content, dependencies, and proof fields.The example separates source-location metadata from the extracted mathematical content and dependency list.
  • B.1 Dataset record: Optional lemma maps provide declaration-level navigation hints rather than formal proof steps, while verifier feedback remains the acceptance criterion.The system may use hinted declarations for retrieval or application but cannot rely on unverified intermediate claims.
  • B.1 Dataset record: Progress checkpoints store the next dataset or file index in a single JSON object to support resumption after interruption.Checkpoints are overwritten in place and contain exactly one integer key.

B.4 History record: compact per-task trace

History and metrics artifacts provide compact, append-only traces of pipeline activity, while verifier-call accounting defines comparable compute across stages and corpora. Budgets and event schemas support reproducible aggregation across interrupted runs.

  • B.4 History record: History records are append-only JSONL objects containing timestamps, pipeline and run identifiers, Lean-file context, task metadata, event kinds, and payloads.Common records include planner outputs, replanning requests, repair attempts, and cleanup actions.
  • B.4 History record: Per-call logs retain full model transcripts and applied diffs, whereas compact history records provide lightweight continuity and debugging context.Truncation saves space while full raw text remains available in per-call logs.
  • B.4 History record: The metrics event log uses a stable top-level schema of timestamp, run ID, event label, and payload, grouped into run, boundary, verifier, oracle, and planning events.Run summaries provide concise totals without scanning the full stream.
  • C.3 Reporting total verifier calls: Verifier calls are single-file Lean elaboration or typechecking invocations under the pinned environment, and zero error-level diagnostics define verification success.These checks are the ground-truth accept/reject signal for statement and proof repairs.
  • C.2 Budgets and per-target caps: Explicit caps bound propose-to-verify loops and fallback repairs, making compute predictable and runs resumable.Stage 1 processes each item with at least one and at most 1 + K verifier calls before early termination or further repair.
  • C.3 Reporting total verifier calls: Interrupted runs receive separate run IDs, and corpus-level verifier totals are summed across included segments.This aggregation applies both direct event counts and reconstructed Stage 1 counts when explicit check events are unavailable.

C.4 Paper metrics: definitions and log reconstruction

The paper defines buildability, proof success, and verifier-centered metrics, reconstructing them from structured logs and distinguishing verifier calls from model-oracle calls. FATE-H reporting also accounts for a wrong-statement instance and per-problem outcome categories.

  • Metric definitions: PB is true when the final generated project builds under the fixed Lean environment, while PSR is the fraction of matched-statement holes closed with zero verifier errors.PSR excludes statement edits during proof search and requires both removal of the designated sorry and successful verification.
  • FATE-H outcomes: 96 problems were solved automatically, 1 with lemma-map supervision, 2 remained open, and 1 had a wrong statement.The wrong-statement instance is separately styled in Figure 3 and is not solvable as stated.
  • Log reconstruction: Oracle calls are model invocations that produce project-changing edits or plans, including statement synthesis, bounded repairs, proof planning, and proof-edit execution.Their totals are reconstructed from oracle-result events and, for some Stage 1 runs, per-item repair counters.
  • Accounting boundary: Lean LSP/MCP queries are excluded from oracle-call totals and verifier-normalized or token-based accounting, although they may add wall-clock time and local compute.These queries include goal inspection, hover information, local search, completions, and small snippet execution.
  • Cost accounting: Verifier calls remain the primary compute unit, while token usage complements oracle-call frequency because invocation counts do not capture call size.Token totals can be summed from metrics events or recovered through the token-backfill artifact.

C.8 Fractional accounting robustness check

The paper tests robustness by pricing model-oracle calls as a fractional addition to verifier calls, while relating the accounting to scalable, auditable project governance. The artifact demonstrates localized edits, inspectable dependencies, and provenance at textbook scale.

  • Fractional accounting: Costα = V + αQ provides a verifier-equivalent compute total that varies the assumed price of oracle calls.V is verifier-call count, Q is oracle-call count, and α ranges from cheap-oracle to comparable-oracle regimes.
  • Fractional accounting: The reported robustness checks use α values of 0.05, 0.10, and 0.25 and compute totals from reconstructed verifier and oracle counts.Table 12 reports the resulting verifier-equivalent totals for representative α choices.
  • Governance at scale: A verifier-driven closed loop localizes failures to files, sections, or parts, enabling revert-and-retry without corrupting the rest of the project.Edits are accepted only when Lean certifies strict improvement in buildability or remaining proof holes.
  • Navigability: Source-faithful module structure preserves navigability by mirroring section numbering, splitting large sections into partK modules, and retaining stable interfaces for downstream imports.The file tree illustrates structure-preserving splitting while keeping verifier-local edit scopes.
  • Governance at scale: The Convex Analysis artifact performs a 23-way structure-preserving split, attaches 600+ provenance anchors, and manages 160+ unique imports.These indicators target edit locality, dependency governance, and auditability rather than the primary scale statistics.

D.4 Representative verified code excerpts

The excerpts show how the generated Lean library exposes reusable interfaces, classical analysis theorems, and heavily parameterized convex-optimization results. Together they illustrate complexity from dependencies, long proofs, and layered hypotheses.

  • Project structure: The formalized Convex Analysis project mirrors sections 1–15 and exposes a Lean file tree for navigating its generated modules.The project includes section-specific modules and structure-preserving part files.
  • Reusable interfaces: A supporting-hyperplane definition encodes a hyperplane equation, a global supporting inequality over C, and attainment of equality at some point.The interface is imported across multiple chapters and illustrates a reusable textbook-level notion.
  • Real analysis: The mean value theorem excerpt formalizes continuity on a closed interval, differentiability on its interior, and existence of c satisfying the classical difference quotient identity.The theorem is presented as a representative long proof whose correctness must remain stable under localized edits and refactoring.
  • Convex analysis: The convex-optimization excerpt combines finite-dimensional spaces, operator-valued parameters, prox-functions, smoothing, and multiple convexity and boundedness hypotheses.Its theorem statement includes a smoothing parameter µ depending on operator norm, iteration count, and prox-related quantities.
  • Convex analysis: The optimization theorem concludes an explicit error bound and an epsilon-convergence condition for the generated sequence.The excerpt includes bounds involving operator norm, prox diameters, strong-convexity parameters, smoothness, and N.
Loading 2602.17016v1…