This repository contains an AI-generated Lean formalization of the strong Prime Number Theorem (PNT) and the complex-analysis infrastructure used in its proof.
Most of the statements and proofs were produced by Gauss, an autoformalization agent. The development was completed with targeted human scaffolding and review of key lemmas and strategies. The finished Lean development is substantial (over 25k lines and 1.1k theorems/definitions) and shows how AI agents can accelerate large formalization efforts when combined with human guidance. See Gauss and Math Inc. for more background.
- Target: the strong Prime Number Theorem.
- Generated by the Gauss autoformalization agent, with human supervision.
- Scale: ≈25k lines of Lean and ≈1.1k theorems/definitions.
- Time to completion: three weeks.
Dependency: this development reuses definitions and some proofs from the PrimeNumberTheoremAnd project (Medium PNT). In particular, PNT5_StrongPNT.lean, Z0.lean, and ZetaZeroFree.lean were adapted from that work.
Generated content: PNT1_ComplexAnalysis.lean, PNT2_LogDerivative.lean, PNT3_RiemannZeta.lean, and PNT4_ZeroFreeRegion.lean were produced by the Gauss autoformalization agent with human supervision. Lean statements and proofs were generated by the Gauss agent. Humans provided the high-level blueprint, reviewed critical lemmas, and adapted prior work where needed.
Repository layout:
StrongPNT/- principal Lean source files produced or adapted for this project.blueprint/- LaTeX blueprint and content used by the autoformalizer.
Compile the Lean files (requires Lean):
lake buildBuild the blueprint PDF (requires uv):
uvx leanblueprint pdfBuild and serve the blueprint website:
uvx leanblueprint web && uvx leanblueprint serve