Math Inc’s Gauss agent completes the Strong Prime Number Theorem formalisation in Lean in three weeks
Result confirmed
Importance: major (4 of 5)The takeaway
Math Inc (Christian Szegedy) announced that its autoformalization agent Gauss completed Terence Tao and Alex Kontorovich’s Strong Prime Number Theorem project in Lean in about 3 weeks, producing ~25,000 lines of Lean and over 1,000 theorems and definitions.
Status
- Claim
Result confirmed
- Our reporting
- High confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 29 September 2026
Your AI and this story
- GPT-6 AstraIn its training data
- Claude Opus 5.5In its training data
- Gemini 4 HydrogenIn its training data
- Grok 4.7In its training data
It happened before the cutoffs of all four assistants, so it can be in their training data.
Key facts
- ~25,000 lines of Lean, 1,000+ theorems and definitions, code public on GitHub
- Human project began in 2024 and had stalled on complex-analysis prerequisites
- Announcement day approximate (10–11 Sep 2025)
What happened
Gauss read the human blueprint of the Strong PNT project and wrote the missing Lean formalisations, including a large amount of complex analysis.
Why it matters
Autoformalization at this scale points to a future where new proofs, including AI-generated ones, are routinely machine-checked. That matters as AI floods mathematics with claimed proofs.
Sources
3 sources from 3 sites. Numbers match the chips in the text.
3 sources: 3 primary
Primary
- Math Inc: Gaussmath.inc, official
- GitHub: math-inc/strongpntgithub.com, code
- Math Inc announcement on Xx.com, official
Changes
- Filed