An agent built on Claude Code for formal theorem proving tasks. We used this system to prove all 12 problems from Putnam 2025, and completed a paper-level formalization of Effective Brascamp-Lieb inequalities.
Follow the setup guide to install Lean, Claude Code, and numina-lean-lsp-mcp:
See the usage guide for detailed instructions on running our agent:
# Run on a single file
python -m scripts.run_claude run leanproblems/Minif2f/mathd_algebra_478.lean \
--prompt-file config/prompt_complete_file.txt \
--max-rounds 5
# Run batch tasks from config
python -m scripts.run_claude batch config/config_minif2f.yaml
# Run all .lean files in a folder
python -m scripts.run_claude from-folder leanproblems/Minif2f \
--prompt-file config/prompt_complete_file.txt \
--max-rounds 5- numina-lean-lsp-mcp - MCP server for Lean LSP integration (based on lean-lsp-mcp)
- lean4-skills - Claude Code skills for Lean 4
- Leandex - Semantic search for Lean codebases
If you find the content of this project helpful, please cite our paper as follows:
@article{liu2026numina,
title={Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics},
author={Junqi Liu and Zihao Zhou and Zekai Zhu and Marco Dos Santos and Weikun He and Jiawei Liu and Ran Wang and Yunzhou Xie and Junqiao Zhao and Qiufeng Wang and Lihong Zhi and Jia Li and Wenda Li},
journal={arXiv preprint arXiv:2601.14027},
year={2026}
}
MIT License