Mathematics and Machine Creativity: A Survey on Bridging Mathematics with AI

TL;DR

The paper surveys AI's role in mathematical research, arguing that AI can contribute meaningfully while acknowledging current reasoning limits of large language models. It articulates three AI-enabled workflows—machine-assisted proofs, pattern-based theoretical exploration, and explicit construction of mathematical objects—and discusses end-to-end proof generation and autoformalization as key components. It emphasizes human–AI collaboration and the ethical, educational, and societal implications of integrating AI into mathematics. Overall, the work provides a framework to bridge AI and mathematics, offering practical pathways to accelerate discovery while preserving rigorous mathematical thinking.

Abstract

This paper presents a comprehensive overview on the applications of artificial intelligence (AI) in mathematical research, highlighting the transformative role AI has begun to play in this domain. Traditionally, AI advancements have heavily relied on theoretical foundations provided by mathematics and statistics. However, recent developments in AI, particularly in reinforcement learning (RL) and large language models (LLMs), have demonstrated the potential for AI to contribute back to mathematics by offering flexible algorithmic frameworks and powerful inductive reasoning capabilities that support various aspects of mathematical research. This survey aims to establish a bridge between AI and mathematics, providing insights into the mutual benefits and fostering deeper interdisciplinary understanding. In particular, we argue that while current AI and LLMs may struggle with complex deductive reasoning, their "inherent creativity", the ability to generate outputs at high throughput based on recognition of shallow patterns, holds significant potential to support and inspire mathematical research. This creative capability, often overlooked, could be the key to unlocking new perspectives and methodologies in mathematics. Furthermore, we address the lack of cross-disciplinary communication: mathematicians may not fully comprehend the latest advances in AI, while AI researchers frequently prioritize benchmark performance over real-world applications in frontier mathematical research. This paper seeks to close that gap, offering a detailed exploration of AI fundamentals, its strengths, and its emerging applications in the mathematical sciences.

Figures (3)

• Figure 1: A Lean 4 (web version) formal proof for the simple fact that if $a, b$ are natural numbers and $a^2 = b^2$, then $a = b$. The left side contains the formal proof, and the right side shows the feedback from the proof engine. Currently the feedback is "No goals", meaning the proof is complete.
• Figure 2: A simplified version of the human-AI collaboration framework from davies2021nature, illustrating the discovery process of Euler's formula for planar graphs: suppose $Z$ is a class of mathematical objects, and $X_1,...,X_k$ are functions defined on $Z$, mathematicians begin by hypothesizing that $X_k$ is related to $X_1,...,X_{k-1}$ by some function $f$. They then use computer programs to sample a large dataset from certain distribution over $Z$. Next, a supervised model $\widetilde{f}$ is trained to approximate these data. Finally, mathematicians analyze $\widetilde{f}$ to formulate a candidate conjecture $f^*$ and proceed to prove it.
• Figure 3: The FunSearch pipeline proposed in mathdiscoveriesfromprogram24.

Theorems & Definitions (1)

• Remark 5.1