Math Inc and Gauss
Last reviewed
Jun 7, 2026
Sources
16 citations
Review status
Source-backed
Revision
v1 · 1,958 words
Improve this article
Add missing citations, update stale details, or suggest a clearer explanation.
Suggest edit
CtrlK
Last reviewed
Jun 7, 2026
Sources
16 citations
Review status
Source-backed
Revision
v1 · 1,958 words
Add missing citations, update stale details, or suggest a clearer explanation.
Math Inc is an artificial intelligence startup founded in 2025 that builds autoformalization tools for mathematics, with the stated mission of creating what it calls "verified superintelligence." Its first product, Gauss, is an AI agent for autoformalization: the task of translating mathematical definitions, statements, and proofs written in natural language into the machine-checkable language of an interactive theorem prover. In September 2025 Math Inc announced that Gauss had produced a complete, machine-verified formalization of the strong Prime Number Theorem in the Lean proof assistant, finishing in roughly three weeks a community project that human experts, including Fields Medalist Terence Tao, had worked on for more than 18 months without completing. The result was widely covered as a landmark for AI for science and automated theorem proving, and also drew measured caution from members of the Lean community about how such results are produced and credited.
Math Inc was incubated at Morph Labs, an AI infrastructure company, and emerged publicly in September 2025. The company was co-founded by Christian Szegedy and Jesse Michael Han.
Szegedy is a research scientist known in deep learning for co-inventing the Inception convolutional-network architecture and Batch Normalization while at Google. He later became a founding scientist at xAI, and in 2019 co-authored a position paper arguing that autoformalization could be a route to machine reasoning that is verifiable by construction. Szegedy left xAI specifically to pursue formalization work and was also an early investor in Morph Labs.
Jesse Michael Han is the founder and chief executive of Morph Labs and is listed as a co-founder and chief executive of Math Inc. As a doctoral student he led, with Floris van Doorn, the Flypitch project, which produced a Lean formalization of the independence of the continuum hypothesis. That earlier work became a recurring point of comparison for the Gauss result. Other contributors named in connection with the prime-number-theorem effort include Jared Lichtman, who helped develop the natural-language blueprint that guided the formalization.
| Fact | Detail |
|---|---|
| Company | Math Inc (also written "Math, Inc.") |
| Founded | 2025; incubated at Morph Labs |
| Co-founders | Christian Szegedy; Jesse Michael Han |
| First product | Gauss, an autoformalization agent |
| Stated mission | "Verified superintelligence" via autoformalization |
| Theorem prover used | Lean |
Formal verification expresses mathematics in a language that a computer can check line by line, so that a completed proof is guaranteed correct by the proof assistant rather than by human refereeing. Lean, together with its mathematics library Mathlib, is one of the most widely used systems for this purpose. The central bottleneck is labor: translating informal mathematics into Lean is slow, exacting work that has historically required scarce human expertise, which is why even well-understood theorems can take many person-months to formalize.
Math Inc frames autoformalization as the missing layer for trustworthy machine reasoning. The idea is that if an AI system can both propose mathematics and render it into a form a proof checker accepts, then its conclusions can be trusted without anyone having to read and audit every step. Gauss is positioned as a tool to compress the formalization bottleneck rather than to replace mathematicians: in its current form it relies on natural-language scaffolding supplied by human experts and on human review of key lemmas and strategies, while the agent generates the Lean statements and proofs. Math Inc has stated a goal of increasing the volume of formally verified mathematics by two to three orders of magnitude within roughly a year of the launch.
The Gauss runs were supported by infrastructure Math Inc calls Trinity environments, developed with Morph Labs. According to the company, the system orchestrated thousands of concurrent agents, each with its own dedicated Lean runtime, running on Morph Cloud's Infinibranch technology and consuming multiple terabytes of cluster memory. This use of large-scale, test-time compute, combined with reinforcement learning infrastructure carried over from Morph Labs, is central to how Gauss differs from a single large language model prompted to write Lean code.
The Prime Number Theorem (PNT) describes the asymptotic density of the primes: the number of primes up to x is asymptotic to x divided by the natural logarithm of x. The strong form, established by Charles-Jean de la Vallée Poussin in 1899, sharpens this by supplying an explicit error term. It states that the prime-counting function differs from the logarithmic integral by a quantity that decays roughly like x times the exponential of negative a constant times the square root of the logarithm of x. Proving this bound requires showing that the Riemann zeta function has no zeros in a region just inside the line where its real part equals one (a "zero-free region"), and then transferring that analytic fact into an estimate on primes by way of complex analysis, including contour integration and the logarithmic derivative of zeta. It is substantially harder to formalize than the ordinary PNT.
The formalization target originated as a community Lean project. In January 2024 Tao and Alex Kontorovich, of Rutgers University, launched the PrimeNumberTheoremAnd project to formalize the prime number theorem together with the surrounding machinery of analytic number theory. The ordinary PNT was completed by that effort, but the strong form with its error term proved difficult; in July 2025 Tao and Kontorovich reported intermediate progress, with the work obstructed by the complex-analysis components, and the project stalled short of the goal.
Math Inc's contribution, released as the open-source repository strongpnt, is an AI-generated Lean development of the strong PNT and the complex-analysis infrastructure its proof requires. The repository reuses definitions and some proofs from the earlier PrimeNumberTheoremAnd project (the "Medium PNT" work), adapting files such as PNT5_StrongPNT.lean and the zeta-zero-free-region material, while four major new files covering complex analysis, the logarithmic derivative, the Riemann zeta function, and the zero-free region were produced by the Gauss agent. By Math Inc's account the humans supplied the high-level blueprint, reviewed critical lemmas, and adapted prior work where needed, and Gauss generated the Lean statements and proofs. Because the final artifact is accepted by Lean, the proof is machine-checked: Lean confirms that the assembled argument is internally valid.
| Metric | Reported figure | Source |
|---|---|---|
| Lean code generated | ~25,000 lines | Math Inc; strongpnt repository |
| Theorems and definitions | ~1,100 | Math Inc; strongpnt repository |
| Time to completion | ~3 weeks | Math Inc |
| Prior human effort | 18+ months (partial) | Math Inc; Tao and Kontorovich |
| Original challenge set | January 2024 | PrimeNumberTheoremAnd project |
| Intermediate human progress | July 2025 | Math Inc; Tao and Kontorovich |
| Announcement | September 2025 | Math Inc |
| Builds on | PrimeNumberTheoremAnd (Lean) | strongpnt README |
To put the scale in perspective, Jesse Han contrasted the effort with his own earlier work: the Flypitch formalization of the independence of the continuum hypothesis took about 12 months and 20,000 lines of Lean, whereas the strong PNT development reached roughly 25,000 lines in three weeks. Math Inc says Gauss can work autonomously for hours at a stretch, compressing labor that had previously been reserved for a small number of formalization specialists.
The announcement drew immediate attention as evidence that AI systems were becoming genuinely useful for research-level mathematics, and it circulated alongside other AI milestones in 2025 as a counterpoint to claims that "AI cannot do math." Math Inc and its founders framed the result as the opening of a period in which the supply of formally verified mathematics could grow by orders of magnitude.
Within the Lean and formalization community the reaction was more qualified. Kevin Buzzard, a number theorist at Imperial College London and a leading figure in the Lean mathematics community, cautioned that there are as yet no guardrails around AI-generated formal proofs. His central point is a subtle but important one: even when Lean certifies that a body of generated code is internally correct, the formal statement that was proved may not faithfully capture the theorem the mathematician intended. In other words, machine-checking guarantees that the proof matches its stated theorem, but not that the stated theorem matches the informal claim it is meant to represent, a gap that places weight on careful human review of the top-level statements.
Commentators and participants also emphasized that the result was a hybrid achievement rather than a fully autonomous one. Gauss's success rested on the natural-language blueprint, the prior PrimeNumberTheoremAnd machinery, and the lemma-level review provided by human mathematicians, many of them early-career researchers, over nearly two years. A recurring concern in community discussion was that framing the outcome as a pure AI victory would understate those contributions. Math Inc's own materials acknowledge the human scaffolding and the reuse of prior work, and the strongpnt repository credits the PrimeNumberTheoremAnd project explicitly.
The Gauss strong-PNT formalization is notable on several fronts. It is one of the first instances in which an AI agent completed a substantial, research-grade formalization that human experts had attempted at length and not finished, and it did so at a pace and scale that would be difficult to reach by hand. It demonstrated a working pipeline in which generative AI produces Lean code, an interactive theorem prover supplies an objective correctness signal, and large-scale parallel compute drives many agents at once, an arrangement that ties together formal verification, automated reasoning, and reinforcement-learning-style search.
The episode also sharpened a debate that the formalization community had been having for some time. If AI can generate machine-checked proofs faster than they can be read, then trust shifts from auditing arguments to auditing definitions and statements, and the social conventions of mathematics, around credit, collaboration, and what counts as a result, come under new pressure. Buzzard's caution about whether a verified statement says what its author thinks it says is likely to remain a live issue as more such systems appear. Following the Gauss launch, Math Inc continued to develop the approach, including releasing an open-source autoformalization agent harness, and the strong-PNT result is best read as an early, concrete data point in the broader project of integrating AI with formal mathematics rather than as a settled verdict on its limits.