A new dawn.

Those who are paying close attention can sense the dawning of a new Golden Age in mathematics.

Current AI models already solve mathematical problems over short-horizons. These skills would have astonished the experts of a few years ago. This next year will birth agents that can collaborate and work continually over far longer time horizons. In 18 months we will see the first wave of breakthroughs in a rising sea of mathematics.

Over the past decade, online crowdsourced 'polymath' projects pushed the boundary of large-scale mathematics. In recent weeks, we are glimpsing a broadening of this paradigm to both human and machine. With proper execution, we will enter into a Golden Age, in which anyone will be able to summon a society of artificial mathematicians, growing their own research idea into a large polymathic initiative.

A vision of mathematics, verified.

This vision unites AI advancement with the rise of formally verified mathematics. Verification is simply the guarantee of correctness. But upon such simplicity, we can build enduring knowledge. One need not know the details of a proof to trust its result, once verified. This opens up the prospect of massive collaboration, leveraging modular parts for re-use. Just as the Industrial Revolution scaled systems through division of labor, so too will the digital age scale knowledge itself, with parallelized verification as its core.

The natural substrate for artificial mathematicians will be formal libraries at industrial scale. Today, the Lean library Mathlib contains the equivalent of fifty textbooks of mathematics. Tomorrow's library will be a hundred times larger — greater still when we incorporate software, computation, and the scientific artifacts of modern research.

Beyond their intrinsic value, verified proofs double as clear reward signals for reinforcement learning. Thus mathematics itself becomes a dynamic training environment.

Additions of new proofs grow the repository into an expanding network of results, and their significance is measured by their connectivity and influence within that network. Coveted additions, like the Riemann Hypothesis, would immediately prove hundreds of theorems downstream.

Moreover, new definitions in the repository allow for compression and unification across domains. Indeed, the 1960s Grothendieck Revolution introduced key definitions that refactored the entire codebase of algebra, geometry, and number theory into a unified modern framework. This proved essential for Fermat's Last Theorem and other breakthroughs.

Thus mathematics may be distilled into the dual objectives of expansion and compression. Expansion pushes the frontier outward with new results; compression refactors the interior under unifying abstractions. We will train agents to seek and produce mathematics with high network value.

This creates a virtuous cycle: as agents enhance in capability, the repository scales up with optimized compression. In turn, the agents grow symbiotically within their ecosystem.

A century ago, Hilbert and Poincaré were the last true universalists who had mastered every field of mathematics of their day. Now, even the greatest living mathematician comprehends only a fraction of the whole. Thus formalization agents trained on the entire corpus of mathematics will give rise to the machine universalists.

Yet this emergence of machine universalists does not diminish the mathematician's role — it amplifies it. Just as Grothendieck's abstractions didn't replace mathematical thinking but elevated it, allowing mathematicians to work at higher conceptual levels while hiding algebraic complexity, AI formalization will serve as the ultimate abstraction layer. Mathematicians will be liberated from computational drudgery to focus on what only human intuition can provide: the creative leaps, the right questions, the recognition of deep patterns. When von Neumann saw game theory emerge from economics' chaos through the minimax theorem, he demonstrated how the right abstraction transforms messy domains into rigorous mathematics. AI agents will handle verification and explore vast implication spaces, while mathematicians do what they do best — imagine new mathematical worlds.

Solve math, solve everything.

As the modern world becomes increasingly computationally encoded, the entire planet becomes the training ground for verified superintelligence.

Mathematics itself paves the way forward, as the universal language of science and of computation. Formalization agents trained on math will be able to rapidly produce formal code and refactor verified codebases. Formal verification of software is already used in mission-critical settings in industry and national security. But our vision extends far beyond this to impact all areas connected to the digital realm. The fundamental challenges we face in the 21st century are complex systems with millions of coupled components: distributed systems, high-resolution simulations of cells, all the way to superintelligence itself. They exceed human comprehension to model and construct as complete wholes. Formal mathematics provides a scalable, trustworthy technology to systematize science into verified models and software, enabling machine intelligence to draft verifiable code for such complex systems, which will transform multiple domains while providing scaffolding for verified AI agents and ultimately superintelligence aligned by default.

The next generation of reasoning agents will discuss the hardest science and engineering problems with precision, producing clean code and verifiable solutions for protein design, material science, chip optimization, and disease cures — all while self-improving at a predictable pace with formal correctness guarantees that make their reliability inevitable. Current AI produces impressive but fundamentally untrustworthy outputs requiring costly validation; we will eliminate this limitation entirely by requiring all solutions to satisfy both verification — logical adherence to formal specifications — and validation — conformance to informal task constraints, creating systems that continuously verify and validate themselves in a demonstrable and guaranteed manner.

This approach bootstraps from mathematics understood as the self-referential foundation of all computable reality — any problem specifiable unambiguously and verifiable through pure logic, encompassing program behavior, chip verification, game strategy, protein folding, and AI algorithm development itself. By formalizing the entirety of human mathematics rather than merely learning to autocomplete math text, our agents will transcend human limitations: developing entirely new mathematical frameworks in depth, analyzing myriad cases while reasoning probabilistically about high-dimensional phenomena, and discovering patterns that open up previously intractable problems.

History is punctuated by the rare polymaths who transcend the boundaries of knowledge. Archimedes passed from mathematics to physics and armaments. Leibniz wove together philosophy, logic, and calculus. Von Neumann laid mathematical foundations for quantum mechanics, economics, and biology. While pioneering computer architecture, he moreover foretold of an “essential singularity” in technological progress.

In the 20th century, von Neumann's mathematical frameworks revolutionized entire scientific disciplines. In the 21st century, formal mathematics will birth machine polymaths, as the culmination of von Neumann’s vision. They will condense verifiable insights from massive formal databases across domains, and ultimately bend the arc of history.

Math, Inc.