Math Inc's Gauss agent completes the Strong Prime Number Theorem formalisation in Lean in three weeks

2025-09-10★★★★scienceMath Incconfidence: high

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. Human experts had worked on the project for 18+ months.

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)

Science result

Field: mathematics / analytic number theory / formal verification
Problem: Formalising the strong Prime Number Theorem (with error term) in Lean
Result: Complete machine-checked formalisation produced largely by an AI agent in 3 weeks.
AI system: Gauss
Human role: AI-assisted: agent wrote most Lean code from the human blueprint; humans supervised
Verification: Formal proof in Lean (compiles against Mathlib)
Status: confirmed
Why surprising: Weeks of agent time finished a formalisation that expert humans had been working on for a year and a half.

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.

Changelog

2026-09-29: created

Related events

2025-12-06AxiomProver produces machine-checked Lean proofs for all 12 Putnam 2025 problems ★★★
2026-03Math Inc's Gauss formalises Viazovska's sphere-packing proofs in dimensions 8 and 24, fixing errors in the originals ★★★★

Sources (3)

id: 2025-09-10-math-inc-gauss-strong-pnt · updated 2026-09-29 · open in the interactive timeline