cs.AIOct 22, 2026

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

Authors: Jiyuan Tan, Jose Blanchet, Vasilis Syrgkanis

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 116 papers

Explore similar work

CardsList

  1. Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization

    Oct 14, 2026Anna Mei, Michael R. DouglasFormal VerificationAutoformalization

    Harvard University · CMSA, Harvard University and AletheAI, Inc

  2. M2F: Automated Formalization of Mathematical Literature at Scale

    Feb 19, 2026Zichen Wang, Wanli Ma, Zhenyu Ming +3AutoformalizationFormal Verification

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

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

    Jun 3, 2026Yuanhe Zhang, Yuekai Sun, Taiji Suzuki +2Lean Theorem ProvingAutoformalization

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