AI Solves Prime Number Puzzle That Stumped Mathematicians for Years

Math Inc. has announced the launch of Gauss, an AI-powered agent designed to assist mathematicians in the formal verification of proofs — a process that converts human-written mathematics into verifiable machine code. The company says Gauss has already achieved a landmark feat: completing the Prime Number Theorem (PNT) challenge set in January 2024 by Fields Medalist Terence Tao and mathematician Alex Kontorovich.

Formalising advanced mathematics has long been considered a “grand challenge,” requiring years of effort from scarce experts. Tao and Kontorovich themselves reported partial progress in July 2025, slowed by hurdles in complex analysis.

Gauss, however, was able to complete the formalisation in just three weeks, autonomously producing around 25,000 lines of Lean code and more than 1,000 theorems and definitions. By comparison, some of the largest formalization projects in history have taken over a decade to complete and produced only an order of magnitude more code.

The achievement was made possible by the Trinity environments infrastructure, developed with Morph Labs, which scaled Lean verification to thousands of concurrent agents consuming terabytes of memory.

While Gauss still relies on natural language scaffolding and expert oversight, Math Inc. expects future versions to become more autonomous. Beta testing with select mathematicians is already underway, and early access is open for registration.

The company says Gauss is only the beginning, predicting a 100–1,000x increase in formalized code over the next year — laying the foundation for what it calls a new era of “verified superintelligence.”