This essay is heavily influenced by James C. Scott’s Against the Grain: A Deep History of the Earliest States.
To the question “what is 2 + 3” a French primary school pupil replied: “3 + 2, since addition is commutative”. He did not know what the sum was equal to and could not even understand what he was asked about! – V. I. Arnold, probably to Serre
A golden year for low-hanging fruit picking
At the end of 2025, we have already seen open problems being cracked by automated theorem provers. Obviously, open doesn’t imply important or difficult; 1 * arbitrarily large number = arbitrarily large number is an open problem but utterly trivial. But donning Erdős’s name gives them a certain weight! The resolution of a couple of Erdős problems was always followed by a murmur of “Ah that was surprisingly easy / a corollary of some result, but nobody made the connection.” Deepmind’s amazing case study echoes the difficulty and subtlety of solving problems with AI.
I’m not trying to belittle the results. On the contrary, I’m very happy to see low-hanging fruit getting picked: of course, they are the first to go. 2026 is going to be the year where one might expect lots of such open problems to be resolved, maybe even some from Formal Conjectures if we’re lucky. Nothing prevents people from hammering all known open problems that have been recognised.
It’s going to be hyped to the nines though, by startups in the AI-maths space, and reasonably so. One can expect to feel a sense of exhaustion after the initial cheer, and wonder if that’s it? Is that all there is? It’s important to remember that incremental progress is the vast majority of scientific behaviour, and not to disparage increments. We will probably have at least one more year of low-hanging fruit picking, and I’m all the happier if it turns out to be more than one year - a decade of rapid mathematical progress should be incredibly exciting for humans as a civilisation.
Formal methods and the ripening of the tax grain
After ACL2, Agda, Coq, HOL Light, HOL4, Isabelle, Lean 1-3, Metamath, and Mizar, it seems that mathematics finally found its tax grain—a general enough, intuitive, open-source, maintainable^*, measurable, and sustainable way of verifying mathematics: the Lean4 proof assistant with a helpful community around it. A lot of the lessons learned from the previous proof assistants went into Lean4, and I’m certain it won’t be the last proof assistant we use, but it has reached an inflection point where we can see a glimpse of how mathematics can be done as a citizen science.
How does a mathematician verify anything in modern mathematics? It’s too complex to check piece by piece by yourself. A result can depend on a chain of other results which one has no chance to validate alone. It is a modern mathematician’s fate to believe some results without verifying them because otherwise one does nothing but verification all day. This can gradually lead to the heat death of mathematics. But what also prevents mathematics from modernizing is that the difficulty in verification brings about the difficulty of scaling the number of collaborators on papers, and the rate at which mathematical papers can become public after peer review.
This excellent article captures well what one can trust in Lean: Spike’s website. The most exciting thing about formal proof assistants is that under certain weak assumptions, trust becomes direct: I don’t need to check Colleague C’s proof because the computer says it checks out, and C didn’t hide the hard parts in axioms (which the computer can also check for me).
Now, Colleague C may also turn out to be a Computer, and C may well have collaborated with many other colleagues I don’t know about. But the abstraction afforded by Lean is that there is no distinction between their work, colleague C’s work, or my work for that matter, in how their validity gets established. We will finally have big maths after two Big Proof conferences one and two.
Lean4 shines as a tax grain as people can deposit formal artefacts of their work as taxes in exchange for guarantees of correctness, greatly improving publication and collaboration at a stroke. The current tax rate is high, but as autoformalization and automation improve, it becomes feasible to focus on the creative parts of mathematics. Finally, time for a revolution.
From the community to the state
There have been schools of mathematics since the time of Pythagoras, who subscribed to particular styles and beliefs about mathematics. I hope I have convinced you that a new state of mathematicians will emerge and attract citizens from across the world, centred around proof assistants. The state can become very strong with the VC money it receives, the useful models or scaffolds it creates, and the envy it attracts by formalising results or even picking low-hanging open problems. I see no reason why it shouldn’t become a very dominant one.
One of the most influential consequences of the agricultural revolution was the emergence of a new class of people who were not directly involved in food production, and had resources to pursue other activities. In the context of mathematics, the state could well lead to a flourishing of mathematical creativity and innovation, as more people become able to contribute to the field.
However, there is a distinct and cautionary parallel to be drawn here about who ultimately reaps the harvest. Just as early agrarian states often led to the exploitation of the laborers who produced the surplus, we must be wary of the enclosing the digital commons. The open-source mathematical community is painstakingly translating the edifice of human thought into a formalised “tax grain”. There is a real risk that companies will harvest this crop to extract the immense value of this collective labour, without ever contributing back to the community. One mathematician recently remarked to me, “We have many imaginations of what a bad mathematical culture looks like, but not much about what a good one looks like.” This is a call for mathematicians to imagine more. As someone working on open-source AI models for math, I believe we must actively envision what a good mathematical culture looks like in the age of automation and forcefully build toward it, by enforcing standards and creating incentives for genuinely beneficial contributions.
To borrow Alexander Grothendieck’s metaphor of the “rising sea”, we should ensure the water level rises for the entire community, dissolving the barriers to collaboration and verification, rather than filling the proprietary reservoirs of a few tech states. The choice is up to the state subjects for now, and this is the chance to shape the future.
Acknowledgements
This essay is inspired by conversations with Simon Sorg, Roman Soletskyi, Fabian Glöckle, George Tsoukalas, and many others, to whom I express thanks.
*: Currently, maintainable is a contested characteristic of mathlib due to the number of AI slop PRs submitted without thought.