Archon
#18 in Reasoning-ModelleUnknown · seit March 13, 2026 (Blog-Announcement "Archon: An Agentic System for Formalizing Research-Level Mathematics") · 2× · zuletzt 05. Nov. 2026
24
Momentum
Archon ist ein agentisches System der FrenzyMath-Gruppe (PKU BICMR, AI4Math), das research-level Mathematik autonom in Lean 4 formalisiert. Es arbeitet mit Plan- und Prover-Agenten und nutzt das Suchwerkzeug LeanSearch. Die Software ist Open Source unter Apache-2.0. Es handelt sich um ein Harness/Orchestrierungssystem, nicht um ein eigenständiges Modell mit eigenen Modellspezifikationen.
Momentum-Verlauf
07.08.05.11.
Features
| Lizenz | Apache-2.0 |
| Plattform | Claude Code-basiertes Harness; Lean 4 / Mathlib; Codex optional (ab v0.3.0) |
| Release-Datum | 13. März 2026 (Blog-Announcement, Open-Source-Release) |