Paper deep dive
Shaping the Future of Mathematics in the Age of AI
Johan Commelin, Mateja Jamnik, Rodrigo Ochigame, Lenny Taelman, Akshay Venkatesh
Intelligence
Status: succeeded | Model: google/gemini-3.1-flash-lite-preview | Prompt: intel-v1 | Confidence: 94%
Last extracted: 3/27/2026, 1:18:13 AM
Summary
This paper discusses the transformative impact of Artificial Intelligence on mathematics, emphasizing the need for the mathematical community to actively shape its future. It identifies five key areas—values, practice, teaching, technology, and ethics—and advocates for community-led infrastructure, ethical guidelines, and a re-evaluation of mathematical curricula to maintain intellectual autonomy and align technological progress with academic values.
Entities (5)
Relation Signals (3)
Johan Commelin → directs → Mathlib
confidence 95% · Johan Commelin is the director of the Mathlib Initiative
AlphaProof → performsat → International Mathematics Olympiad
confidence 95% · AlphaProof have recently performed at medal level at the International Mathematics Olympiad
Lean → usedby → Mathematical Community
confidence 90% · A growing community of mathematicians is using the Lean proof assistant
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Artificial intelligence is transforming mathematics at a speed and scale that demand active engagement from the mathematical community. We examine five areas where this transformation is particularly pressing: values, practice, teaching, technology, and ethics. We offer recommendations on safeguarding our intellectual autonomy, rethinking our practice, broadening curricula, building academically oriented infrastructure, and developing shared ethical principles - with the aim of ensuring that the future of mathematics is shaped by the community itself.
Tags
Links
- Source: https://arxiv.org/abs/2603.24914v1
- Canonical: https://arxiv.org/abs/2603.24914v1
Trouble viewing inline? Open PDF directly →
Full Text
15,267 characters extracted from source content.
Expand or collapse full text
Shaping the Future of Mathematics in the Age of AI Johan Commelin ∗ Mateja Jamnik † Rodrigo Ochigame ‡ Lenny Taelman § Akshay Venkatesh ¶ Artificial Intelligence (AI) is transforming math- ematics at a speed and scale that demand we reconsider the very intellectual basis of our disci- pline.Built on twentieth-century explorations of computability and the foundations of mathematics, modern AI has grown beyond calculation and exhaustive checking to sophisticated mathematical deduction. The rapid emergence of these abilities creates a host of issues that our community urgently needs to address. This transformation appears across diverse and competing AI methods. A growing community of mathematicians is using the Lean proof assistant 1 — a formal verification system based on traditional symbolic methods—to encode and verify com- plex proofs in collaborative formalization projects [CT24]. Neuro-symbolic systems such as AlphaProof [HMS + 25] have recently performed at medal level at the International Mathematics Olympiad, while large language models (purely neural AI) are be- ginning to serve as mathematical research assistants ∗ Johan Commelin is the director of the Mathlib Initiative and an assistant professor at the mathematics department of Utrecht University. His email address is j.m.commelin@u.nl. † Mateja Jamnik is a professor of artificial intelligence at University of Cambridge.Her email address is mateja.jamnik@cl.cam.ac.uk. ‡ Rodrigo Ochigame is an assistant professor of anthro- pology at Leiden University.Their email address is ro- drigo@ochigame.org. § Lenny Taelman is a professor of mathematics at the University of Amsterdam.His email address is l.d.j.taelman@uva.nl. ¶ Akshay Venkatesh is a professor at the School of Mathe- matics of the Institute for Advanced Study. His email address is akshay@ias.edu. 1 See https://leanprover-community.github.io for the community portal about Lean and Mathlib; for associated ar- ticles, see [dMKA + 15, Com20]. [Sal25]. Though these approaches differ in method and philosophy, together they have the potential to change how we discover, verify, and organize mathematical knowledge. We—the authors of this article—organized a work- shop on “Mechanization and Mathematical Research” in September 2025 at the Lorentz Center in Leiden, The Netherlands. 2 The workshop brought together mathematicians, computer scientists, philosophers and historians to look beyond the immediate techni- cal horizon. The resulting discussions were electric— all the attendees understood the stakes. We write pri- marily from our own perspective on the most impor- tant takeaways, aiming to spark a necessary conversa- tion within the mathematical community—one that neither idealizes established practices nor assumes that technological change is inherently desirable. To clarify terms for readers: by formal proofs we mean computer-verifiable proofs in systems such as Lean, Rocq, or Isabelle. References to libraries of formal proofs indicate shared repositories of veri- fied statements and proofs, such as Mathlib and the Archive of Formal Proofs 3 . By AI we refer to both symbolic and neural methods, including large lan- guage models. These tools differ in method but can each contribute to automating mathematical reason- ing and discovery. Finally, we interpret mathemati- cal community broadly, encompassing researchers in academia and industry, as well as students and inde- pendent contributors. 2 See https://w.lorentzcenter.nl/mechanization-and -mathematical-research.html for programme and slides, and https://w.youtube.com/@mechanicalmath for recordings of the lectures of the concluding public symposium. 3 https://w.isa-afp.org 1 arXiv:2603.24914v1 [math.HO] 26 Mar 2026 Below, we highlight five key themes that emerged from the workshop: our values in mathematics, our practice, our teaching, the technologies we engage with, and the ethical considerations arising from new intelligent systems. We will emphasize several central questions and recommendations. The future of mathematics in the age of AI need not be something that happens to us—it is something that the mathematical community should shape together. Values in mathematics We were struck by the breadth of viewpoints ex- pressed at our workshop. Some participants were enthused by the idea of computers freeing them from tedious tasks of proof writing, while others felt that these very tasks might hold some essential part of the craft of mathematics. Some advocated for a greater role of formal proofs in research and teaching, while others defended the exact opposite. These disagreements often highlighted an ongoing tension between professed values and the reality of mathematical practice. This spectrum reflects a genuine diversity of views about basic values, tied to mathematics’ distinctive heritage as both a humanistic and a scientific dis- cipline. Simplistic generalizations about the values of mathematicians should therefore be viewed with caution. Yet the current moment calls for a deliberate exam- ination of our values in all their complexity. Means reshape ends: the capabilities of new technology risk dictating what counts as mathematically significant, rather than serving our priorities. The ability to au- tomate pieces of mathematical arguments will change the kinds of problems that are pursued and the forms of proof that are valued; the strengthening of rigor by means of formalization and automated proof- checking will change the expectations and standards of publication. And while some parts of the commu- nity may benefit from the increased commercial in- terest in mathematical AI, we must remain conscious of how such interest can reorient the field’s internal compass. Otherwise, our discipline risks losing its intellectual autonomy. These issues are not new; what makes them press- ing is the scale and speed of recent developments. There are no simple answers, but the workshop re- vealed broad agreement on a fundamental principle: Ensure that the development and adoption of new technologies in mathematics remain firmly rooted in our own epistemic and aesthetic values—diverse as they are—rather than driven by the internal logic of those technologies or the commercial interests of their developers. Professional societies, mathematics departments, and individual researchers all have important roles to play in facilitating conversations around these is- sues and shaping a deliberate path forward. Future of mathematical practice We do not know if, when, or to what extent AI sys- tems will surpass humans in their ability to perform clearly defined mathematical tasks such as generating formal proofs. The discussions at the Lorentz Cen- ter, however, underscored that it is well past time to grapple with the implications of these possibilities. As a community, we must now ask: in such sce- narios, what will qualify as mathematical discovery? Will it be the generation of a formal proof, the formu- lation of an important conjecture, the construction of an explanatory argument, or something else? What will the role of human intuition be? How can we nur- ture the next generation of mathematicians when the very nature of our practice is in flux? Such questions help us frame our responsibility: Engagecollectively—andalongsideour students—with the question of how our relationship to mathematics will change if computers can perform many of the day-to- day tasks of current mathematical research. 2 Teaching and education As with the introduction of handheld calculators and other past technologies, AI may change what we re- gard as fundamental mathematical competencies and the very purpose of mathematical education. If com- puters can perform precisely defined mathematical tasks at scale, then mathematical fluency may no longer lie in executing those tasks oneself. Instead, it may lie in understanding which tasks to perform and why, in connecting them to larger questions, and in cultivating the judgment and insight that give mathematics its meaning. This shift also raises ques- tions about assessment and examinations: how can we evaluate students’ understanding and skills in a landscape where AI can perform routine calculations and proofs? To make the mathematical community more resilient to an unpredictable future, we propose that the community: Review undergraduate and graduate math- ematical curricula to emphasize a broader range of skills, including posing problems, communicating ideas, and critiquing pur- ported logical arguments. Students should have a say in this deliberation: their future is at stake. Technology How can mathematicians contribute directly to the creation of AI tools for mathematics, so that we have more of a voice in their development? One way this is already happening is through for- mal proof libraries. These libraries have succeeded in involving a large community of professional and non- professional mathematicians. To ensure long-term health of these libraries and their alignment with academic values, we must now address critical ques- tions of governance, learning from both the successes and the failures of open-source projects. In particu- lar, we must establish clear licensing frameworks and contributor norms that protect these libraries from unrestricted commercial use without attribution or respect for the rights of authors. Another proposal being pursued by multiple groups is the creation of community-owned bench- marks.Good benchmarks can signal community values to those developing AI systems, while also helping mathematicians understand realistic use cases for, and limitations of, the technology. For example, benchmarks that focus on open-ended problems can counter overstated claims based on narrow task suites. At present, the most advanced AI systems for mathematical reasoning are proprietary and originate in for-profit labs, yet open-source and open-weights alternatives are emerging (e.g., [LTL + 25, WUL + 25]). These different implementations naturally compete, but they also create opportunities for synergy, both within academia and between academia and indus- try: shared learning, cross-validation, and comple- mentary approaches can strengthen the community’s understanding and development of AI tools. The mathematical community thus faces an ambi- tious goal: Build academically oriented technological infrastructure, with open-source code, trans- parent decision-making,and community oversight, in ways that reduce dependence on any single commercial actor. Besides helping to maintain intellectual indepen- dence, such infrastructure would allow for more transparency around issues of cost, computational resources, training data, and environmental impact, and would help to align technological development with the community’s values and priorities. Norms, ethics, and governance The integration of AI into mathematical research raises significant ethical and governance concerns. The training of such systems uses the work of the mathematical community in an opaque way that threatens established norms of attribution and credit. AI-generated papers are starting to put still more pressure on a publication system already strained to the breaking point; and how should formal proofs be 3 integrated into this? Mechanization may also create new forms of inequality, in which disparities in ac- cess to computational resources distort the compet- itive dynamics of mathematical research. Moreover, the substantial energy demands of AI systems raise important environmental concerns. We thus propose that the community: Develop and maintain a living statement of ethical principles to guide academic math- ematicians and mathematical institutions in their interactions with AI systems and developers. Such a statement is not intended to be binding or exhaustive, but rather a collective articulation of shared values and ethical practices, established through wide consultation (compare with [otAC75]). It may address norms about attribution and citation, disclosure of computational resources and training data, guidelines on the licensing of preprints and for- mal proof libraries, and a code of conduct for AI use. Maintaining such a statement requires ongoing gov- ernance, ideally under the leadership of professional societies, to adapt to new challenges. A group of workshop participants is currently developing such a statement. Please engage! The torrent of AI-related news may provoke skepti- cism, or, conversely, a sense of resignation. Yet we exhort everyone reading this to engage with the topic of AI and mathematics. Learn about its technical aspects and capabilities. Discuss it with your col- leagues, your students, and your professional organi- zations. Reflect on what you value in your practice of mathematics, and take collective action. We are at a crossroads. As we see it, the nature of the discipline is being renegotiated. By engaging with these questions, you are helping to ensure that this fu- ture will reflect our collective values and aspirations. References [Com20] The mathlib Community, The lean mathemati- cal library, Proceedings of the 9th ACM SIG- PLAN international conference on certified pro- grams and proofs, 2020, p. 367–381. [CT24] Johan Commelin and Adam Topaz, Abstraction boundaries and spec driven development in pure mathematics, Bulletin of the American Mathe- matical Society 61 (2024), no. 2, 241–255. [dMKA + 15] Leonardo de Moura, Soonho Kong, Jeremy Avi- gad, Floris van Doorn, and Jakob von Raumer, The lean theorem prover (system description), Automated deduction - CADE-25, 2015, p. 378– 388. [HMS + 25] Thomas Hubert, Rahul Mehta, L ́eonard Sar- tran, J ́ulia Komj ́athy, Julian Schrittwieser, Sher- jil Ozair, Arthur Guez, Oriol Vinyals, Ioannis Antonoglou, Timothy P. Lillicrap, David Silver, and Laurent Sifre, Olympiad-level formal math- ematical reasoning with reinforcement learning, Nature (2025). [LTL + 25] Yong Lin, Shange Tang, Bohan Lyu, Ji- ayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin, Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving, arxiv (2025), available at 2502.07640. [otAC75] The Organizing Committee of the Asilomar Con- ference, Asilomar conference on DNA recombi- nant molecules, Nature 255 (1975), 442–444. [Sal25] Adil Salim, Accelerating mathematical research with language models: A case study of an interac- tion with gpt-5-pro on a convex analysis problem, arXiv (2025), available at 2510.26647. [WUL + 25] Haiming Wang, Mert Unsal, Xiaohan Lin, Man- tas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxc ́e, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, L ́eo Dreyfus-Schmidt, Lewis Tunstall, Luigi Pa- gani, Moreira Machado, Pauline Bourigault, Ran Wang, Stanislas Polu, Thibaut Barroyer, Wen- Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang, Zhengying Liu, and Jia Li, Kimina-Prover Pre- view: Towards Large Formal Reasoning Models with Reinforcement Learning (2025), available at 2504.11354. 4