PaperFormalizer puts authors in control of AI-assisted Lean checks for research papers
A new preprint describes an AI pipeline that reviews a paper’s claims with its author, then links revised statements to Lean-checked declarations.
Formalising a paper without silently changing what it says
A preprint posted on October 22 introduces PaperFormalizer, an agentic workflow intended to help researchers turn their own mathematical papers into Lean-verified artifacts. Its central design choice is procedural rather than a new theorem-proving model: the system is meant to stop when prose is ambiguous or a proposed repair could alter a result, and to leave that decision with the paper’s author.
The distinction matters. A Lean proof can certify that a formal statement follows from the definitions and prior results supplied to it. It cannot, by itself, decide whether that statement still captures the author’s intended theorem after an informal sentence has been translated or repaired. The authors present PaperFormalizer as a way to make that gap visible instead of hiding it behind a successful compilation.
From TeX source to a linked formal record
According to the preprint, the pipeline begins with a paper’s LaTeX source. It extracts definitions, assumptions, results and cited claims into a dependency graph, then audits them for faithfulness, ambiguity and correctness. When the system finds a counterexample or a reading that is not settled by the text, it can propose a small repair or ask the author which reading is intended. Only after that review does it plan Lean declarations, reuse available library results where appropriate, fill proofs and link each declaration back to the corresponding statement in the paper.
The reported output is more than a folder of proof files: it includes a revised paper, an annotated version that marks changes, and a report that classifies statements such as proved, conditional, repaired, refuted or unresolved. The authors also describe a personal Lean toolkit that may accumulate reusable results across a researcher’s papers. That could make later formalization cheaper, but it also means readers need to inspect which assumptions and previously formalized material are being reused.
What the case study shows—and what it does not
The authors report applying the workflow to three of their own papers. In one case study on treatment effects in extreme events, they say five of seven results needed revision before the final Lean version could be proved without sorry or nonstandard axioms. This is an illustrative report from the project team, not an independent audit of the papers, the implementation or every proposed repair. The work is also an unreviewed preprint.
For mathematical AI, the useful idea is not that an agent can settle authorial intent. It is that a formalization workflow can expose where intent, assumptions and proof code diverge—and give the domain expert an explicit chance to decide how to resolve that divergence.