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

AI summary

Overview

Research area: AI for mathematics — autoformalization (translating informal mathematics into machine-checkable code), interactive theorem proving in Lean 4, and human–AI collaboration for research workflows.

Technical level: Intermediate. The paper is readable without Lean expertise, but some familiarity with proof assistants, dependency graphs, and LLM agent pipelines helps.

Scope: The paper presents PaperFormalizer, a Lean-based agentic pipeline in which an author's own research paper is transcribed, reviewed, repaired, formalized, and proved, with the author making every decision that could change what the paper claims.

What This Paper Is About

Even carefully proofread theory papers often contain small gaps — an unstated regularity condition, a boundary case, a proof step that silently assumes more than the paper states. PaperFormalizer is a tool that turns a paper's LaTeX source into a dependency graph of statements, audits each statement for faithfulness, ambiguity and correctness, and then formalizes and proves them in Lean against Mathlib, optional domain libraries, and the author's personal library of reusable results.

The core claim is that two problems cannot be settled by a machine alone: natural language is ambiguous (a statement can admit several readings, and formalizing the wrong one proves something the author never meant), and when a statement is false there are many possible repairs, of which the logically minimal one may discard the part of the result the author cares about most. Both depend on author intent, so the pipeline stops and asks.

Key Contributions

1. A six-stage author-in-the-loop pipeline. Stage I (natural language review) has two steps — transcription of the LaTeX source into a dependency graph of statements, and review for faithfulness, ambiguity and correctness with proposed repairs. Stage II (autoformalization) has four steps — planning, scaffolding, proof filling, and linking each Lean declaration back to the paper statement it formalizes.

2. A principled division of labor between agent and author. The agent never unilaterally makes decisions that would change what the paper claims: repairs that substantively change a main result, any other ruling leaving a main result substantively different than printed (unless it only adds a bookkeeping assumption such as measurability), promotion of results into the toolkit, and sharing of a paper. All of these wait for author approval on a local web page.

3. A personal, growing Lean toolkit plus a public sharing site. Each run lives inside the author's own Lean project, structured in three tiers: read-only base libraries (Mathlib and chosen domain libraries), a middle tier of reusable results split into Foundations (standard results missing from base libraries) and Tricks (the author's own reusable lemmas), and a top tier with one module tree per formalized paper. Proved results can be promoted into the toolkit, and verified papers can be shared publicly at paperformalizer.org.

4. A detailed case study on the authors' own paper. The pipeline produced a Lean-verified version of Estimation of Treatment Effects in Extreme and Unobserved Data, in which all seven results were proved with no sorry and no axioms beyond Lean's standard ones — after five of the seven were found not to hold as printed.

Main Findings

• Most results in the case-study paper needed repair. Five of the seven results in Estimation of Treatment Effects in Extreme and Unobserved Data did not hold as printed. The errors traced to two independent roots: Proposition 3.3 (the identification result) and Lemma A.1 (the rate of the adaptive Hill estimator). Theorem 3.5 and Lemmas A.2 and A.3 rest on Proposition 3.3 and inherit its error, and their proofs also contain errors of their own. The two corollaries had no error of their own and were restated to follow the revised results.

• A concrete counterexample refuted the identification result. For Proposition 3.3, the reviewer constructed a setting with X ~ Unif[0,1], D ~ Ber(1/2) and V ~ Unif[0,1] independent, W independent with P(W > w) = w^(-3) for w ≥ 1, U = W(V, 1−V), and α = 1, with T(w) = (1−w^(-3))^(-1/3), Y(1) = DW + (1−D)T(W) and Y(0) = 0. Exogeneity given X and homogeneity both hold, yet the right-hand side of the claimed formula equals 3/2 while θ_NETE = 3/4. The gap: the proof replaces E[Y(d) | X, U] by the observed regression f(X, d, U), which needs exogeneity given (X, U) — something the two stated assumptions do not imply. The reviewer also found three smaller gaps in the same proof: a choice of ε > 0 with α − β + ε < 0 that requires α < β, a radial limit stated as α/(β − α) instead of β/(β − α), and uniform integrability inferred from a uniform bound on first moments.

