formalize-math-paper, an agent skill for formalizing papers in Lean 4

formalize-math-paper is an Agent Skill: instructions, guides and scripts that an AI coding agent loads to formalize a mathematics paper in Lean 4 with Mathlib. It works with any agent that reads SKILL.md (Claude Code, Codex, Gemini CLI, Antigravity, Copilot, Cursor), and an arXiv link is enough to start.

Left alone, an agent drifts: it weakens a theorem when the proof gets hard, adds a hypothesis, swaps the paper’s argument for an easier one, guesses a Mathlib name, or declares an axiom and moves on. The skill keeps a long formalization from drifting this way.

The workflow

• Read. Find later versions, errata and earlier formalizations; read the TeX source; record every result, constant, citation and suspected typo.
• Set up. Three libraries, in layers: Basic for general mathematics, filed as Mathlib would file it; External for the cited results, stated in their sources’ terms; and the paper’s own results. A well-known theorem that the paper needs and no Lean library has gets a package of its own, which the project requires at a pinned commit.
• State. Every result is stated before any is proved, and a second agent checks each statement against the TeX.
• Prove. First what the paper proves, then what it cites, each by the paper’s own argument. A proof departs only when the paper’s step is wrong, needs mathematics Lean lacks, or has no meaning in the formalization, and every departure is reported. A cited result out of reach becomes a visible hypothesis, and the result is reported as conditional. A book too large for one pass is planned in layers, each published when it is proved.
• Check. Proofs use only Lean’s three standard axioms. A route check compares each proof’s dependencies with what the paper’s proof cites, Comparator confirms the statements of record, and cleanup removes unused hypotheses without changing any argument.
• Report. REPORT.md audits the paper (errors, gaps, missing and redundant hypotheses, departures, each confirmed by a second reader), places it in the literature, and lists what’s next. CREDITS.md records the agents, models, time and effort.
• Next paper. A private NEXT.md, kept out of git, asks what paper you could write next. It keeps only directions that would be papers of their own and works the best few through to the step where the paper’s method stops, with attempts, evidence and partial results, each marked as proved, checked or conjectured.
• Package. Write the Palomar files and, with your permission, publish and run the preflight.

Principles

• The paper is the source of truth; Lean judges correctness. A statement never changes to make a proof go through.
• Proofs follow the paper’s arguments, and every departure is necessary and reported.
• A formalization nobody compiled is a draft. Mathlib names are checked, never guessed.
• “Standard” and “routine” still need proofs.
• A skipped step, a failing proof or a changed statement is reported.

Examples

• The moving sofa: Baek’s 119-page proof that Gerver’s sofa is optimal, with one agent and 19 sub-agents in about four hours, on an early version of the skill.
• lean4-adr11: Allman, Degnan and Rhodes (2011), identifying the species tree from unrooted gene trees. Made in 6.4 hours; no result of the paper is wrong.
• lean4-ecsbm: the two theorems of the EC-SBM network generator (2025), in 1.5 hours; every proof follows the paper’s.
• lean4-camus: the optimality of CAMUS (2026), made with Codex and then Claude. Claims of Sections 2.4 and 3.2 fail as printed; Theorem 1 holds.
• lean4-markman25-hodge-abelian-fourfolds: Markman’s Weil classes on abelian sixfolds and the Hodge conjecture for abelian fourfolds, conditional on its sheaf theory and cited results on cycles. Eleven statements are false as printed or misprinted, and corrected.
• lean4-power-of-few-sparse: two papers of Tran and Vu on majority dynamics on G(n, p). Three theorems are false as printed; Lean proves counterexamples and corrected versions.
• lean4-smoothed-polygon: Chapters 2–8 of Hales and Vajjha’s book Packings of Smoothed Polygons (2024), in six rounds and about 55 hours, planned in layers. Mahler’s First conjecture is proved conditionally on one named hypothesis, which later chapters are to discharge. The audit has 61 findings; several statements are false as printed, among them a lemma refuted in Lean.
• lean4-optimal-control and lean4-fixed-point: packages of their own for the Pontryagin maximum principle, by Agrachev and Sachkov’s proof (three gaps in it are repaired), Filippov’s theorem, and Brouwer’s fixed-point theorem.

The skill was first written down from earlier work such as lean4-graham-rearrangement-conjecture (Pham and Sauermann, 2026): a ChatGPT draft that Claude made compile and audited on the day the skill began.

Thank you to the authors of the papers and books formalized with the skill. I formalized and audited your work, and published the results, without asking you first. I apologize for that.

Versions

A major version changes what the skill delivers. The last of each series is a release: 3.0.0 adds NEXT.md and the External library, and the 3.x versions since add packages of their own and a short README rewritten each round (the current version is 3.4.0); 2.5.1 has the report’s literature and what’s next, CREDITS.md and Basic; 1.4.0 has the workflow, Palomar packaging and proofs that follow the paper’s.

Install

1
 
npx skills add vltanh/formalize-math-paper -g
 

The README covers installing by hand and where each agent looks for skills.