PaperFormalizer helps authors turn a paper into a Lean-verified version. It reads each theorem, lemma and assumption alongside the paper's own proof, proposes a revision wherever a statement needs one, with the author deciding each, and proves the statements in Lean 4.
The papers below were formalized with PaperFormalizer and shared by the people who ran it. On a paper's page, the notes sit next to the text they refer to, and each result links to its Lean statement.
Share a paper you formalized
Share your formalized paper so that others can read it and build on its Lean proofs. On a finished run, press Share on the paper's page and sign in with GitHub; the paper is checked automatically and appears here under your GitHub name. A share carries the whole bundle, including the revised paper's TeX source and PDF.
Reading the badges.Proved in Lean counts the paper's results whose statement, as revised, Lean certifies; unresolved results are those for which no revision that holds was found. Revisions are statements revised where the original did not hold as written; clarifications are readings of ambiguous wording. Formalization covers the paper's results, not the prose around them.
7/7 proved in Lean5 revisions94 clarifications552M tokens
Summary. 7 result(s) of the paper were examined. 5 were found wrong as printed: 5 corrected (5 by a weaker statement), 0 not repaired. In Lean: 7 proved, 0 taken from the literature as cited, 0 not certified, 0 not formalized.
12/12 proved in LeanUnrevised213 clarificationsDepends on 1 cited result1.6B tokens
Summary. 12 result(s) of the paper were examined. None was found wrong as printed. In Lean: 12 proved, 0 taken from the literature as cited, 0 not certified, 0 not formalized.
2 unresolved20/29 proved in Lean15 revisions237 clarificationsDepends on 7 cited results2.5B tokens
Summary. 19 result(s) of the paper were examined, and 1 corollary a correction split off them. 13 were found wrong as printed: 13 corrected (7 by a weaker statement), 0 not repaired. In Lean: 20 proved, 0 taken from the literature as cited, 0 not certified, 0 not formalized.
Proposition B.2 — proof revised, statement unchanged, proved in Lean
Lemma E.1 — statement revised, proved in Lean
Theorem 3.6 — statement revised, proved in Lean
Corollary 3.8 — statement revised, proved in Lean
Proposition C.1 — statement revised, proved in Lean
Lemma E.6 — statement revised, proved in Lean
Lemma E.5 — statement revised, proved in Lean
Theorem 4.2 — statement revised, proved in Lean
Proposition 4.3 — statement revised, proved in Lean
Corollary 4.4 — statement revised, proved in Lean
Proposition B.1 — statement revised, proved in Lean
lemma lem:wide-nn-perekrestenko-theorem-viii-1 — no revision that holds, not proved in Lean
lemma lem:sup-wasserstein-anthony-theorems — statement revised, not proved in Lean
lemma lem:sup-wasserstein-anthony-theorem-17-1 — statement revised, not proved in Lean
lemma lem:sinkhorn-luise-proposition-1 — no revision that holds, not proved in Lean
No paper matches.
How a paper is formalized, and shared
PaperFormalizer reads a paper's LaTeX source. Every result is audited against the paper's own proof; where a statement does not hold as written, a revision is proposed, the smallest change that keeps the claim, and the author decides; the statements are then stated and proved in Lean 4, and two reviewers must each pass every Lean statement as saying what the paper says. The tool and its manual are on GitHub.
Pressing Share on a finished run sends its bundle and opens a GitHub sign-in that asks for your public name and nothing else. You confirm the share on the page that follows; an automatic check then confirms the bundle is complete and unchanged since the run wrote it, and the paper appears here, after the registry owner's review unless you are a trusted sharer.