Towards the mathematical singularity

For most of recorded history, civilization's bottleneck was production. However, we are now in the trillion-token present, where the cost of using AI to produce output has dramatically fallen. We're witnessing a watershed moment where AI can create software, develop research, and architect systems faster than humans can audit them. Production scarcity has flipped into excess: verification is the bottleneck and trust is the constraint. The default state of knowledge becomes machine-verifiable and continuously updated: what can't be verified won't be trusted, and what isn't trusted won't be used.

Why Mathematics

At Math, Inc., our goal is to develop systems for this trillion-token present. As our name implies, mathematics is the best substrate to begin with: it is pure, compositional, and without side effects. In mathematics, outputs can be formally verified, errors can be localized, and progress is unambiguous. Our 200,000-line formalization of the Fields Medal-winning proof of the sphere packing problem demonstrates what this looks like in practice: projects that once required years of coordinated effort now take only days. Today, a substantial body of modern mathematics is already within reach of Gauss, our formalization engine.

A Research Agenda

Moving forward, we are scaling autoformalization to all of existing mathematics and beyond, requiring an ambitious and interdisciplinary research agenda.

Programming Languages. The current generation of formal systems remains limited by their origins as manual proof assistants, creating a fundamental ceiling for industrial-scale autoformalization. Most existing tools suffer from poor concurrency support, low-level operational models, and modularity issues that obscure higher-level mathematical intent. Developing the next iteration of formal systems necessitates fundamental advances in the underlying programming language theory to create systems that are inherently scalable and modular. With trillions of tokens, knowledge organization becomes the most crucial concern: automatically compressing theorems into coherent hierarchies and discovering the right abstractions at the right level of generality. Just as Alexander Grothendieck revolutionized algebraic geometry by shifting focus from solving individual problems to building the foundational abstractions that made their solutions inevitable, our system must infer common patterns and continuously refactor its own knowledge base to discover the right levels of generality for all of mathematics.

AI. Formally verified code serves not merely as a correctness certificate, but also as the highest-fidelity training signal. A central research frontier is learning to leverage these symbolic rewards into autonomous supervision by combining language models, multi-agent reinforcement learning, and neuro-symbolic approaches. We need to build an agentic discovery engine capable of the full repertoire of mathematical reasoning: proving, decomposing, and critiquing at scale. These agents must learn to reason across multiple levels of abstraction in order to discover and build knowledge from the ground up.

Systems. To handle the accelerating pace of discovery, we are building for continual and lifelong learning. Because new mathematics will be generated by both humans and machines at increasing velocity, we cannot rely on static datasets or periodic retraining. We need infrastructure that can ensure every newly formalized theorem immediately expands the system's capabilities. Scaling this loop to millions of proofs introduces significant systems challenges, requiring a distributed, high-concurrency verification engine. Today's proof should become tomorrow's lemma with zero latency.

Human-Machine Interfaces. Our eventual goal is not automating mathematics away but rather enabling co-discovery, where humans and machines can collaborate to explore new mathematical frontiers. Hence, we are partnering with our Veritas Fellows — Terence Tao, Maryna Viazovska, Kevin Buzzard, and others — to redefine the future of mathematics. The revolution in mathematics is already underway, and we must build the correct interface to introduce it to the rest of the world.

The Mathematical Singularity. Soon, a mathematical superintelligence will be able to reinvent and understand all of today's existing mathematics. Then, it will push beyond the frontier: learning, discovering, and verifying new knowledge. This is the mathematical singularity, where mathematics becomes a self-sustaining, self-improving and endlessly growing body of knowledge.

Beyond Mathematics. However, mathematics is just the beginning, and the destination is everything else. What makes mathematics this ideal substrate is simultaneously its limit: in the real world, most things are not absolute, and correctness is affected by uncertainty and human judgment. The next frontier will be bridging the capabilities we forge from mathematics into other domains via a controlled reintroduction of complexity.

We will expand from mathematics to physics, chemistry, materials, biology, control systems, software, and beyond. Each domain has its unique complexities, but the core is identical: formal reasoning, continuous learning, and human co-discovery. The instruments we build for mathematics will be reforged for the world.

Join Us

The scaling of autoformalization is one of the greatest scientific and engineering challenges of our time, sitting at the intersection of programming languages, systems, artificial intelligence, and mathematics. It is time for us to fuse these domains that have historically advanced in isolation. We need ambitious researchers who can innovate and think critically from first principles, world-class engineers who can build infrastructure at planetary scale, and bold mathematicians willing to reimagine their discipline from the ground up. If this sounds like you, join us at math.inc/careers.

Math, Inc.