AI formalizes Strong PNT in Lean

Math, Inc.’s 'Gauss' agent reportedly completed the Strong Prime Number Theorem formalization in Lean in about three weeks, clearing complex‑analysis hurdles that Terence Tao and Alex Kontorovich had flagged. The public artifact includes ~25k lines of Lean, ~1.1k theorems/definitions, and a blueprint; the team says 'most statements and proofs were produced by Gauss' with human scaffolding. The work was funded under DARPA’s expMath program. — If AI agents can complete frontier‑level formalizations, norms for proof, peer review, and math education may need to adapt as automated, machine‑checked proofs become a standard path for advancing hard theorems.