TLDR; AI is about to flood the world with code, proofs, and machine-generated decisions. Almost none of it will be meaningfully audited. If output scales exponentially while trust does not, the scarce asset becomes correctness.

We’re witnessing a watershed moment where software writes software, models discover research, and agents deploy systems faster than any human team can audit them. This results in a structural problem. Investing in Math Inc is a bet that verification becomes the gating mechanism of the AI era.

1. What is Math Inc?

Humanity advances whenever individuals gain the capacity to verify truth for themselves, without institutional permission.

Before Galileo looked through a telescope, the structure of the heavens was a matter of authority — ecclesiastical, philosophical, traditional. After he looked, it was a matter of observation. Anyone with the instrument could check. The moons of Jupiter did not require papal approval. They were simply there.

This pattern repeats. The printing press did not merely spread information; it made the suppression of ideas ruinously expensive. The scientific method did not merely produce knowledge; it created a formal grammar in which a lone experimenter could overturn consensus. Most recently, formal verification has allowed mathematics and software to be certified by anyone with access to the tools, regardless of standing or station.

In each case, the decisive advance was not primarily in what was known, but in who could verify it. The distribution of verification capacity is the distribution of sovereignty.

II.

Ultimately, centralized authority inevitably accumulates incentives that distort the very knowledge it was meant to protect. In time, the guardians of knowledge become its bottleneck.

Alexander Grothendieck understood this early.

Raised by Russian-Jewish anarchists, Grothendieck was born an outcast. The internment and eventual death of his father at Auschwitz, and the broader persecution of Jews in prewar Europe, provided an early and concrete lesson: governments and institutions systematically misrepresent reality for their own gain. These failures are correlated, and reliance on them produces errors that lead towards catastrophe.

When he encountered mathematics, he treated it the way he treated everything else — with suspicion of received wisdom and an insistence on seeing the truth for himself. In the years 1945 to 1948, working in isolation in Montpellier without access to the major centers, he independently rediscovered large portions of measure theory, not knowing the work had already been done. A conventional mind would have regarded this as wasted time. Grothendieck regarded it as the most important period of his life. He had learned to reach for things in his own way, rather than relying on the notions of a consensus, overt or tacit, that claimed authority over what was worth thinking about.

By working at the right layer of abstraction, he uncovered structures that made entire classes of problems tractable. His revolution in algebraic geometry was, at its core, an act of compression: refactoring the entire codebase of algebra, geometry, and number theory into a unified framework. The introduction of schemes, topoi, and étale cohomology did not merely add new results to the existing edifice. It reorganized the edifice itself, so that problems which had resisted decades of effort became consequences of the architecture.

Late in life, reflecting on colleagues whom he acknowledged as more brilliant than himself, Grothendieck observed that their imprint on mathematics had not been very profound. They had done beautiful things, he wrote:

“in a context that was already set out before them, which they had no inclination to disturb. Without being aware of it, they had remained prisoners of those invisible and despotic circles which delimit the universe of a certain milieu in a given era.”

To break those bounds, they would have had to rediscover in themselves a capability that was their birthright:

The capacity to stand alone.

III.

Sovereignty, in politics, is the right to make individual decisions without relying on institutions. In mathematics, sovereignty takes a different form: the ability to individually verify that proofs are correct without an institutional stamp of approval. In both politics and math, collective decisions — proof correctness, how resources should be allocated — come from consensus. Sovereignty ensures that consensus can be reached without institutional coercion, as individuals can independently vote as part of the collective.

The question is whether this capacity can be made general — whether instruments exist, or could exist, to extend the regime of self-verification beyond the rare genius and into the infrastructure of civilization itself. To answer this, one must look at what has happened to mathematics since Grothendieck’s time — who saw where mathematics was heading.

The last mathematicians who could hold the whole of the field in a single mind were Hilbert and Poincaré, roughly a century ago. Since then, mathematics has grown beyond any individual’s capacity to comprehend. Even the greatest living mathematician commands only a fraction. Fragmentation follows not only from bad incentives but from the sheer scale of what has been built.

The pathology Grothendieck diagnosed in his peers — the invisible despotic circles, the unexamined boundaries, the absence of inclination to disturb — was not simply a failure of individual courage. It was a structural condition accelerated by the same institutions that were supposed to nurture the discipline. Unable or unwilling to judge what is important, the academy counts citations instead. Unable to maintain standards without appearing exclusionary, it abandons standards. Unable to render collective judgment, it retreats into procedure.

The result is a quiet centrifugal motion. Mathematics continues to produce extraordinary work — arguably more, and at a higher level, than at any point in history. But the subfields drift apart. The journals multiply. The conferences specialize. And the capacity of any one mathematician, or even any one community of mathematicians, to assess work outside its immediate neighborhood diminishes with each passing decade. This is nobody’s fault. It is the consequence of success: the edifice has grown larger than any individual can survey.

