Strong prime number theorem formalized in Lean by an autoformalization agent
Strong prime number theorem formalized in Lean by an autoformalization agent is graded author verified on whataifound.org, with the AI's role graded ai-assisted.
An agent completed a Lean formalization of the strong prime number theorem in about three weeks, finishing a project two expert mathematicians had left blocked after 18 months.
- Verification
- Author verified
- Autonomy
- AI-assisted
- Lab
- Math, Inc.
- Model
- Gauss (autoformalization agent)
- Field
- Mathematics
- Date
- 2025-09-11
- Human collaborators
- Terence Tao, Alex Kontorovich
- Notability
- 49 Wikipedia language editions
What was found
Tao and Kontorovich began a Lean formalization of the strong prime number theorem (the version with an explicit error term) in January 2024, and by July 2025 had announced intermediate progress blocked on core difficulties in complex analysis. Math, Inc. reports that Gauss produced over 25,000 lines of Lean and roughly 1,100 theorems and definitions in about three weeks, completing the project. The repository README states that most statements and proofs were produced by the agent, with humans supplying the high-level blueprint, reviewing key lemmas, and adapting prior work.
Novelty check
The prime number theorem is not new mathematics; the contribution is formalization. What was open was whether this particular formalization could be completed, and the surrounding claim is about speed. Recorded because formalization at this scale is a distinct kind of contribution and because the AI finished work humans had started and stalled on, rather than producing a new theorem. Prior art is the PrimeNumberTheoremAnd project itself, which this build reuses and which the README credits.
Caveats
This is a formalization result, not a mathematical discovery: no new theorem was proved. The comparison to '18+ months' is not like-for-like: Tao and Kontorovich worked intermittently, and the repository explicitly reuses definitions and some proofs from their earlier PrimeNumberTheoremAnd project. Math, Inc.'s announcement states the agent 'relies on natural language scaffolding supplied by human mathematicians, and requires high-level expert guidance'; the proportion of human effort is not quantified, and neither Tao nor Kontorovich is quoted in it. Graded author-verified rather than formal: the artifact is public and Lean-checkable, but the README does not itself assert a sorry-free build and no independent audit of that is on the public record. Vendor-announced, so the framing carries the usual caution.
Independent checks
Public Lean artifact (not independently audited): repository public and machine-checkable; README reports the development finished · link ↗
Sources
How this is graded
whataifound.org grades every entry on two axes: verification (how solid the result is, from a machine-checked proof down to refuted) and autonomy (how much the AI did versus its human collaborators). This finding is author verified and ai-assisted. Full definitions are in the methodology.
Cite this entry
whataifound.org (2025). Strong prime number theorem formalized in Lean by an autoformalization agent. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2025-09-11-gauss-strong-pnt