When Proof Becomes the Bottleneck: Formal Mathematics, AI, and the Next Operating System for Discovery

Suppose an artificial intelligence produces a proof of an important theorem this afternoon. How long should it take us to trust it?

For most of mathematical history, the answer has depended on people. A mathematician develops an argument, writes it down, and other mathematicians inspect the reasoning. That social process is one of humanity's most successful systems for producing reliable knowledge. It is also a system with a very human constraint: verification takes time.

This matters because AI is changing the rate at which mathematical arguments can be generated. The interesting question is no longer only whether an AI can solve a difficult problem. It is whether our methods for checking those solutions can scale at the same speed.

Figure 1. If proof generation scales faster than expert review, verification becomes the scarce resource.

When Generation Becomes Cheaper Than Verification

Imagine that an AI system needs several hours to produce a sophisticated proof, while an expert needs an hour to check it. That ratio is manageable when there is one proof. It becomes a serious problem when there are hundreds or thousands of candidate proofs.

The bottleneck is not only labor. Mathematical review is highly specialized. A difficult proof may require deep familiarity with a narrow area, careful reconstruction of hidden assumptions, and substantial time simply to understand the author's strategy. More proof-generating machines do not automatically create more experts capable of checking their output.

This is the central scaling problem: AI can increase the supply of mathematical arguments much faster than society can increase the supply of expert attention.

Recent competition results make the issue concrete. In 2024, Google DeepMind's AlphaProof and AlphaGeometry 2 solved four of the six International Mathematical Olympiad problems, reaching silver-medal-level performance. AlphaProof worked in Lean, so its formal proofs could be checked mechanically. In 2025, several systems reached the five-out-of-six level: Google DeepMind reported gold-medal performance in natural-language reasoning, while formal systems including Aristotle and Seed-Prover also reported solving five of six problems with machine-checkable proofs.

The important signal is not the medal color. It is that mathematical generation is becoming increasingly automated while formal verification offers a path for the checking process to become automated as well.

Formal Mathematics: Change the Unit of Trust

The conventional mathematical paper is written for a human reader. It deliberately omits many steps that experts consider obvious. It uses context, notation, prose, diagrams, and shared background knowledge. This flexibility is a strength for communication, but it creates ambiguity for a computer.

Formal mathematics takes a different approach. A mathematical statement and its proof are represented in a precise formal language. Every object has a type, every assumption is explicit, and every proof step must be accepted by a small trusted checker.

The goal is not to make mathematics less creative. It is to separate two activities that are currently entangled:

Discovery     versus     Verification

Discovery can remain exploratory, heuristic, and imaginative. Verification can become mechanical.

Lean: A Programming Language for Proof

Lean is both a functional programming language and an interactive theorem prover. Its reference documentation describes a small logical kernel whose job is to check proof terms. This architecture matters because the final object being trusted is not a persuasive explanation generated by a model; it is a formal object that the kernel can independently verify.

At a high level, a theorem in Lean behaves like a type and a proof behaves like a term inhabiting that type. The implementation can provide tactics, automation, search, and convenient syntax, but the trusted core remains comparatively small.

This produces an important shift. Instead of asking, “Does this proof sound convincing?” we can ask a stricter computational question: “Does this proof object satisfy the formal statement under the rules of the kernel?”

Figure 2. Formal mathematics separates powerful discovery tools from a small trusted verification core.

Mathlib: When Proofs Become Infrastructure

A proof assistant is far more useful when it does not start from zero. This is the role of Mathlib, the community-maintained mathematical library for Lean.

Mathlib contains definitions, theorems, structures, tactics, and reusable abstractions across a broad range of mathematics. The mathlib community describes it as a unified library of formalized mathematics built collaboratively around Lean. In practical terms, it turns previous mathematical work into reusable machine-checkable infrastructure.

This changes the economics of formal proof. Once a theorem is formalized and accepted, future proofs can import it instead of rebuilding it. The output of one project becomes the trusted input of another. Over time, the library behaves less like a collection of papers and more like a growing computational substrate for mathematics.

That is why the combination Lean + Mathlib + AI is more interesting than any one component in isolation. Lean provides the language and checker. Mathlib provides accumulated knowledge. AI provides search, translation, conjecturing, lemma generation, and proof synthesis.

Leibniz's Old Dream Looks Surprisingly Modern

The philosophical idea behind this architecture is much older than computers. In the seventeenth century, Gottfried Wilhelm Leibniz imagined a characteristica universalis: a universal symbolic language capable of expressing knowledge precisely, together with a logical calculus for reasoning over it. The Stanford Encyclopedia of Philosophy notes that Leibniz sketched this program as early as 1666.

He hoped that intellectual disputes could eventually be transformed from rhetorical disagreement into calculation. The dream was vastly too ambitious for his era, but its structure feels familiar today: a precise language, a body of encoded knowledge, and a mechanism that derives consequences from it.

