25岁广州女孩用AI验成了！两大菲尔兹奖得主心血，无误

TL;DR - Axiom Math says its multi-agent AxiomProver system formalized and verified the human proof that infinitely many prime pairs differ by at most 246. The result demonstrates how AI-assisted Lean 4 formalization can audit complex mathematics and potentially support verification of AI-generated software.

• AxiomProver uses agents for formalization, intermediate-lemma generation, proof search, and translation of machine proofs into human-readable explanations.
• The 132-page formalization encodes the GPY–Maynard sieve argument, including a 50-dimensional optimization and the bound (M_{50,1/25}>4.0043).
• Lean 4 checked the proof chain, which ultimately relies on the Bombieri–Vinogradov theorem and a prime number theorem with an error term; AxiomProver did not discover a new theorem.
• Axiom Math open-sourced the work as PrimeGapsTheory and PrimeGapsCert in its PrimeGapsLib repository for independent verification.