SERIES · As application deadlines approach, Proofs and Prompts is publishing a series of posts from 19 to 23 October for people considering a PhD, doing a PhD or looking for a postdoc: guidelines, discussions and speculation about what to do and what careers in mathematics will look like. This post is one of them. Each is written independently and reflects only its authors’ views. All posts in the series
Mathematics is a creative and emotional endeavor. We are driven by challenge and curiosity. We express our ideas carefully to be precisely understood. Our highest moments can fill us with exhilaration and awe.
But how we do mathematics has evolved over time. We have moved away from pictures and informal arguments; we now have axioms and proofs. We have outgrown the time when one person could have understood all of known mathematics; now, we specialize, relying on others to teach us what we know less about.
Today, it is clear that mathematics is again changing and growing beyond us. There exist machines which can prove new mathematical statements, and convert them into papers for humans to verify. This is strange and disruptive to our current process. However, I offer a positive vision of a future which includes these machines while preserving our motivations for this extreme passion.
We should change our mindset from explorers of the mathematical frontier to stewards of a world commons of mathematics.
A commons is a societal resource available to all because it improves everyone’s quality of life. My favorite example is the US National Park system. At a national park, I can reliably experience an overwhelm of natural beauty in mountains, forests, or rivers. I can camp, swim, or just walk on a trail. After a weekend trip, I return to my normal life refreshed and inspired.
I like the outdoors, but I am not very adventurous. For some people I know, the outdoors can feel like home. They will go into nature for weeks or months at a time: backpacking, rock climbing, journaling. One can make a living like this as a park ranger or firefighter; people in these jobs are paid to understand wildlife, take responsibility for keeping man and nature in balance, and build trails to make life pleasant for visitors like me.
We can build the same kind of environment for mathematics.
For many of us, research is more of a passion than a job. The mathematical outdoors feels like home. This is why theorem-proving machines can feel so intimidating: they are strange new creatures. I think the machines are here to stay, and I don’t think we can control which problems they will solve. Instead, we should learn from them, keep them in balance with human understanding, and show other humans the beauty of this place. We can be the rangers and firefighters of our mathematical parks, which are more alive than ever before.
The sudden advent of theorem-proving machines will make the next few years painful and difficult. However, if we do not act, we may quickly lose relevance, and our community is likely to wither. This makes building a mathematical commons extremely urgent. But what would it take to build this commons?
The most important step is to create a coalition of mathematicians to steward the commons. We should create a non-profit with a large advisory board, who represent the broad and diverse interests of people who prove or teach theorems in their work. This organization should not be run by any AI company, and our artifacts should be open to everyone.
The next step is to convert all mathematics into formally verified statements. This is the goal of the Mathematics Autoformalization Project. If we can use computer code to certify correctness of a proof, we can maintain our trust in these proofs at scale. Today, the most popular way to formally verify mathematics uses the Lean proof assistant. There is a vibrant open-source community around Mathlib, which has verified essentially all of undergraduate mathematics. It is now even possible to use LLMs to convert proofs of research-grade theorems directly into Lean. (The recent formalization of Fermat’s Last Theorem used the public prove2.me site I helped build.)
Formalizing all of mathematics would create a large directed graph of known statements and their implications. Creating this graph is achievable if AI companies donate some compute resources to the mathematical commons. Here, they can work together instead of against each other. In the future, all new results could be added to this graph of knowledge.
The final step is to tame this graph of formally verified statements. We do not have to digest all at once; we only have to manage it. We should cluster and sparsify the graph until it corresponds to human-sized chunks of knowledge. We can look for simplifications, common definitions, and unifying theories. We can build trails through wonderful proofs to share both with other mathematicians and with “park visitors”. This can all be assisted by machines, provided it helps accomplish our goals.
If done well, the commons will bring about a golden age for human understanding. With responsible stewardship, we can nurture the next generation of mathematicians and math appreciators alongside theorem-proving machines.
Let us start by building this broad coalition of mathematicians. If we work together, we can steer the way mathematics evolves in this uncertain future.
Kunal Marwaha
Received 5 October 2026, revised 23 October 2026.
Add to the discussion