This chapter explores the implications of these innovations, focusing on their impact on how mathematical knowledge is created and shared, and how they are reshaping the social dimension of mathematics, altering collaboration dynamics, trust relationships, and the collective production of knowledge.
Abstract
Quickly evolving technologies, such as Interactive Theorem Provers (ITPs), Automated Theorem Provers (ATPs), and Large Language Models (LLMs), all falling under the general heading'AI for mathematics,'are transforming mathematical practice in profound ways. This chapter explores the implications of these innovations, focusing on their impact on how mathematical knowledge is created and shared. It also discusses how they are reshaping the social dimension of mathematics, altering collaboration dynamics, trust relationships, and the collective production of knowledge. For instance, tools like ITPs facilitate large-scale collaborations and make new types of teamwork possible, where trust is not a necessary ingredient. ITPs also help us mitigate our human fallibility, yet they raise questions about the nature of formalization and the relationship between traditional and formal mathematics. Technologies such as LLMs are reshaping the division of epistemic labour between humans and machines and urge philosophers of mathematics to ask questions about the value of their work.
It is argued that the next leap in AI4Math systems requires a decisive shift from predefined problem-solvers to research agents that can address frontier mathematical challenges with rigorous formal mathematical reasoning, highlighting core limitations of existing systems in serving as mathematical research agents.
E. Jiang, Xiao Liang, Yikai Zhang et al.· 1 citation
We advance the hypothesis that human mathematical reasoning, constrained by both the undecidability and the computational intractability of even modest logical fragments, relies fundamentally on pattern matching from domains external to pure deduction. The most prolific reservoir of such patterns is the natural world, whose physical laws and biological systems have undergone billions of years of ``pre-computation''and already exhibit surprisingly innovative solutions. To ground this claim, we trace the history of the Fourier transform and relevant mathematics, from the vibrating string controversy to the hear equation and subsequent formalisms prevalent in mathematics. At each critical juncture, a physics problem forced the acceptance or creation of a mathematical tool that pure formal reasoning failed to anticipate or, worse, human reasoning had resisted. We further survey the landscape of logical complexity, from NP-hard propositional satisfiability to the non-elementary decision-procedures for monadic second-order theories, to demonstrate that even when a logic is decidable, the resources required for worst-case deduction are astronomically prohibitive. We argue that these barriers make physics-inspired pattern matching not just a historical accident but a cognitive necessity. Finally, we draw the consequence for artificial intelligence: if pure reasoning is constitutively insufficient, then any system aiming at human-level mathematical creativity must embed a vast store of cross-domain patterns rather than rely on deduction alone. This furnishes a principled justification for the enormous scale of contemporary large language models.
Mathematics is often valued for its role as the language of science, but it is equally important as a human practice that teaches us how to think and cultivates creativity, problem-solving skills, attention, and judgment. The rapid rise of modern AI systems, which can solve many standard problems and produce fluent mathematical explanations, forces a reconsideration of the nature of mathematical understanding and how it is developed. This article reflects on the impact of AI across three intertwined domains: mathematics education, mathematical research, and the broader role of mathematics as a way of learning to think. In education, AI changes how students interact with mathematical material, making high-quality assistance widely available while weakening the traditional link between assigned work and demonstrated understanding. The challenge concerns not only academic integrity but also the risks of cognitive offloading and the illusion of explanatory depth. In research, AI can accelerate exploration in various ways, including generating conjectures and examples, performing symbolic manipulation, suggesting proofs, and assisting in the communication of ideas. It has also begun to contribute to discoveries on problems that had resisted human efforts. Yet its limitations remain serious, especially in long arguments requiring global structure, careful verification, and the synthesis of multiple ideas. The central claim is that in an era when routine tasks become easier to automate, the most human aspects of mathematics, including conceptual insight, problem framing, genuine understanding, and creative judgment, become more visible and more valuable.
Existing LLM-based theorem provers have achieved impressive results on formal mathematics benchmarks, yet they remain confined to acting as autonomous agents that prove a stated proposition. In this paper, we propose MathCoPilot, a human-in-the-loop system that embodies a new human--AI symbiotic paradigm for mathematical research, in which the mathematician steers the high-level mathematical direction while AI agents carry out the detailed formalization and proof work under continuous human guidance. MathCoPilot unifies three core capabilities: (1) an interactive workbench where the mathematician and AI agents collaborate through a living proof blueprint that decomposes a proof into navigable steps the human can directly inspect, direct, and refine; (2) automated proving skill orchestration with adaptive knowledge base search and Lean-integrated iterative verification; and (3) topic-driven paper retrieval and automated formalization into a verified Lean knowledge base. Using MathCoPilot, we systematically compare four state-of-the-art LLMs, including Gemini~3.1~Pro, GPT-5.4, and Claude~Opus~4.7, on a FormalMATH subset and on two real PDE theorems requiring deep domain expertise, evaluating their ability to produce verified Lean~4 proofs and to identify errors in deliberately incorrect proofs. Our results show that while current models can handle undergraduate-level problems with high success rates under favorable autoformalization conditions, substantial challenges remain for domain-specific theorems requiring genuine mathematical understanding.
Junjie Zhang, Jia-Yin Liu, Wenbin Liu et al.· 1 citation
The essay makes the case for treating mathematical capacity as a strategic asset on a par with semiconductor capability and proposes, among other measures, that AI systems performing consequential reasoning be required to expose their decision-critical claims in formal, machine-checkable form.