Modern formal mathematics is not literally Leibniz's universal language, and Lean is not a universal calculator for every kind of truth. Still, the resemblance is useful. The missing ingredient in Leibniz's time was not only logic. It was computation at scale.

AI Becomes the Engine of Search

Formal proof is unforgiving. A human mathematician may understand the core idea of an argument and still find the process of encoding every detail into a proof assistant tedious. AI is unusually well suited to this gap because it can search large spaces, propose intermediate lemmas, translate between representations, and react to immediate verifier feedback.

AlphaProof demonstrates one version of this idea. The system treats Lean theorem proving as a reinforcement-learning environment: the model proposes proof actions, Lean provides an exact success-or-failure signal, and search is guided by feedback from the formal system. The final proof can then be checked independently of the process that generated it.

Aristotle and Seed-Prover extend the same general direction with combinations of informal reasoning, formal proof search, lemma generation, and specialized components. The architectures differ, but the pattern is becoming clear: AI generates; the proof assistant judges.

This is a major difference from ordinary natural-language reasoning. A beautifully written argument can still hide a false step. A formal checker does not care how plausible the explanation sounds.

The Important Scientific Caveat

“The computer checked it” is powerful, but it is not magic.

A formal proof establishes that a formal statement follows from the encoded assumptions under the rules accepted by the proof assistant's trusted base. It does not automatically prove that the formal statement perfectly captures the informal problem a human intended to ask.

There are therefore several layers of trust:

1. The statement. Was the natural-language theorem translated correctly?
2. The assumptions. Did the formalization accidentally include something stronger than intended?
3. The definitions. Do the formal objects represent the mathematical concepts we think they represent?
4. The checker. Is the trusted kernel and its execution environment behaving correctly?

The last layer can be engineered to be very small and auditable; the first three still require mathematical care. Formal verification therefore does not remove humans from the epistemic loop. It moves human attention to a higher-value location: defining the problem correctly, choosing useful abstractions, interpreting results, and deciding what is worth proving.

A New Division of Labor

The most productive future is not “AI replaces mathematicians.” It is a new division of labor.

Humans are good at deciding which questions are meaningful, spotting analogies across domains, inventing definitions, judging whether a theorem matters, and recognizing when a result changes our understanding of a field. Machines are increasingly good at exploring large combinatorial spaces, maintaining exact symbolic state, generating many candidate steps, and repeating a search without fatigue.

A formal verifier adds a third role: it provides a neutral mechanical checkpoint between creative generation and accepted knowledge.

Figure 3. The output of one verified proof can become reusable infrastructure for the next discovery cycle.

The loop is powerful because it compounds. A verified theorem enters the library. The enlarged library supports more difficult proofs. Better proofs create better training and search environments. Better systems produce more verified results. The frontier can move without requiring humans to manually inspect every intermediate step.

What Changes When Verification Scales?

If this architecture works at research scale, the effect could be larger than simply making existing proofs faster.

First, AI could explore many more branches than a human research group can practically pursue. Most branches will fail, but formal verification makes failure cheap and success recognizable.

Second, researchers could ask for stronger guarantees. Instead of accepting an argument that looks correct after review, they could demand a machine-checkable artifact for critical results, much as software engineering increasingly relies on automated tests and formal verification for high-assurance systems.

Third, mathematical knowledge could become more compositional. A theorem would not merely be a PDF that another researcher reads; it could be a reusable object that another theorem prover imports directly.

And finally, the scarce human resource could shift from checking to choosing: choosing questions, representations, conjectures, abstractions, and applications.

The Real Lesson: Verification Must Scale with Intelligence

The most interesting implication of mathematical AI is not that machines may become better at proving theorems. It is that our infrastructure for trust must evolve at the same time as our infrastructure for generation.

If AI can produce more arguments than humans can inspect, then human-only verification becomes a bottleneck. If the arguments are expressed formally, a machine can check them at computational speed while humans concentrate on meaning, direction, and interpretation.

This is not the end of human mathematics. It may be a transition from mathematicians as both explorers and proof-checkers to mathematicians as explorers, architects, and question designers—working with AI systems whose output does not have to be accepted on faith.

The future of mathematical superintelligence may depend less on teaching machines to sound convincing, and more on building a world in which they can be checked.

References

Stanford Encyclopedia of Philosophy. Gottfried Wilhelm Leibniz. Discussion of Leibniz's 1666 program for a universal characteristic and logical calculus.
de Moura, L., Ullrich, S., et al. (2021). The Lean 4 Theorem Prover and Programming Language. CADE-28.
The mathlib Community. (2020). The Lean Mathematical Library. Proceedings of CPP 2020, 367–381.
Hubert, T., Mehta, R., et al. (2025). Olympiad-level formal mathematical reasoning with reinforcement learning. Nature.
Achim, T., Best, A., Der, K., et al. (2025). Aristotle: IMO-level Automated Theorem Proving. arXiv:2510.01346.
Chen, L., Gu, J., Huang, L., et al. (2025). Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving. arXiv:2507.23726.
Google DeepMind. (2025). Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad.