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

• Long technical proofs can hide boundary cases, missing regularity conditions, or unstated assumptions even after several rounds of proofreading.The paper notes that such gaps usually do not affect the main conclusions.Source: §1 · p. 1
• Lean accepts a proof only when every step follows from definitions and earlier results, making it a way to expose gaps that hand proofreading may miss.Formalizing a research paper by hand can take weeks from someone fluent in both its field and Lean.Source: §1 · p. 1
• Because statements can have multiple readings and repairs can change what matters to the author, PaperFormalizer asks for author input when intent is uncertain.It also proposes repairs for the author to consider rather than deciding what the paper claims on the author’s behalf.Source: §1 · pp. 1–3
• PaperFormalizer helps authors find and repair proof gaps, then produces a Lean-verified version while leaving decisions about the paper’s claims to the author.Its workflow starts with a reviewed and repaired dependency graph and then formalizes and proves the revised statements in Lean.Source: §1 · p. 2, Figure 1 · p. 2
• Authors can build a personal toolkit and share verified papers so later work can reuse Lean code and results.The paper presents reuse across related papers as a way to make later papers cheaper to verify.Source: §1 · p. 2

• The six-stage pipeline begins with transcription and natural-language review, followed by planning, scaffolding, proof filling, and linking.The author controls the run from a coding agent and makes decisions on a local page that displays the paper with pipeline marks.Source: §2 · p. 3
• Transcription creates one graph node per definition, assumption, result, or cited result, with edges recording when statements or proofs use other nodes.A node that breaks off inside a formula or environment is returned to the transcription agent.Source: §2 · p. 3
• Natural-language review checks faithfulness, ambiguity, and correctness in dependency order, asking the author when context does not settle a statement’s intended meaning.A reviewer reports a result as wrong only after finding a counterexample in the paper’s setting; degenerate counterexamples may instead prompt a side condition.Source: §2 · p. 3
• Planning chooses which statements to reuse from libraries, formalize, or leave cited as explicit assumptions, while a separate agent checks the plan’s faithfulness.Reuse may draw on Mathlib, domain libraries, and the author’s personal toolkit.Source: §2 · p. 4
• Scaffolding writes and compiles Lean statements against their natural-language counterparts, and proof filling checks proofs for faithfulness, placeholders, and nonstandard axioms.If Lean work reveals a paper statement is wrong as written, the pipeline proposes returning to review for an author-approved repair.Source: §2 · p. 5
• Linking connects each Lean declaration to its paper statement, while the report lists changes and classifies the findings by severity.The outputs include an annotated paper, a revised paper, a report, and Lean code; the viewer maps stages and displays the proof map and review outcomes.Source: Figure 2 · p. 4, §2 · p. 5

• The author makes decisions that change the paper’s claims, corrects misreadings, and owns every output of the run.The agent never decides on its own to make a repair that would substantively change a main result.Source: §3 · p. 5
• Repairs that would substantively change a main result wait for the author, who can accept, decline, redirect, or withdraw the finding.Other rulings that leave a main result substantively different also wait, apart from bookkeeping assumptions such as measurability.Source: §3 · pp. 5–6
• Authors can flag findings, edits, or clarifications, revise pinned readings, add side conditions, and withdraw findings that misread the paper.The author can also provide a cited source the agent could not obtain or message the agent to clarify a passage.Source: §3 · p. 6
• The revised paper preserves the author’s class, preamble, bibliography, and file layout, while annotations show changes and Lean declarations link to statements.The author decides which results enter the toolkit and whether the paper is shared.Source: §3 · p. 6

• The author’s Lean project separates read-only base libraries, reusable Foundations and Tricks, and a module tree for each formalized paper.Source: §4 · p. 6
• The pipeline proposes cited-but-unproved results after planning and proved results after reporting for possible inclusion in the toolkit.An accepted cited result is proved in the toolkit and replaces an assumption; an accepted proved result can be promoted in general form, leaving the paper’s result as a corollary.Source: §4 · p. 6
• Nothing enters the toolkit without the author’s decision, and Lean checks that promotion leaves every paper and toolkit statement unchanged.The toolkit is intended to accumulate techniques from an author’s research line, reducing how many results later papers need to formalize from scratch.Source: §4 · p. 6
• Authors may share verified papers with revised source, PDF, findings, report, and Lean code; sharing is optional and at the author’s discretion.Source: §4 · p. 6
• Researchers building on shared papers can start from their Lean code and proved results rather than formalizing them again.The shared collection adds verified results for later work in the same area to build on.Source: §4 · p. 7

What the run produced

• All seven results were proved in Lean after the run found and helped repair five that did not hold as printed.The authors accepted weaker statements; two corollaries had no error of their own and were restated to follow the revised results.Source: §5 · p. 7
• The run made 94 readings explicit and resolved four further findings about points the paper left open using the authors’ stated interpretations.One clarification specifies that Assumption 3.2 holds for both treatments and every radius, uniformly over bounded covariates and the positive unit sphere of the ℓ1 norm.Source: §5 · p. 7

Repairing the identification result

• Proposition 3.3’s identification proof used an exogeneity step not implied by its assumptions; a counterexample gives 3/2 for the right-hand side but θNETE = 3/4.The accepted repair adds α < β, overlap, conditional-mean exogeneity, and finite conditional tail-mean conditions.Source: §5 · pp. 7–8

Repairing the rates

• Lemma A.1’s repaired rate uses a full-sample Hill estimator with prefix selection, while Lemma A.2 replaces an unsupported square-root bound with a truncated-variance bound.The repair retains a log n factor at β = 1; the angular Wasserstein rate is taken from cited work [18] as an explicit assumption.Source: §5 · p. 8

Shared papers

• Among the shared papers, the optimal-transport paper’s 12 results were proved as printed, while the neural-causal-model paper had 20 of 29 proved and two non-main results refuted.The latter two results had no repair that kept their claims.Source: §5 · p. 9

6 Usage and Current Status

• Authors use Claude Code or Codex to install PaperFormalizer, choose domain libraries, and ask the agent to formalize a paper.The agent runs the pipeline and asks the author on a web page whenever a decision is needed.Source: §6 · p. 9
• In fully automatic mode, decisions follow the agent’s recommendations, but the authors suggest using this mode only for a first pass because choices may differ from author intent.Authors can later approve or reject those decisions on the web page.Source: §6 · pp. 9–10
• PaperFormalizer aims to make verification a routine part of writing and let later work build on Lean-checked results and reusable code.The authors envision researchers verifying their own papers as they write them.Source: §6 · p. 10