Formalizing a paper in Lean

The formalize-paper skill

This is the workflow I follow to formalize a machine learning paper in Lean 4, on top of Mathlib and Lean Machine Learning (LML). It is written as a skill for Claude Code: a folder of instructions and template files that an AI agent reads when it starts, extends or checks a formalization. The instructions are plain Markdown, so they can just as well be read by a person.

Get the formalize-paper skill (a folder on GitHub). It contains:

• SKILL.md: the layout of a project, the workflow and the checks to run;
• bootstrap.md: how to start from an empty directory, step by step;
• tools.md: where each tool comes from, resources to learn Lean, and pitfalls met along the way;
• templates/: files to copy into a new project (lakefile, CI workflows, scripts, formalization.yaml).

To use it with Claude Code, copy the folder formalize-paper to ~/.claude/skills/ (for all your projects) or to .claude/skills/ inside the repository of your formalization. Claude then loads it when the task calls for it, or when you type /formalize-paper.

The skill was written during the formalization of a COLT 2026 paper by Maiti, Xu and Jamieson, and its examples use the names from that project (the Lean library Maiti2026Power, the repository colt-2026-83). A few of those names also appear in the templates; bootstrap.md says which ones to change for another paper.

What the skill says

The goal is a formalization that someone can trust without reading all of it. Two ideas serve that goal. First, the statements are fixed before the proofs: the main results of the paper are stated in Lean with sorry, and those statements are then frozen. Second, the main results are checked by comparator. For each main theorem, challenge-gen writes a self-contained file that imports only Mathlib, with the statement and every definition it uses copied into it. A reader checks that this short file says what the paper claims, and comparator checks that the project proves exactly that statement, with no axioms beyond the three standard ones.

Project layout

• source/ holds the TeX sources of the paper, and notes/blueprint-outline.md breaks the paper down into labelled lemmas before any Lean is written.
• blueprint/ is a leanblueprint. Part I follows the paper; Part II gathers the prerequisites that belong in Mathlib or LML (concentration inequalities, information theory, algorithms).
• The Lean library has three parts: Mathlib/ and LeanMachineLearning/ for general material, which mirror the upstream layouts so that it can later be contributed there, and one directory for the paper itself, with one file per result.
• formalization.yaml (schema) lists the main statements and the status of the project. comparator/ holds one generated challenge per main theorem.

Workflow

1. Outline first. Before any Lean or blueprint, write the outline: the results, the lemmas they need, what Mathlib and LML already provide, and the modelling choices. The outline fixes the labels and the proof routes; the blueprint chapters are then written from it.
2. Phase 1: statements. Define the objects in the generality a library would want, not only the special case the paper needs. State each main result with sorry, list it in formalization.yaml and generate its comparator challenge. From then on the statements are frozen, and phase 2 must prove exactly them.
3. Phase 2: proofs, driven by the blueprint. Before attacking a large theorem, expand its blueprint entry into small labelled lemmas with their dependencies. Formalize one coherent area at a time (for example a whole prerequisite chapter) rather than scattered lemmas. Prove the general, Mathlib-style statement and obtain the paper's version as a one-line special case.
4. Keep everything in sync. Each Lean declaration is linked from the blueprint and marked as done as soon as it compiles. Hypotheses that the proof does not use are removed, and the docstring says so.
5. Record. Update the status in formalization.yaml, the list of candidates for upstreaming to Mathlib and LML, and the README.

Checks

After every batch of Lean edits, the library must build with warnings treated as errors, pass the Mathlib linters, contain no sorry once in phase 2, and use theorem only for the main results (everything else is a lemma):

lake build <Lib> --wfail
lake exe runLinter <Lib>
grep -rn "sorry" <Lib>
grep -rn "^theorem" <Lib>
lake exe mk_all --lib <Lib>

After a change to the blueprint, a script checks its consistency (labels, dependencies, bibliography), the PDF and web versions are rebuilt, and checkdecls checks that every Lean name cited in the blueprint exists. When a main statement or a definition it depends on changes, the comparator challenges are regenerated and must still compile.

Starting from nothing

bootstrap.md is meant for a collaborator with an empty directory and no experience of formalization. It has seven steps, each ending with a check that must pass before going on:

1. Install the tools: elan (which installs Lean), VS Code with the Lean 4 extension, git and the GitHub CLI, leanblueprint, and a TeX distribution such as TeX Live.
2. Create the Lean project from the Mathlib template, with the template lakefile. The project depends on LML rather than directly on Mathlib, so that Mathlib comes at the version LML uses. Every Lean file follows the example file, written with Lean's module system.
3. Add the paper and write the outline: the TeX sources of the paper go in source/, and the outline is written before any blueprint or Lean.
4. Create the blueprint with leanblueprint new, one chapter per part of the outline. On every push, the template workflow builds and lints the project, builds the referee site and publishes the blueprint on GitHub Pages.
5. Write formalization.yaml from the template, which follows the formalization.yaml schema.
6. Set up comparator once the main statements exist. Two scripts, make-challenges.py and comparator-verify.sh, generate the challenges with challenge-gen and check them with comparator.
7. Push to GitHub and check that the workflow succeeds.

Tools and pitfalls

tools.md says where each tool above comes from and how it is installed. Most of them are maintained by the Lean developers, the Mathlib community or the LeanTrustBuilders suite. It also lists the GitHub actions used in CI, including mathlib-update-action for dependency updates. To learn Lean and Mathlib:

• Mathematics in Lean, the tutorial for doing mathematics with Mathlib;
• the Mathlib documentation, and Loogle to search for lemmas by the shape of their statement;
• the Lean reference manual and the Mathlib style guide;
• the Lean Zulip chat, for questions.

tools.md ends with a list of pitfalls met during the project, with their workarounds: about Lean and Mathlib, about the blueprint, and about the restrictions comparator puts on the definitions behind the main statements.