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

PaperFormalizer. Author-in-the-Loop Autoformalization of Research Papers in Lean. By Jiyuan Tan and two others, from Stanford University. Published on the twenty-second of October. Its code repository is worked out: about five hundred source files, with a readme and a licence.

Even a carefully proofread paper can leave small gaps behind. Sometimes the gap is in a proof, and sometimes it is in the assumptions the paper states. A version of the paper verified in Lean would expose those gaps, but producing one raises a question no pipeline can settle on its own: what was each statement meant to say? Only the author knows that. And only the author knows how a formalization gap in a result is best fixed, because a fix can change what the result claims. That puts the author at the center of the process, alongside the prover.

PaperFormalizer is a Lean-based agentic pipeline built around that constraint. It helps authors find and close gaps in their own papers, and turns each paper into a Lean-verified version. The author is kept in the loop at the points where judgment is needed. The pipeline stops and asks the author whenever a statement admits more than one reading. It presents every repair as a proposal, written in natural language and TeX symbols rather than in Lean, and the author can accept it, decline it, or redirect it. And every decision that could potentially change what the paper claims is left to the author. The machine does the transcription, the checking and the proving. The person decides what the mathematics means.

Work begins from the paper's LaTeX source. PaperFormalizer first transcribes the paper into a dependency graph of statements, so that each result is held together with the statements it rests on. Each statement is then audited in natural language, on three counts: faithfulness, ambiguity and correctness. Only after that audit does the formal work begin. The statements are formalized and proved in Lean, against Mathlib, against optional domain libraries, and against the author's personal toolkit.

The output comes in three parts. There is an annotated and revised version of the paper. There is a report of the changes that were made. And there is Lean code in which each declaration is linked to the statement it formalizes, so the prose and its formal counterpart can be read side by side. The whole pipeline runs inside a coding agent, either Claude Code or Codex.

What the authors put forward is the pipeline itself and the place where its results accumulate. PaperFormalizer is available on GitHub, under Jiyuan-Tan slash PaperFormalizer. Papers with Lean code shared by users are collected at paperformalizer dot org. The design also compounds over time. The author's toolkit grows as more papers are formalized, so each paper an author verifies leaves more behind for the next one. And authors can share their verified papers, so that researchers who build on them can reuse their Lean code instead of formalizing the same results again.

The artifact at the end of the process is a paper paired with Lean code, each declaration tied to the statement it formalizes, and a report of what had to change to get there. PaperFormalizer's stated aim is to make such verified papers practical to produce, and through them to make research that rests on mathematical proofs more robust. Every one of those papers that is shared at paperformalizer dot org becomes Lean code the next researcher does not have to write.