AI Agent Gauss Formalizes Prime Number Theorem in Record 3 Weeks, Outperforming Human Experts

San Francisco – Math Inc. has announced the launch of Gauss, a pioneering autoformalization agent that successfully formalized the strong Prime Number Theorem (PNT) in Lean, a formal proof language. This significant mathematical achievement was completed in just three weeks, a task that had previously challenged leading mathematicians, including Fields Medallist Terence Tao and Alex Kontorovich, for over 18 months. The announcement was highlighted by engineer and essayist Stephen Pimentel, a member of the Math Inc. team, who shared the news on social media.

Gauss autonomously generated approximately 25,000 lines of Lean code, encompassing over 1,000 theorems and definitions. This rapid formalization demonstrates a dramatic compression of the labor typically required for such complex mathematical verification. The project also formalized key missing results in complex analysis, opening new avenues for future initiatives previously deemed unapproachable.

The development of Gauss was significantly supported by large-scale infrastructure provided by Morph Labs, utilizing their Infinibranch on Morph Cloud. This infrastructure was crucial for scaling Lean verification environments to manage thousands of concurrent agents and multiple terabytes of cluster RAM. Math Inc. anticipates that future iterations of Gauss will achieve even greater autonomy and capability.

Math Inc. plans to deploy this technology to assist working mathematicians and proof engineers, with early access already being offered to a select group of mathematicians for beta testing. The company aims to increase the total volume of formal code by two to three orders of magnitude within the next year, envisioning a new paradigm in mathematical verification driven by verified superintelligence and machine polymaths. The project received support from DARPA’s expMath program.