AxiomProver Formalizes 15,000-Page Theorem in Lean

This is less a chatbot demo than a new software architecture for mathematical research: parallel agents generate, integrate, and verify enormous bodies of dependent code.

• –The swarm coordinated 108 milestones and roughly 380 subtasks instead of producing isolated proof snippets.
• –Lean turns probabilistic model output into independently checkable artifacts, with humans still reviewing specifications and difficult mathematical gaps.
• –Formalization exposed 34 deviations in published arguments, showing that verification can uncover new mathematics rather than merely transcribe old work.
• –The engineering bottleneck shifts toward dependency graphs, shared libraries, cached builds, and integration—the same problems agent swarms face in large software repositories.
• –For AI developers, this is a compelling template for fleets of coding agents governed by a deterministic test or proof system.