AxiomProver, a multi-agent system developed by the startup team Axiom, completed the formal verification of the Classification of Finite Simple Groups theorem in just 24 days. This theorem—crafted by more than a hundred leading mathematicians over more than half a century and spanning 15,000 pages—is known as the "giant theorem," essentially a "periodic table" for all finite simple groups, and is of great value in both mathematics and physics. Previously, because its proof was so vast and complex, it was difficult for humans to read through in its entirety and was prone to errors. AxiomProver built a Lean codebase of over 43 million lines, making it the largest open-source software project currently in existence. During the formalization process, the AI identified hundreds of anomalies, 34 of which were major logical deviations; the core flaw lay in arguments related to the key unbalanced group theorem, and the AI also provided corresponding counterexamples. The team then worked with senior group theory scholars to devise a new proof route, with the AI leading the proof of an entirely new group theory result as a patch, successfully repairing the flaw and completing the verification. This marks the first time AI has become a core collaborator in top-tier pure mathematics research by discovering new theorems and repairing core flaws.