cs.AIOct 22, 2026

PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean

Authors: Jiyuan Tan, Vasilis Syrgkanis, Jose Blanchet

Organizations: Stanford University

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

Even a carefully proofread paper can leave small gaps in its proofs or its stated assumptions. We introduce PaperFormalizer, a Lean-based agentic pipeline that helps authors find and close such gaps in their own papers and turn each paper into a Lean-verified version. Starting from the LaTeX source, PaperFormalizer transcribes the paper into a dependency graph of statements, audits each statement in natural language for faithfulness, ambiguity and correctness, and then formalizes and proves the statements in Lean against Mathlib, optional domain libraries and the author's personal toolkit. Only the author knows what a statement is meant to say and how a formalization gap in a result is best fixed. The pipeline therefore stops and asks the author whenever a statement admits more than one reading, presents every repair, in natural language and TeX symbols, as a proposal that the author can accept, decline or redirect, and leaves to the author every decision that could potentially change what the paper claims. The output is an annotated and revised version of the paper, a report of the changes, and Lean code in which each declaration is linked to the statement it formalizes. The author's toolkit grows as more papers are formalized, and authors can share their verified papers so that researchers who build on them can reuse their Lean code. By making verified papers practical to produce, PaperFormalizer aims to make research that rests on mathematical proofs more robust. PaperFormalizer runs inside a coding agent (Claude Code or Codex) and is available at https://github.com/Jiyuan-Tan/PaperFormalizer. Papers with Lean code shared by users are available at https://paperformalizer.org.

Figures & tables

Figure 1: Workflow of PaperFormalizer . Stage I turns the L a T e X source into a reviewed and repaired dependency graph. Stage II formalizes and proves the revised statements in Lean. Dashed purple arrows mark the points where the author takes part (Section 3 ); the dashed green arrow is the feedback loop into the personal toolkit (Section 4 ).
Figure 2: The page of the case-study paper (Section 5 ) after its run; the viewer carries the name of the public website, PaperFormalizer. The left column tracks the run’s stages (V1 is Stage 1, V1.5 Stage 2, F1–F1.5 Stage 3, F2 Stage 4, F2.5–F4 Stage 5, and F5–V6 Stage 6), gives the paper’s contents, and draws the proof map, in which an arrow reads “used by” and each result is colored by its review outcome. Above the paper are the report’s verdict and the box in which the author writes to the agent. The paper itself follows, with the pipeline’s marks; Figures 4 and 5 show one of its results.
Figure 3: (a) A toy dependency graph after Stage 2. Each node is a statement of the paper; edges point from a result to the results that use it. Colors show the review outcome. (b) The categories in which the final report places each result of the paper.
Figure 4: Proposition 3.3 of the case-study paper on its page in the PaperFormalizer viewer. The printed statement is shown in red and the confirmed repair in blue; the card on the right gives the reviewer’s finding, quoting each step of the proof that fails. The dots under the statement open the other notes on this passage, here two clarifications.
Figure 5: The Lean statement of Proposition 3.3 next to the revised statement. Each hypothesis of the Lean theorem links to the assumption of the paper it formalizes (Assumption 2.1, 3.1 or 3.2, a clarification, or the proposition itself) and to its definition in the Lean files; pointing at a row highlights the matching phrase of the paper.
More in this topic

Autoformalization

Autoformalization converts natural-language mathematics, proofs, and specifications into machine-checkable formal languages.

See all 115 papers

Explore similar work

CardsList
Oct 14, 2026

Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization

We introduce a novel method for verifying Lean formalizations that goes beyond LLM-judged faithfulness. Unlike most verification methods, which rely on LLMs or trained models, our method combines LLM-based semantic review with mechanical numerical and vacuity checks, providing checkable feedback and detecting errors missed by LLM judges. We apply this method, along with our Extract-Verify-Proof autoformalization pipeline, to construct the Formalized Library of Mathematical Functions (FLMF), a partial formalization of the NIST Digital Library of Mathematical Functions (DLMF). On three labeled datasets, our method achieves the lowest accepted-error rate among the evaluated methods, measured as the fraction of incorrect statements accepted by the verification method. Expert review of the results also identifies translation and source defects in existing datasets. Code available at https://github.com/annamei1/FLMF-Ch7ErrFunc-Release.git.

Anna Mei, Michael R. Douglas

Harvard University · CMSA, Harvard University and AletheAI, Inc

Formal VerificationAutoformalizationLLM-as-a-Judge
AskPDF
Feb 19, 2026

M2F: Automated Formalization of Mathematical Literature at Scale

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%96\% proof success (vs.\ 80%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.

Zichen Wang, Wanli Ma, Zhenyu Ming +3

School of Mathematical Sciences, Peking University · Beijing International Center for Mathematical Research, Peking University · Huawei Technologies +1

AutoformalizationFormal VerificationAutomated Theorem ProvingLean Theorem Proving
AskPDF
Jun 3, 2026

LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization

Long-horizon autoformalization of research mathematics fails not only at hard lemmas, but at scale: statements drift, dependencies tangle, context decays, and local repairs corrupt distant work. We present LeanMarathon, a multi-agent harness for reliable research-level Lean autoformalization. Its core abstraction is an evolving blueprint: a Lean file that serves simultaneously as formal proof skeleton, natural-language proof graph, and shared system of record. Four contract-scoped agents construct, audit, prove, and repair this blueprint. These agents are coordinated by a two-stage orchestrator that first stabilizes target fidelity through adversarial review and then discharges the proof directed acyclic graph (DAG) from its dynamic leaves upward in parallel CI-gated rounds. LeanMarathon turns one brittle multi-hour run into many local, recoverable, parallel transactions. We evaluate LeanMarathon on two recent research papers spanning four Erdős problems (#1051, #1196, #164, #1217). Across three autonomous runs, it formalizes all seven target theorems with no sorry, proving 258 lemmas and theorems. These results show that reliable AI co-mathematics requires not only stronger provers, but durable harnesses that preserve target fidelity across long mathematical developments. The code can be found at https://github.com/YuanheZ/LeanMarathon.

Yuanhe Zhang, Yuekai Sun, Taiji Suzuki +2

Department of Statistics, University of Warwick, UK · Center for Advanced Intelligence Project, RIKEN, Japan · Department of Statistics, University of Michigan, USA +3

Lean Theorem ProvingAutoformalizationMulti-Agent LLMs
AskPDF