But the consequences are real. Consider the ABC Conjecture. In 2012, Shinichi Mochizuki released a proof spanning over five hundred pages, written in a framework of his own devising that almost no mathematician on earth had the background to evaluate. More than a decade later, the community has not reached consensus on whether the proof is valid. The difficulty is not that mathematicians are unwilling to do the work. It is that the work required to verify this single claim may exceed what the existing social infrastructure of mathematics can coordinate. This is a new kind of problem — not a failure of rigor within any subfield, but a failure of reach across them.

Grothendieck’s contribution had been to insist on the unity of mathematics — to show that algebraic geometry, number theory, and topology were aspects of a deeper structure. Hilbert, Poincaré, Langlands — the vision was always the same. Mathematics is one thing. The task is to see it whole. When that vision recedes — not because anyone rejects it, but because the sheer scale of the enterprise makes it harder and harder to sustain — something important is lost.

When verification becomes practically impossible, sovereignty is quietly extinguished, and what remains is trust, deference, and a dependence on authority that mathematics, of all disciplines, was supposed to render unnecessary.

IV.

The crisis of verification is not confined to mathematics. It is the defining condition of the modern world.

We live in a civilization mediated by software that almost no one can read and no one can fully audit. The financial system, the power grid, the communication networks, the AI systems now being deployed at civilizational scale — all of it runs on code whose correctness is, in practice, taken on faith. When a government demands a backdoor in an encryption protocol, or a technology company deploys an algorithm that shapes the beliefs of billions, the question is not whether these systems are trustworthy. The question is whether anyone is in a position to check. Usually the answer is no. The sovereignty problem that Grothendieck diagnosed in mathematics — invisible dependence on authority, verification beyond the reach of any individual — is now the general condition.

The cypherpunk movement recognized this early. Code creates jurisdictions: a cryptographic protocol holds regardless of what any government decrees. But without the means to verify that the code itself is correct — that it does what it claims and nothing else — sovereignty remains incomplete. You have traded dependence on one institution for dependence on another. The lock on the door is only as trustworthy as the locksmith.

Here the Curry-Howard correspondence becomes decisive. Proofs are programs and propositions are types. Mathematics is not merely like software; it is software at the foundational level. This means that the capacity to verify a mathematical proof and the capacity to verify that a piece of software is correct are not analogous skills. They are the same skill. A system that can formalize and check mathematical proofs can, in principle, verify code, audit protocols, and confirm the reasoning of AI systems. Mathematical sovereignty and software sovereignty are one thing.

Autoformalization is the instrument through which sovereignty can be exercised at scale.

It is against this backdrop that one must consider what is being built in the emerging field of AI-driven formal mathematics.

Open-source worked for decades because transparency enabled human verification. But the most useful open-source systems today (for example, Linux and Kubernetes) are already too large for anyone to audit comprehensively. Trust is mostly historical, and AI-generated code accelerates this problem dramatically.

At the same time, modern infrastructure encodes increasingly complex behavior — distributed systems and cryptography — so the real bottleneck is specification. As AI writes more code, open-source will need large, evolving formal specifications that precisely define how systems should behave. Proof assistants like Lean make those guarantees machine-checkable, but writing them has historically been too expensive. AI-powered autoformalization changes that, making it possible to scale verification with the size of modern codebases.

Math Inc solves this issue.

On the surface, it is a technology company pursuing the formalization of mathematics at industrial scale. Today, the Lean library Mathlib contains the equivalent of roughly fifty textbooks. The aim is a corpus a hundred times larger, continuously expanded and compressed by human and artificial agents working together.

Math Inc is building the verification infrastructure for an AI-native economy. As AI systems generate millions of lines of code, mathematical proofs, and scientific designs, the bottleneck around scale becomes trust. The outputs are too large and too complex for humans to reliably audit, yet AI-generated code will increasingly power critical infrastructure, financial systems, cryptography, and autonomous machines.

Their thesis is simple: verification scales as a function of AI generation. Every dollar spent on AI-produced code creates a corresponding need to confirm that code is correct. So, Math Inc treats verification as core infrastructure: the layer that makes large-scale autonomy economically and socially viable.

Their first product is Gauss, an autoformalization agent. Since the founding of Math Inc last year, Gauss has synthesized each in three weeks:

• June 2025: 3,500 lines (de Bruijn theorem on the ABC conjecture)

• September 2025: 25,000 lines (Strong Prime Number Theorem)

• February 2026: 200,000 lines (Sphere packing in dimensions 8 and 24 — Viazovska’s Fields Medal result)

