AutoformBot

Turn a paper or your notes into a Lean 4 formalization you can check.
A plugin for your coding assistant: Claude Code, Muse Code or Codex.

What you get · Installation · Quick start · Example

What you get

Point AutoformBot at a paper, a book chapter or your notes. It plans the formalization, has agents carry it out in Lean, and shows exactly what is proved. See the example project.

flowchart LR
  setup["<b>setup</b><br>Lean project and blueprint"] --> roadmap["<b>roadmap</b><br>articles and dependencies"]
  source(["Paper or notes"]) --> roadmap
  roadmap --> formalize["<b>formalize</b><br>Lean definitions and proofs"]
  roadmap & formalize -.-> review["<b>human-review</b> · <b>agent-review</b><br>inspect the plan or the proofs"]
  roadmap & formalize --> site[("Blueprint site<br>book and dependency map")]

Loading

Installation

Requires Python 3.11 to 3.14, uv, Git, and Lean 4 v4.27.0 or newer with Lake.

Claude Code

claude plugin marketplace add facebookresearch/autoform-bot@v0.7.0
claude plugin install autoform@autoform

Muse Code

muse plugins marketplace add autoform 'https://github.com/facebookresearch/autoform-bot.git#v0.7.0'
muse plugins install autoform@autoform

Codex

codex plugin marketplace add facebookresearch/autoform-bot --ref v0.7.0
codex plugin add autoform@autoform

These commands install release 0.7.0. Then start a new session in your project, or anywhere for a new project.

Other install options

• On Claude Code before 2.1.71, run claude plugin marketplace add 'facebookresearch/autoform-bot#v0.7.0' instead.
• To follow main, drop the @v0.7.0 or #v0.7.0 suffix, and give Codex --ref main.
• To move from main or an earlier release, remove the autoform marketplace, then run the commands above. Claude Code: claude plugin marketplace remove autoform. Codex: codex plugin marketplace remove autoform. Muse Code: muse plugins remove autoform, then muse plugins marketplace remove autoform.

Quick start

Type these into your coding assistant; it runs AutoformBot's CLI for you.

Step	Claude Code, Muse Code	Codex	What it does
1	/autoform:setup	$autoform:setup	Set up the Lean project and blueprint
2	/autoform:roadmap	$autoform:roadmap	Plan from a paper or notes
3	/autoform:formalize	$autoform:formalize	Write Lean definitions and proofs
Any time	/autoform:human-review	$autoform:human-review	Review the roadmap, progress and statements
Any time	/autoform:agent-review	$autoform:agent-review	Request an independent AI review

For example, invoke roadmap and ask: "Build a complete roadmap for Sections 2–4 of paper.pdf." Keep the source in your project, or give a path the agent can read.

Run several sessions

In one test, four agents on a 36-leaf roadmap were no faster in two sessions than in one (74.8 accepted leaves an hour against 84.5) and used a third more tokens per leaf. So let one session run more agents first; in Codex, raise max_threads under [agents] in ~/.codex/config.toml. Past that, sessions divide the work by claiming articles on a claim board kept as Git refs on origin.

1. Give each session its own clone of the project, with the same origin and the same branch (not a git worktree).
2. Tell each session that other sessions share the project, and let it push claims and verified results to origin, even when they all start together: each one sees an empty claim board and would otherwise work alone.
3. Have each session release its claims when it stops: a claim nobody releases blocks its articles for seven days.

For example, invoke formalize in each session and ask: "Formalize the results that are ready. Four other sessions share this project; use claims, and push claims and verified results to origin."

Sessions on one machine share its memory, and each builds Lean: start only as many as fit (limits).

Search and reuse

Before adding a result, agents search the blueprint and every dependency that publishes a search index Autoform can verify, such as ATLAS.

Development

Clone with git clone https://github.com/facebookresearch/autoform-bot.git, then follow CONTRIBUTING.md. The blueprint format and CLI reference, servers/README.md and the changelog cover the rest. MIT license.

Issues and ideas are welcome. After a setup, roadmap or formalize run, your agent may end its report with a link to a draft issue about where AutoformBot got in its way; you decide whether to send it. AUTOFORM_DEBRIEF=0 turns this off.