Formalize your paper in Lean

Trusting the result without reading it

This is why the main theorems are stated first, and why you check them before any proof is written. Then, for each main theorem, a tool called challenge-gen writes a short Lean file of its own: the statement, and the definitions it uses, copied out of the project. Another tool, comparator, checks that the project proves exactly that statement, using no axioms beyond the three standard ones of Lean, and has Lean's kernel check every proof again. A reader who wants to trust the formalization reads these short files and runs comparator; the rest of the project can stay unread.

The shared library

LMLExplore is a Lean library of machine learning theory, built on Mathlib (Lean's main mathematics library) and on LML. AI agents write it and review each other's contributions. People decide what it should contain, in roadmaps: lists of results to formalize, by area (bandits, identification, online learning, reinforcement learning). A contribution is accepted once the library still builds and the AI reviewers approve it, with no person involved.

Step 1: setting up

The sentence you type points the AI to START.md, a page of instructions written for an AI agent. It has the AI install, after asking you: uv, a Python tool runner; elan, which installs Lean; jq and the GitHub command-line tool; and the lml plugin for Claude Code, a set of instructions (called skills) that Claude Code loads when they apply. It installs only into your home directory, never as administrator, and each step first checks whether it is already done, so running it again is safe.

The new repository starts as a copy of a template, which provides the folder layout, the scripts and the checks that run on GitHub. It is named after the paper's Google Scholar key, such as Garivier2016Optimal (first author, year, first word of the title). It can be public on GitHub, which is recommended: GitHub then checks every change and publishes a website for the formalization (see below). It can also be private, or kept only on your computer.

Step 2: writing the main theorems

With you, the AI:

1. breaks the paper down into a list of lemmas, each with the results it uses, and looks in LMLExplore and Mathlib for what already exists;

2. writes a blueprint: a document that follows the paper, in which each statement is linked to its Lean counterpart, with a graph of which result uses which;

3. writes the definitions in Lean, in the generality a library would want rather than only for the paper's special case, then the statements of the main theorems, without proofs;

4. goes through each statement with you, against the paper. You record how it compares: the same claim, a more general one, a less general one (for instance after correcting an error of the paper) or one part of it. Errors found in the paper go to an errata file, with their corrections;

5. writes the short comparator files of the main theorems, which make the statements final.

Step 3: what formalize.sh does

The script runs without you, outside Claude Code, and does two things at once.

It writes the proofs. It starts Claude Code sessions one after the other, each with the same instructions. Each session takes one part of the blueprint (a chapter, or a main theorem with what it still needs), proves as much of it as it can, and saves its work in the repository. The first session sorts the general results the paper needs:

• those LMLExplore already has, which the paper uses as they are;

• those a roadmap asks for, which are proved in the paper's repository, then contributed;

• improvements of results LMLExplore already has, such as a more general version, which are contributed too;

• those no roadmap asks for yet, which stay in the paper's repository with a proposed addition to the roadmap, until a maintainer of LMLExplore accepts it (the one decision that needs a person);

• the paper's own results, which stay in the paper's repository.

The general results are written in a separate folder, ForLMLExplore/, following LMLExplore's conventions, so that contributing them is close to copying them. The list, with each result's status, is in PAPER_ROADMAP.md.

It contributes the general results. Background agents, from the Tau Ceti worker tool that also builds LMLExplore, take the general results once they are proved, and propose them to LMLExplore from your GitHub account, as pull requests. They then answer the AI reviewers until the pull requests are accepted. scripts/formalize.sh status lists these agents, and scripts/formalize.sh logs <id> shows what one of them is doing.

Both run on your Claude subscription, as fast as its limits allow. When a session hits a usage limit, the script waits 15 minutes and tries again.

When it stops. Once no proof is missing, the script runs comparator on every main theorem, which takes 10 to 15 minutes. If comparator agrees, the paper is formalized: the script stops, and lists what is still on its way into LMLExplore. Running it again sees that through: the background agents answer the reviewers, the script follows the pull requests, and once all are accepted, it moves the paper to the latest version of LMLExplore and deletes the paper's own copies of the results that LMLExplore now has. Until then, the paper uses one fixed version of LMLExplore, so that the library does not change under it.

The script also stops, and says why, when the sessions cannot work: Claude Code does not trust the folder, a session reports a problem with the setup, or three sessions in a row save nothing.

When the AI finds an error

Every error found in the paper goes to the errata file, notes/paper-errata.md: where it is, what is wrong, the correction, and the Lean result that states the corrected form, so that the file can be sent to the authors as it is. When a session finds that a main statement is false as written, it records why, in the errata when the paper is wrong or in notes/statement-corrections.md when only the Lean statement is. It marks the theorem as blocked, and the other sessions go on with the rest. /lml:formalize-paper decide asks you how to correct it, then changes the statement, its blueprint entry and its comparator file.

The website

For a public repository, GitHub checks every change: the project must build, and pass Mathlib's style checks and LMLExplore's rules. It also publishes a website with:

• the blueprint, on the web and as a PDF;

• a referee site, to browse the Lean declarations and what each one depends on;

• the literature links: for each result of the paper, the Lean declarations that formalize it and how they compare with it, also as data in the Literature Links format;

• the errata.

For example, the formalization of Optimal Best Arm Identification with Fixed Confidence (Garivier and Kaufmann, COLT 2016), made this way: its website and its repository.

With another AI agent

START.md works with any agent. The skills are plain text, in the plugin's repository, so another agent can follow them, and so can a person. The plugin itself and formalize.sh need Claude Code.