• The accepted repair preserved the main claim. The repair keeps the identification formula and adds the conditions the proof actually uses: α < β, 0 < p(X) < 1, conditional mean exogeneity E[Y(d) | X, U, D] = E[Y(d) | X, U], and finite conditional tail means of |Y(d)|.

• Rate errors were of a different kind. In Lemma A.1, the adaptive Hill estimator's selection rule compares candidates up to rank n, which requires the order statistic of rank n+1; the statistic in the proof differs from the one in Algorithm 1; and the density used in the proof carries the outcome exponent α where the tail index β belongs. The repair states the rate for a full-sample Hill estimator with prefix selection, with exponent 1/3 for β < 1 and a log n factor retained at β = 1. In Lemma A.2, the sampling-term rate t^(β/2) n^(−1/2) requires a bounded variance of the normalized score that the assumptions do not supply; with symmetric stable noise of index 3/2 the doubly robust estimator's error has scale n^(−2/15) while the printed bound is of order n^(−1/5), so the probability that the bound holds tends to zero. The repaired lemma replaces the square-root term by a truncated-variance bound, replaces e(t) by its tail supremum sup over r ≥ t of e(r), and keeps a logarithmic factor in the angular bias at β = 1; the angular Wasserstein rate is taken from a cited result and enters as an explicit assumption.

• Ambiguity, not just error, was a major output. The run made 94 readings explicit and listed them as clarifications — for example, fixing that the homogeneity inequality of Assumption 3.2 holds for both treatments and every radius, uniformly over the bounded covariates and the positive unit sphere of the ℓ1 norm. Four further findings, raised while Lean statements were being written, concerned points the paper leaves open, such as whether the overlap constant may depend on the sample size; the authors answered each by stating their reading, which the Lean code then adopted.

• Scale of the formalization. The Lean development of the case-study paper has 136 files and about 26,000 lines, plus 13 modules (about 2,500 lines) drawn from the Foundations tier of the authors' toolkit, including Chernoff bounds, conditioning on events, and Rényi's representation of exponential order statistics used in the proof of Lemma A.1.

• Results on two further shared papers. In an optimal transport paper, the run proved all twelve results in Lean as printed. In a neural causal models paper, it proved 20 of 29 results and refuted two for which no repair keeps the claim; neither refuted result is a main result. The introduction separately notes that 15 of the 29 results in another paper needed some revision.

• Model assignment is deliberately split. Most roles run on OpenAI's gpt-6.1-sol through the Codex CLI at high or medium reasoning effort; the Lean plan, the second independent reviewer in the proof-review loop, and curation of the personal toolkit run on Claude Opus through the Claude Code CLI — so the plan and the final review come from a different model family than the one writing the Lean code. Claude Code's roles fall back to gpt-6.1-sol at high reasoning effort, and any model can be swapped via an environment variable.

Methodology in Plain English

The pipeline is run from inside a coding agent (Claude Code or Codex) and displays its progress on a local web page next to the paper, with findings marked on the text and the original in red against revisions in blue.

Stage 1 — Transcription. The agent takes a .tex file, folder, or arXiv e-print and splits the paper into nodes, one per definition, assumption, lemma, proposition, theorem, corollary, or cited result, adding an edge whenever one statement or proof uses another. Nodes whose text breaks off mid-formula are sent back to the transcription agent.

Stage 2 — Natural language review. A reviewer agent walks the graph in dependency order, checking each node for faithfulness (does it match the paper?), ambiguity (is there exactly one sensible reading?), and correctness (does the statement hold, and does its proof establish it?). If context settles the reading, the reviewer pins it as an explicit assumption the author can edit or remove. If not, it stops and asks. A result is called wrong only if a counterexample is found within the paper's own setting; if every counterexample is a degenerate case readers would exclude anyway (zero variance, an empty class), the reviewer adds a side condition instead of an error. For each error a fixer agent proposes a small repair preserving the result's key contribution, and a separate reviewer checks the repair. Cited results are checked against their sources, which the system downloads itself or requests from the author, and misuse of a citation is reported.