Math Inc is scaling verification exponentially: each cycle formalizes an order of magnitude more mathematics in the same time. As a point of comparison, human teams often take a decade to complete verification projects spanning 500,000 lines of code.

What impressed us most about Math Inc versus competitors was the depth of Gauss’s technical performance on sphere packing formalization. The 8-dimensional case had already required a team of seven and an estimated six more months to complete with existing tools. Gauss extended the existing 20k LOC codebase with another 60k LOC to finish it in five days and then autonomously solved the 24-dimensional case from arXiv papers, with no manual intervention and faster than its human counterparts.

The space has attracted significant capital and talent, but the competitive landscape has focused largely on competition benchmarks — Olympiad problems, Putnam questions, problems with clean statements and known solutions. Math Inc and the neolabs are operating in the same broad category — AI for formal mathematics, but they’re optimizing for different end states.

The neolabs have leaned heavily into benchmark visibility, particularly competition-style performance (e.g., Olympiad-level problem solving), which makes for a strong business development strategy and brand for the autoformalization space. That strategy builds their credibility quickly, but it also risks commoditization as other labs replicate benchmark gains. Competition-grade theorem proving is increasingly reproducible. The harder challenge is extending these systems to large, structurally novel proofs.

Math Inc is focused on industrial-scale autoformalization — long-horizon synthesis of large bodies of mathematics directly from primary sources. Math is currently world-class at long and complex proofs versus their competitors; they are not just scaling reasoning, rather they are expanding the horizons of proofs they can solve.

Industrial-grade autoformalization — the kind required to verify software at scale, to formalize mathematics from primary sources, to build the verification layer for an AI-driven economy — is a different problem. Nobody is building for it.

Gauss running for days to generate six-figure-line formalizations is qualitatively different from solving curated problem sets. The bet is that large-scale structural formalization, library management, and governance create compounding data and integration advantages that are harder to copy. Math is working at the frontier of mathematics and is trying to build the infrastructure layer beneath real-world verification. The tradeoff is visibility versus depth: the neolabs win on optics today; Math may win if they can interlink scale and integration.

To us, this ability demonstrates an exceptional, unchallenged benchmark of progress and showcases Math’s compounding growth and advantages. The avant-garde sphere packing proof in 24 dimensions will be the largest singular autoformalization ever created; this results in a virtuous cycle whereby each new formalization extends Math’s library. The extended library provides richer training signals. Richer training produces more capable agents. More capable agents formalize harder results. The loop compounds.

VI.

At Robot, we are doubling down on Math Inc for a few reasons:

Technology and leadership. Math Inc has repeatedly set the pace for the field. Their formal proof of the Strong Prime Number Theorem was a landmark achievement. Trinity — a 3,500-line formalization of the de Bruijn theorem showing that the ABC conjecture holds almost always — applied autoformalization to a central open problem in number theory at unprecedented scale. Their more recent formalization of the FRI security protocol shows what sovereign infrastructure actually looks like: a cryptographic primitive whose correctness can be mechanically verified by anyone, without trusting its authors. Alongside deep collaborations with mathematicians like Terrance Tao, this work has helped define the direction formal mathematics is heading.

Team. Math Inc has assembled something unusual: researchers and engineers (Jesse Han, Alex Gu, Auguste Poiroux) from frontier AI labs alongside first-rate mathematicians (Cameron Freer, Jared Lichtman), together with a cadre of bright, interdisciplinary young builders (Dean Cureton) — what the company calls “math engineers” — who are inventing the discipline of engineering mathematical infrastructure at a planetary scale as they go. This is the team the moment demands. Recent breakthroughs in autoformalization and AI-driven theorem proving suggest that the race toward large-scale mathematical formalization — and ultimately mathematical superintelligence — is just beginning. In a landscape of rapidly shifting technological headwinds and tailwinds, the advantage belongs to teams that are nimble, mission-driven, and deeply technical. Math Inc is that team.

Results. Where competitors optimize for competition benchmarks, Math Inc. has executed on research mathematics at scale. Their formalization of the 8 and 24-dimensional sphere packing problem — over 200,000 lines of high-quality Lean code, completely formalizing the 2022 Fields Medal-winning proof of Maryna Viazovska — is the largest and most significant formalization of a major mathematical result ever completed. This is not a benchmark. It is the proof that the approach works.

Grothendieck’s birthright — the capacity to stand alone, to verify for oneself, to know without asking permission — has been, for most of history, the province of rare genius. The ambition of Math Inc. is to make it infrastructure.

The old lesson was that the truth will set us free.

The deeper lesson, earned by long experience of what institutions do with the truth they control, is different.

We must first set the truth free.

This piece was co-authored with Tarun Chitra, Jesse M. Han, and Jared D. Lichtman.