Archon

Archon is an open source agentic system from FrenzyMath, the AI for mathematics team at Peking University's Beijing International Center for Mathematical Research. It autonomously formalizes research level mathematics in Lean 4, turning informal definitions and proofs into machine verified code across whole multi file projects rather than isolated competition problems. It is built for mathematicians and formalization researchers working on repository scale Lean projects. A plan agent provides strategic guidance while prover agents write and verify proofs, which keeps analysis separate from execution and limits context growth. Work runs in three phases: scaffolding, proving and polish. By default it runs on Claude Code with a Claude Opus model, using a modified Lean language server MCP and Lean skills, and it can also work with Codex. Recent releases add a dashboard with project scoping and a roadmap agent, per operation and per turn token and dollar cost tracking, a static dashboard export, multi project views of the proof dependency graph, and a safe mode that confines writes to the active project. Archon is free under the Apache 2.0 license and published on GitHub. There is no paid tier; users bear the cost of the underlying model provider, which the built in cost tracking reports. The team has since released Archon Horizon, a complementary workspace first system for long running formalization across multiple sessions and interdependent projects. The lab's other work includes a complete Lean 4 formalization of the Poincare Conjecture.