A plugin for Claude Code and Codex that helps turn mathematical papers and notes into Lean 4 formalizations: plan the work, write proofs, and review progress from your coding assistant.
Requires Python 3.10+, uv, Git, and Lean 4
v4.27.0 or newer with Lake.
Claude Code
claude plugin marketplace add facebookresearch/autoform-bot
claude plugin install autoform@autoformCodex
codex plugin marketplace add facebookresearch/autoform-bot --ref main
codex plugin add autoform@autoformAfter installing, start a new session in the repository you want to inspect or set up.
Use these skills from your agent window; users do not need to learn or run its commands:
| Task | Claude Code | Codex |
|---|---|---|
| Set up the project | /autoform:setup |
$autoform:setup |
| Plan from a paper or notes | /autoform:roadmap |
$autoform:roadmap |
| Write Lean definitions and proofs | /autoform:formalize |
$autoform:formalize |
| Review the roadmap and progress | /autoform:human-review |
$autoform:human-review |
| Request an independent AI review | /autoform:agent-review |
$autoform:agent-review |
Start with setup, then use roadmap to plan your formalization and
formalize to work through it. Use either review command to inspect the plan
or the resulting formalization.
For example, invoke roadmap and ask:
Build a complete roadmap for Sections 2–4 of
paper.pdf.
Keep the source file in your project or provide an accessible path.
Setup changes local files by default. Creating or pushing a remote repository, enabling GitHub Pages, and publishing blueprint content require an explicit request; content published through Pages is public.
Autoform keeps the roadmap and dependency graph as Markdown under
blueprint/; publication graphs and pages are derived. See the
blueprint format and CLI reference for the complete
format and command contracts, or browse the
Cabannes thesis example.
git clone https://github.com/facebookresearch/autoform-bot.git
cd autoform-bot
make setup
make lint
make test
make check-exampleLean server architecture and operations are documented in
servers/README.md.
MIT.