Archon

Archon

Frenzymath · PKU @ AI4Math

*Autonomous formalization of research-level mathematics in Lean 4*

We just released Archon Horizon, a workspace-first orchestration system for long-running Lean 4 formalization with Codex or Claude Code. Horizon is a complementary alternative to Archon, designed for long-horizon agents working across multiple sessions and interdependent projects. Check it out.
✨✨ Archon v0.3.3. Dashboard, workflow, and safety polish. Project scoping & roadmap: a Scope Home view with interactive status checklists and an archon scope roadmap agent that condenses the plan into milestones. Cost visibility: per-operation and turn-level token + USD tracking in the log viewer. Static export (archon dashboard --static-build) publishes a self-contained dashboard to GitHub Pages. Multi-project: a project switcher and a Meta DAG union view across peers. Workspace-only safe mode (archon loop --safe) keeps commands automatic while using the native Claude Code or Codex filesystem sandbox to prevent writes outside the active project. The DAG view gains a layered-by-depth layout, and the dashboard now works behind a path-prefix reverse proxy. Carries forward every 0.3.1/0.3.2 fix.
🔄 Upgrading from v0.1.0 or v0.2.0? Just run archon update once and then archon init in existing projects. *Please, first backup your work!*
⌛️ Upgrading from even before? See MIGRATION.md.
📝 Full release notes: CHANGELOG.md.

Archon is an agentic system that autonomously formalizes research-level mathematics in Lean 4. A plan agent provides strategic guidance while prover agents write and verify proofs — separating analysis from execution to avoid context explosion. The system handles repository-scale formalization through three phases: scaffolding, proving, and polish. By default,…