The strongpnt repository contains an AI-generated Lean formalization of the strong Prime Number Theorem and its supporting complex-analysis infrastructure. Most of the statements and proofs were produced by Gauss, an autoformalization agent developed by Math Inc., with targeted human scaffolding and review. The finished development spans over 25,000 lines of Lean code and includes approximately 1,100 theorems and definitions, demonstrating how AI agents can accelerate large formalization efforts when combined with human guidance. The project reuses some definitions and proofs from the PrimeNumberTheoremAnd project and was completed in three weeks.