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.

Fields Medallist Terence Tao and Alex Kontorovich set this formalization challenge in January 2024. After 18 months, they announced intermediate progress in July 2025 but were blocked by core difficulties in complex analysis. Gauss broke through these barriers autonomously.

We're entering a Golden Age where anyone can summon artificial mathematicians for research. As verified math becomes the training ground for AI, we're creating machine universalists that will transcend human limitations—the von Neumanns of the digital age. https://math.inc/vision

Mathematics is the universal language of computation. Agents trained on formal math will revolutionize verified software, protein design, chip optimization, and disease cures—all while providing scaffolding for aligned superintelligence. Solve math, solve everything.

Gauss is entering beta testing with select mathematicians. Blog: https://math.inc/gauss GitHub: https://github.com/math-inc/strongpnt… Early access: https://math.inc/early-access

We are hiring a small team of extraordinarily aligned and capable researchers and engineers: https://math.inc/careers

Built with support from DARPA's expMath program and @Morph Trinity environments infrastructure.