Mathematicians often like to describe their research with the metaphor of climbing a mountain. Through an immense solitary effort, we reach a summit from which we contemplate a vast landscape of unexplored mathematical truths. From the mountain, we have now descended into the mine: an industrial landscape filled with machines, unexpected discoveries, and disruptive innovations. The romance of the search, the ideal of pen and paper, in which human genius could win immense fame through solitary effort alone, has been lost along the way. As John von Neumann once wrote, “For progress, there is no cure” (“Can We Survive Technology?”, Fortune, 1955): we have no choice but to adapt.
Soon, we will all be miners digging in the mathematical mine, either collaborating or competing with mathematical AI machines. Publications would then be seen primarily as a means of helping humans understand mathematics, while the measurement of mathematical progress would be entrusted to a Mathematical Universal Machine.
This post summarizes the ideas of my recent preprint, which explores what this brave new world of mathematics might look like and how we might collectively shape its future.
What we are afraid to lose
Year after year, we patiently build our own little planet of mathematics. We explore it with constant effort, and these explorations produce stories as well as theorems. The living experience of mathematics lies in sharing what we have learned: passing on intuitions, mistakes, and the secret gestures of mathematical thinking. All of this, and much more, is the human adventure of mathematics. With AI, we risk becoming the Geographer of Saint-Exupéry’s Le Petit Prince, who never leaves his desk: we would let the AI explore the planet for us. The AI would be much faster, much more efficient, and more accurate. But we would lose the pleasure of exploration: choosing where to go, with all its approximations and errors.
We were trained to prove, and proof itself risks becoming obsolete as a distinctively human skill. When proofs become abundant, where is the new scarcity? There is a second danger. Mathematics rests on unusually strong norms of trust and intellectual honesty, and AI risks releasing one of the worst genies from the bottle: suspicion. A divide between the “AI-free” and the “AI-assisted” mathematician could fracture our community.
Decoupling understanding from measurement
The old system of papers, peer review, journals, citations and prestige was never perfect; faced with an abundance of machine-generated mathematics, it may become increasingly inadequate. I propose to partially decouple the advancement of human understanding from the measurement of mathematical progress. Publications would serve primarily to help humans understand mathematics, while progress would be measured by a new institution: a Mathematical Universal Machine (MUM), a shared AI infrastructure available to the entire mathematical community, in the spirit of H.G. Wells’s World Brain (1938).
The mine and the miner
Let me make the metaphor of the mathematical mine more precise. The mine is the space of mathematical truth, results are diamonds hidden within it, and proofs are the tunnels leading to them. The mathematical AI system is the miner, , with three components:
- maps : research papers, databases of proven results, definitions, graphs of dependencies between theorems;
- tools : Lean for formal verification, Python and computer algebra for experimentation;
- a brain : a large language model, with a memory of its past attempts, which decides where and how to dig.
The miner has finite patience, represented by a finite computational budget : the resources of the Machine must ultimately be shared among all mathematicians. More fundamentally, I believe that designing the Machine itself could become a new goal of mathematical research: building a system that achieves the highest possible rate of discovery per budget, or of energy.
Left to explore freely, the Machine progressively fills in the territory accessible from what is already known: I call this the convexification of the mine. My hypothesis is that human intelligence and imagination will not be entirely subsumed by the Machine: new viewpoints, unexpected definitions and genuinely original research may lie outside this convexification. This suggests two complementary modes of research:
- the mathematician as a supervisor, who explores mathematics through the Machine, proposing directions and steering the miner within their own expertise;
- the mathematician as a miner, who works outside the Machine to reach mathematics beyond its current horizon. The resulting papers become new maps which, through a Machine Update, change how the miner explores.

Measuring progress: the Machine horizon
For a statement known to humans but excluded from the Machine’s prior knowledge, let be the probability that the miner proves within the budget . For a level , the Machine horizon is the set of results the Machine can reach:
The Machine would be updated at fixed intervals with newly published mathematics, , and its capabilities reassessed after each update: how much a contribution raises the probabilities of success, enlarges the horizon, or reduces the computation needed to reach a result. Such measurements could complement peer review and provide a new basis for recognizing the contributions of mathematicians, whether they discover new mathematics themselves or improve the Machine’s exploration as supervisors. This echoes Erdős’s book (see Aigner and Ziegler’s Proofs from THE BOOK): rather than collecting the most beautiful proof of each theorem, I propose to seek shorter paths to entire regions of the mine. The goal would be to design a Mathematical Universal Machine with the fastest possible discovery rate, the ratio of mathematical capacity to computational budget (or energy) becoming the new metric.
A political project
The current trajectory of AI is not what we dreamed of. It consumes considerable amounts of energy, water, land, and physical resources. It raises serious ethical concerns when associated with surveillance, social control or warfare. Moreover, AI for mathematics is concentrated in the hands of a few private companies, whose most powerful models are accessible only to selected collaborators. We must not resign ourselves to this status quo. We can build a universal AI infrastructure for mathematics, developed in partnership with an international institution such as UNESCO, governed by mathematicians (for instance through the International Mathematical Union), and belonging to the global scientific commons. As a starting point, it could follow six principles:
- Ecological accountability: its energy consumption and environmental footprint independently assessed and published every year.
- Open architecture: the model architecture, its weights, and the essential components of the system openly accessible.
- Universal and equal access: open to the whole mathematical community, students included, with an equal computational budget for every user.
- Privacy: private research and unpublished results never incorporated into the shared system without explicit consent.
- Transparent Machine Updates: a yearly update with newly published mathematics, together with an estimate of the computational importance of each contribution.
- International scientific governance: a joint mathematics and computer science laboratory responsible for updates, maintenance, evaluation and communication.
Life in the mine
Asked what percentage of mathematics one could hope to understand, John von Neumann reportedly answered “about 28 percent”. With the Machine, we might recover something of the nineteenth-century ideal of understanding mathematics as a whole. I do not want to sound naively optimistic: this text deliberately takes a positive stance, while the reality is challenging, frightening and even depressing. But in the mud of the mine, we still have the power to organize the search collectively: adaptation is not optional (for progress, there is no cure), but preserving our values, and some of our working habits, is still possible.
AI disclosure. This post was condensed from my preprint with the help of an AI, which drafted a first version of the text; the ideas are my own.
Received 27 October 2026.

Add to the discussion