Gauss AI Agent Completes Complex Math Formalization in 3 Weeks, Outpacing Human Effort by 18 Months

Math, Inc. today announced the successful completion of the Strong Prime Number Theorem formalization project by its autoformalization agent, Gauss, in a mere three weeks. This achievement significantly accelerates a task that had seen over 18 months of partial progress by human experts, including Fields Medallist Terence Tao and Alex Kontorovich. The company stated on social media, > "Today we're announcing Gauss, our first autoformalization agent that just completed Terry Tao & Alex Kontorovich's Strong Prime Number Theorem project in 3 weeks—an effort that took human experts 18+ months of partial progress."

Math, Inc. is a newly established company dedicated to autoformalization and the creation of "verified superintelligence." Gauss, their inaugural autoformalization agent, is designed to assist human mathematicians in the rigorous process of formal verification. The agent can operate autonomously for extended periods, substantially compressing the labor traditionally required for top-tier formalization experts.

The Strong Prime Number Theorem project was initiated as a challenge by mathematicians Terence Tao and Alex Kontorovich in January 2024. Their efforts over 18 months faced significant obstacles, particularly in formalizing core difficulties within the field of complex analysis. Gauss's rapid completion of this complex task highlights its advanced capabilities in translating human mathematical concepts into verifiable machine code.

The formalization effort resulted in approximately 25,000 lines of Lean code, encompassing over 1,000 theorems and definitions. While Gauss generated the bulk of the Lean statements and proofs, the project involved human supervision, providing high-level blueprints and reviewing critical lemmas. This scale of formal proof has historically represented major milestones, often requiring multi-year endeavors.

Math, Inc. plans to deploy this technology to working mathematicians and proof engineers, aiming to dramatically increase the total volume of formal code. The company envisions future iterations of Gauss to be even more capable and autonomous, contributing to a new paradigm of "verified superintelligence" and "machine polymaths." The development has received support from DARPA’s expMath program.