This project is an AI-generated Lean formalization of the strong Prime Number Theorem (PNT) together with the complex-analysis infrastructure required for its proof. Most statements and proofs were produced by Gauss, an autoformalization agent, with targeted human scaffolding and review of key lemmas and strategies.

The formal development (≈25k lines, ≈1.1k theorems/definitions) demonstrates how formalization agents, guided by expert mathematical scaffolding, can condense many months or years of formalization work into just a few weeks.