PaperFormalizer aims to help researchers turn a LaTeX paper into a version whose formalised results can be checked by Lean, while keeping the author responsible for decisions that change the mathematics. The project combines AI extraction, semantic review and proof construction in a workflow designed to stop for human judgment.[1][2]
The 22 October preprint is by Jiyuan Tan, Vasilis Syrgkanis and Jose Blanchet. Its central problem is translation: a machine can verify a formal proof of a statement, but that statement must still faithfully represent what the paper intended to claim. A successful proof of an accidentally weakened theorem would not settle the original result.[1]
From a paper to a checked statement
The workflow first transcribes results from the paper and organises their dependencies. It then audits the transcription for faithfulness, ambiguity and correctness before constructing Lean statements and proofs using Mathlib and selected domain libraries. The author reviews questions that require a mathematical decision, such as an ambiguous assumption or a repair that changes a claim.[2]
This separates two forms of verification. Lean checks whether a proof follows from the formal definitions and assumptions. The surrounding author-and-AI review checks whether those definitions and assumptions match the paper. Both are needed for a useful result, and they answer different questions.[1][2]
What each stage contributes
| Stage | Purpose |
|---|---|
| Transcription and dependency mapping | Identify the claims and which earlier results they use |
| Faithfulness review | Find ambiguity or changes in meaning before proving the wrong statement |
| Lean formalisation and proof | Check the formal argument against its stated assumptions |
| Author decisions and reporting | Approve repairs and connect the final proofs to the revised paper |
The intended output is more informative than a pass/fail label. The repository describes an annotated paper, revised text where changes were approved, linked Lean files and a report of what was proved and what was changed. That record lets a reader distinguish a theorem verified as written from one that required an additional assumption.[2]
A toolchain with real resource requirements
PaperFormalizer runs through a coding agent such as Codex or Claude Code. Its installation guidance estimates roughly 8 GB for a Mathlib-only toolkit, with additional domain libraries increasing the storage requirement. A verification run makes repeated model calls for extraction, review, planning and proof work, so the project recommends starting with a short paper or a limited set of results.[2]
The repository also describes practical limits in the current implementation, including setup paths that have not all received the same testing. Those details matter to a researcher deciding whether to trial the software: time spent installing libraries and resolving formalisation questions is part of the workflow, not an incidental cost outside it.[2]
Its strongest use is as an inspectable research aid. A failed formalisation can expose a missing assumption; an author-approved repair can make the mathematics clearer; a successful Lean proof can supply a reproducible check. The author remains able to see which of those outcomes occurred instead of receiving an unexplained declaration that the paper has been verified.[1][2]
Sources & further reading
- PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean arXiv / Jiyuan Tan, Vasilis Syrgkanis and Jose Blanchet · 22 Oct 2026 · Accessed 27 Oct 2026
- PaperFormalizer public repository and installation guidance GitHub / Jiyuan-Tan · Accessed 27 Oct 2026