Strong prime number theorem formalized in Lean by an autoformalization agent
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.
- Lab
- Math, Inc.
- Model
- Gauss (autoformalization agent)
- Field
- Mathematics
- Date
- 2025-09-11
- Human collaborators
- Terence Tao, Alex Kontorovich
Sources
Original work
Announcement
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 and known objections
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 ↗
Disagree with these grades?
Bring a citation: a grade moves on evidence, not on argument.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Author verified and AI-assisted.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded author verified for verification and ai-assisted for autonomy. What these mean.
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-pntBibTeX
@misc{whataifound-mathinc-2025-pnt,
title = {Strong prime number theorem formalized in Lean by an autoformalization agent},
author = {{whataifound.org}},
year = {2025},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Math, Inc.. Verification: Author verified. Autonomy: AI-assisted.},
url = {https://whataifound.org/finding/2025-09-11-gauss-strong-pnt}
}