PaperFormalizer Turns LaTeX Papers into Verified Lean Code, with the Author in the Loop

A team from Stanford has proposed a way to make formal verification of mathematical papers a routine part of preparing a publication. PaperFormalizer, released by Jiyuan Tan, Vasilis Syrgkanis and José Blanchet, turns a LaTeX source into a Lean-verified version of the work. It runs as an agentic pipeline inside Claude Code or Codex. The key idea: even a carefully proofread paper can contain small gaps in its proofs or in how its assumptions are stated, and the best person to close them is the author, with the machine helping.

A pipeline from LaTeX to Lean

The process starts with the source file. PaperFormalizer transcribes the paper into a dependency graph of statements: which lemmas each theorem needs and what rests on what. Each statement then goes through a natural-language audit along three axes: fidelity to the original meaning, ambiguity and correctness. Only after that does the system formalize the statements and prove them in Lean.

For the proofs, the pipeline draws on several sources:

• Mathlib, the main mathematical library for Lean;
• optional domain libraries for a specific field;
• the author's personal toolkit, meaning their own lemmas and definitions.

This toolkit accumulates over time. The more papers an author runs through the system, the more ready-made building blocks are available for the next one.

The author decides what the paper claims

Autoformalization often suffers from a silent substitution of meaning. A model can prove a formally flawless theorem that does not say what the author meant. PaperFormalizer's creators start from the premise that only the author knows what a statement is supposed to mean and how best to close a formalization gap.

The system therefore follows several rules:

• if a statement allows more than one reading, the pipeline stops and asks a question;
• every fix is presented in natural language and in TeX symbols as a suggestion that the author can accept, reject or redirect;
• any decision that could change what the paper claims stays with the author.

Unlike systems that try to formalize other people's work entirely on their own, here the human acts as the arbiter of meaning, while the machine handles the heavy mechanics of proving.

What the author gets

The result consists of three parts:

• an annotated and corrected version of the paper;
• a report on all changes made;
• Lean code in which every declaration is linked to the statement it formalizes.

That last link matters for readers. They can open any theorem in the text and see the corresponding verified Lean object, rather than hunting for the match by hand.

A shared library of verified papers

The authors also propose an ecosystem layer. Researchers can publish verified papers on paperformalizer.org, and those who build on these results can reuse the ready-made Lean code. This lowers the cost of formalizing the next paper in the same field: the necessary definitions and lemmas already exist and have been verified.

The tool is published on GitHub in the Jiyuan-Tan/PaperFormalizer repository. The paper came out on 22 October 2026 and made it into Hugging Face Papers' daily digest; the organization is listed on the page as Stanford University.

What this means for researchers

For mathematicians and theorists in statistics, economics and machine learning, whose conclusions rest on proofs, this is a way to get an independent check before submitting to a journal. It is especially useful where errors in assumptions slip through peer review unnoticed. The barrier to entry is lower than for manual formalization in Lean: you need a LaTeX source, access to Claude Code or Codex, and a willingness to answer the system's questions.

Caution is also warranted. The pipeline checks that a formal statement is proven, but a human still has to confirm that the formalization matches the intent. The quality of the result therefore depends on the author's attention at exactly those points where the system stops and asks.