---
id: "2025-09-10-math-inc-gauss-strong-pnt"
url: "https://postcutoff.com/e/2025-09-10-math-inc-gauss-strong-pnt/"
as_of: "2026-11-13T13:49:00+01:00"
date: "2025-09-10"
date_precision: day
category: science
importance: 4
confidence: high
status: [Result confirmed]
verification: Lean-verified
sources: 3
editor: human editor
human_review: null
version: "2026-10-04"
---

As of: 2026-11-13 13:49 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2025-09-10-math-inc-gauss-strong-pnt/

# Math Inc's Gauss agent completes the Strong Prime Number Theorem formalisation in Lean in three weeks

Math Inc (Christian Szegedy) announced that its autoformalization agent Gauss completed Terence Tao and Alex Kontorovich's Strong Prime Number Theorem project in Lean in about 3 weeks, producing ~25,000 lines of Lean and over 1,000 theorems and definitions. Human experts had worked on the project for 18+ months.

## Key facts
- ~25,000 lines of Lean, 1,000+ theorems and definitions, code public on GitHub
- Human project began in 2024 and had stalled on complex-analysis prerequisites
- Announcement day approximate (10–11 Sep 2025)

## What happened

Gauss read the human blueprint of the Strong PNT project and wrote the missing Lean formalisations, including a large amount of complex analysis.

## Why it matters

Autoformalization at this scale points to a future where new proofs, including AI-generated ones, are routinely machine-checked. That matters as AI floods mathematics with claimed proofs.

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): in its training data
- Claude Opus 5.5 (training cutoff June 2026): in its training data
- Gemini 4 Hydrogen (training cutoff March 2026): in its training data
- Grok 4.7 (training cutoff May 2026): in its training data

## Sources

1. [Math Inc: Gauss](https://www.math.inc/gauss) (math.inc, official)
2. [GitHub: math-inc/strongpnt](https://github.com/math-inc/strongpnt) (github.com, code)
3. [Math Inc announcement on X](https://x.com/mathematics_inc/status/1966194751847461309) (x.com, official)

## Changes

- 2026-09-29 (filed): Created

## Related

- 2025-12-06: [AxiomProver produces machine-checked Lean proofs for all 12 Putnam 2025 problems](https://postcutoff.com/e/2025-12-06-axiomprover-putnam-2025/index.md)
- People: [Terence Tao](https://postcutoff.com/person/terence-tao/)
- Archived: 1 post, listed in https://postcutoff.com/e/2025-09-10-math-inc-gauss-strong-pnt/index.json