Citations

Citing this project

@software{openatp,
  title = {OpenATP: Open Automated Theorem Proving},
  author = {Henry Robbins},
  year = {2026},
  publisher = {GitHub},
  url = {https://github.com/henryrobbins/open-atp}
}

References

[1]

Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern-Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, and others. Aristotle: imo-level automated theorem proving. arXiv preprint arXiv:2510.01346, 2025.

[2]

Oliver Dressler. Lean LSP MCP: Tools for agentic interaction with the Lean theorem prover. 3 2025. URL: https://github.com/oOo0oOo/lean-lsp-mcp.

[3]

Cameron Freer. Lean 4 Skills: theorem proving skill and workflow pack for AI coding agents. October 2025. URL: https://github.com/cameronfreer/lean4-skills.

[4]

Jiedong Jiang, Wanyi He, Yuefeng Wang, Guoxiong Gao, Yongle Hu, Jingting Wang, Nailin Guan, Peihao Wu, Chunbo Dai, Liang Xiao, and others. Fate: a formal benchmark series for frontier algebra of multiple difficulty levels. arXiv preprint arXiv:2511.02872, 2025.

[5]

Junqi Liu, Zihao Zhou, Zekai Zhu, Marco Dos Santos, Weikun He, Jiawei Liu, Ran Wang, Yunzhou Xie, Junqiao Zhao, Qiufeng Wang, and others. Numina-lean-agent: an open and general agentic reasoning system for formal mathematics. arXiv preprint arXiv:2601.14027, 2026.

[6]

Borja Requena, Austin Letson, Krystian Nowakowski, Izan Beltran Ferreiro, and Leopoldo Sarra. A minimal agent for automated theorem proving. In ICLR 2026 Workshop: VerifAI-2: The Second Workshop on AI Verification in the Wild. 2026. URL: https://openreview.net/forum?id=E30g7bO7rU.

[7]

George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: evaluating neural theorem-provers on the putnam mathematical competition. Advances in Neural Information Processing Systems, 37:11545–11569, 2024.

[8]

Lean FRO. Official agent Skills for developing with Lean 4. 2025. URL: https://github.com/leanprover/skills.

[9]

Mistral AI. Leanstral: open-source foundation for trustworthy vibe-coding. https://mistral.ai/news/leanstral, March 2026. Blog post.