Source-linked AI summary
What is mathematics now, and what should it be?
Jeremy Avigad
TL;DR
AI for mathematics is often narrowed to neural theorem proving, leaving broader possibilities and mathematicians’ role underexamined. This essay expands the scope to formalization, symbolic reasoning, and other AI applications, arguing that mathematicians should help shape these technologies and pursue new mathematical avenues.
Problem
Successes in neural theorem proving are crowding out broader AI applications and leaving mathematics uncertain about its role in an AI-transformed world.
Method
The essay develops an expansive conception of AI for mathematics spanning formalization, proof assistants, symbolic reasoning, and machine-learning approaches beyond large language models.
Results
The essay concludes that mathematicians should lead AI’s development by creating new reasoning procedures, applications, and mathematical uses for the technology.
Takeaways & Limitations
Mathematics has substantial opportunities in the AI era if it clarifies its goals and actively explores technologies rather than merely consuming them.
Takeaways & Limitations
Other AI applications in mathematics have not achieved successes comparable to neural theorem proving, while the essay does not require every mathematician to master machine learning or formal methods.
Abstract
from arXiv · showhide
Advances in neural theorem provers have been impressive, but the successes obscure a broader vision of what AI can do for mathematics and how mathematicians can engage with AI. This essay advances a more expansive and optimistic point of view.
1 Worries about AI
Rapid advances in AI theorem proving and widespread use of systems such as ChatGPT and Claude are making the future of mathematics feel uncertain, especially for students and early-career researchers. The deeper concern is that AI may change the experience and emotional character of doing mathematics, not merely eliminate mathematicians’ jobs.
- Uncertainty about AI: AI’s growing ability to prove theorems and mathematicians’ routine use of systems like ChatGPT and Claude have made the future feel dangerously uncertain, particularly for students and early-career researchers.OpenAI has announced AI-generated solutions to longstanding open problems, while mathematicians increasingly use AI systems to help prove theorems.
- Changing mathematical work: The central worry is that AI will alter the phenomenology of doing mathematics, including the enjoyment of thinking and the freedom to explore ideas that attract mathematicians to the subject.This concern differs from fearing that AI will simply eliminate mathematicians’ jobs.
- Emotional consequences: Adapting to AI-driven workflows and changes to mathematics can produce visceral emotional challenges and a sense of foreboding.Kyu-Hwan Lee described these challenges in personal terms at a recent workshop.
2 A historical perspective
The section frames the essay through Dedekind’s 1888 call to define numbers axiomatically and construct them set-theoretically. It presents this style as a historically disruptive shift that faced resistance because mathematics became strange and unfamiliar to its contemporaries.
- 2 A historical perspective: Dedekind’s 1888 essay characterized the natural numbers axiomatically as a system generated by 1 and a successor function, with a set-theoretic construction.
- 2 A historical perspective: Dedekind sought to replace explicit representations and calculation with axiomatic characterization and set-theoretic construction, a program later championed by Hilbert but resisted by others.
- 2 A historical perspective: The transition to modern mathematics involved foundational debates and personal opposition, as practitioners experienced mathematics becoming strange and unfamiliar.
3 What is AI for mathematics?
“AI for mathematics” should not be reduced to neural theorem proving: it includes formal, symbolic, and collaborative technologies that could enable fundamentally new mathematical work. Realizing this broader potential requires mathematicians themselves to investigate what AI can do.
- 3 What is AI for mathematics?: Neural theorem-proving successes risk crowding out a broader range of promising AI applications in mathematics.The author rejects the idea that AI merely supplants theorem proving and leaves mathematicians only a residual role.
- 3 What is AI for mathematics?: AI for mathematics encompasses formalization and digitization, proof assistants, curated libraries, automated reasoning, and new forms of mathematical interaction and collaboration.It also includes symbolic AI, such as SAT and SMT solvers and first- and higher-order provers.
- 3 What is AI for mathematics?: Investment has been heavily concentrated in LLM-based theorem proving, while other mathematical applications have achieved less and received far fewer resources.Big tech companies and startups have spent billions pursuing theorem proving, orders of magnitude more than on creative alternatives.
- 3 What is AI for mathematics?: These broader applications could create new ways to synthesize data, discover patterns, search for mathematical objects, and find structure in complex phenomena.The author argues that even a small fraction of the resources devoted to theorem proving could reveal substantial mathematical advances.
- 3 What is AI for mathematics?: Mathematicians must help determine AI’s mathematical possibilities rather than leaving that work to computer scientists and big tech companies.The AI revolution is prompting mathematicians to reconsider their values, goals, and ways of pursuing mathematics.
4 Mathematical values
AI should be treated as technology serving mathematical purposes rather than as a competitor, while mathematics must preserve its problem-solving power, legitimacy, and distinctive intellectual values. The section argues that mathematicians’ creativity, depth, abstraction, and commitment to meaningful knowledge remain essential in an AI-shaped world.
- 4 Mathematical values: AI is technology designed to serve our purposes, so mathematicians should focus on how to use it effectively rather than compete against it.The relevant questions are how AI should be used and what purposes it should serve.
- 4 Mathematical values: Mathematics risks losing legitimacy if practitioners no longer rely on it and its distinctive contribution is reduced to advising people to use ChatGPT.Because AI will transform science, business, government, and industry, mathematics must offer more than generic access to AI tools.
- 4 Mathematical values: Mathematics continues to offer creative methods for solving difficult problems and carrying out complex reasoning with limited computational resources.The AI era is presented as another stage in mathematics’ scientific and technological development, while LLMs are not necessarily the most efficient mechanism for mathematical reasoning.
- 4 Mathematical values: Mathematicians’ enduring value lies in asking questions, developing abstractions, building theory, exploring concepts, pursuing deep engagement, and contributing meaningful knowledge rather than short-term profit.These values and attitudes are described as especially needed in the present era.
5 The challenges
Mathematics is changing as practitioners develop AI and formal-methods expertise, but institutional norms often exclude this work and drive young talent away. The discipline must adapt while preserving its core values and recognize that it needs those practitioners.
- Young practitioners are learning formal libraries, APIs, automated reasoning, neural-network tuning, machine-learning experimentation, reinforcement learning, SAT encodings, and solve-statistics interpretation.
- Mathematical institutions often treat engagement with AI and formal methods as abandoning mathematics, discounting computer-science publications and driving trainees toward industry.
- The field should broaden its methodological standards and recognize nonconventional contributions while developing a clearer account of research in AI for mathematics.
- Mathematics must balance conservatism with flexibility, adapting to social, political, cultural, and technological change while preserving its core values.
- Mathematics must anticipate AI’s effects, equip students for the future, and acknowledge that it needs practitioners who have moved into AI and formal methods.
6 The future
Future mathematicians should develop basic competence with AI-related tools, while mathematicians must actively shape AI’s methods and applications rather than merely consume them. This requires rethinking what mathematics should be so technological advances become opportunities for exploration and growth.
- 6 The future: Future mathematicians need basic competence with machine learning and formal methods, though not every mathematician must become an expert in them.This competence should be treated as broadly foundational, like established mathematical subjects in contemporary PhD programs.
- 6 The future: Mathematicians should help lead the AI revolution by developing scalable reasoning procedures, finding applications, and applying deep mathematical expertise to theoretical and practical problems.The goal is active contribution, not passive consumption of AI.
- 6 The future: Mathematics must clarify what it wants to become: clinging to the status quo risks helplessness, whereas embracing new technologies opens opportunities for exploration and growth.The essay treats this conceptual consensus as a prior step to deciding how to proceed.