Stage 3 — Planning. A planning agent decides per statement whether to reuse an existing library result, formalize it, or leave it cited. Reuse draws on Mathlib, on domain libraries chosen at installation (Causalean for causal inference, StatLean for statistics, FoML for learning theory, optlib for optimization), and on the author's toolkit, searched by keyword and via the Loogle and LeanSearch engines. Cited results that are not main results usually stay cited as explicit assumptions, since formalizing them can be too costly. A separate agent checks the plan for faithfulness.

Stages 4 and 5 — Scaffolding and proof filling. Scaffolding writes every planned statement in Lean with proofs left open, compiles it, and checks each Lean statement against the natural language one. Proof filling then loops: workers fill proofs by querying Lean through its language server, while reviewer agents confirm that each proved statement is faithful and that no proof uses sorry or non-standard axioms. If Lean work shows a paper statement is wrong as written, the pipeline proposes returning to the review stage, subject to author approval.

Stage 6 — Linking and report. Each Lean declaration is linked to the paper statement it formalizes, so the author can confirm the formalization assumption by assumption without reading proofs. The report places each result in one of seven categories — proved, side condition, conditional, repaired, refuted, not determined, unresolved — lists every added condition, pinned reading and repair, and rates how much the mathematics changed: major errors, minor issues, or no errors found. Outputs are an annotated paper, a revised paper in the author's own LaTeX class and file layout (no macros or traces of the tool), and the Lean code.

Why This Matters

Formal verification of research papers has been rare because it is expensive — the paper notes that hand-formalizing a paper can take weeks even for someone fluent in both the field and Lean. PaperFormalizer's argument is that the cost can be amortized: a personal toolkit accumulates the definitions and techniques of one research line, so each new paper in that line has fewer results to formalize from scratch, and shared verified papers give downstream researchers checked results to build on rather than re-deriving.

Potential applications:

• Theory-heavy statistics and machine learning papers — the case study is an extreme-value treatment-effect paper, exactly the kind of work with long technical appendices where a missing regularity condition goes unnoticed.
• Causal inference and econometrics — via domain libraries such as Causalean, papers whose claims rest on identification assumptions can be checked assumption by assumption.
• Operations research and optimization — via optlib, where convergence rates and feasibility conditions are common sources of silent gaps.
• Textbook, survey and course material — verified statements and linked Lean code can serve as checked reference material for readers who want to see exactly which hypotheses each theorem uses.

Industry relevance: The pipeline runs inside standard coding agents (Claude Code, Codex) and produces artifacts — annotated PDFs, revision reports, compilable Lean code — that fit existing authoring and review workflows. Teams that rely on mathematical guarantees (ML theory groups, quantitative research, verification-adjacent engineering) get a reviewable audit trail linking each formal claim to its natural-language source.

Future Directions

• Replacing the author's judgment is still unsolved. The paper offers a fully automatic mode where every reserved decision follows the agent's recommendation and is reviewed afterward, but explicitly recommends it only for a first pass, since a decision made on the author's behalf may differ from what the author intends. How much of the loop can safely be automated is open.

• Measuring repair quality at scale. The evidence rests on three of the authors' own papers. Whether "small repairs that keep the key contribution" generalize to papers by other authors, in other fields, and with unfamiliar notation is untested — as is whether reviewers other than the original authors would accept the same repairs.

• Growth of the shared verified corpus. The value of paperformalizer.org depends on adoption: each shared paper adds checked results to a common collection, but the paper reports no data yet on reuse rates or how much toolkit and shared code actually shorten the next formalization.

• Cost and scale of proof filling. Cited non-main results are typically left as explicit assumptions because formalizing them is too costly and slow. Reducing that cost — or deciding systematically which citations are worth formalizing — would determine how much of a paper's mathematical foundation ends up machine-checked.

Target Audience

Authors of theory papers in statistics, machine learning, operations research, economics and mathematics who want to find and close gaps in their own proofs before or after publication; Lean and Mathlib practitioners interested in LLM-driven autoformalization pipelines; and AI researchers studying human-in-the-loop agent design, particularly the question of when an agent should stop and defer to a human rather than act on its best guess. Readers wanting the formal-methods background should note the paper assumes familiarity with Lean, Mathlib, and the sorry placeholder convention.

Authors’ 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.