How Machines Are Transforming Proofs
My career began in mathematics, followed by a transition to quantitative finance. In the early 2000s, I became a data scientist. Mathematics is highly specialized, making it difficult to stay abreast of the latest developments. Therefore, I am far from an expert on the use of AI in mathematics. However, someone who is both an elite mathematician and an avid user of AI for “Machine-Assisted Proof” is Fields Medalist Terence Tao. He recently gave a talk and interview on this very topic, which prompted me to write this overview on AI in mathematics.
“Machine-Assisted Proof” is a collaborative approach where mathematicians use computational tools to assist various aspects of the proof process. This includes formal proof verification, conjecture generation, and proof assistance. Proof assistants like Lean rigorously check the correctness of formalized proofs. Machine learning, particularly neural networks, can analyze mathematical data and suggest potential theorems or relationships. Large language models (LLMs) can suggest proof techniques, related literature, or even generate code for specific steps. This approach remains human-centric, with the mathematician providing the initial proof structure and key ideas while the computer handles the tedious and error-prone aspects of proof verification and formalization. This enables large-scale collaboration among mathematicians by dividing the proof into manageable parts, each verified computationally.
Tao and other mathematicians are excited about Machine-Assisted Proof because it has the potential to revolutionize the way mathematics is done. By automating tedious tasks, finding novel proofs, and even surpassing human capabilities in certain areas of mathematical reasoning, AI systems could help mathematicians formalize proofs, find insights, and collaborate more effectively on large-scale projects. Proof assistants like Lean are already valuable tools for mathematicians, even without AI integration, as they help ensure correctness and facilitate collaboration.
One interesting aspect of Machine-Assisted Proof is the potential for a division of labor between mathematicians and AI. Not everyone needs to be a programmer; some can focus on the high-level mathematical direction while others specialize in formalizing proofs using AI tools. This allows for leveraging diverse skill sets and could make mathematics more accessible to a wider range of people.
Another exciting application is intuition and idea generation. Language models can generate ideas that resemble human intuition, aiding in the creative process of developing new approaches and ideas for proofs. While their success rate in generating valuable ideas is currently low, the potential for breakthroughs remains. For example, Tao mentions using GPT for suggesting the use of generating functions in a proof, which he had initially overlooked.
Collaboration and knowledge sharing are other key areas where AI shines. AI can facilitate large-scale collaborative proof development by managing contributions from multiple mathematicians. Formalized and interactive textbooks can make it easier for people to collaborate on complex projects. Projects like the formalization of the Polynomial Freiman-Ruzsa (PFR) conjecture have involved over 20 contributors, highlighting AI’s role in compartmentalizing and coordinating efforts.
AI systems help mathematicians formalize proofs, find insights, and collaborate more effectively on large-scale projects
AI’s tool integration and automation capabilities also offer significant benefits. Coupling language models with reliable tools like Wolfram Alpha and using AI-powered autocomplete can aid in automating certain tasks and making the proof process more efficient. Tao mentions using an AI-powered autocomplete tool for writing code and LaTeX, which suggests new sentences based on the text already written.
Lastly, theoretical advances and insight extraction are areas where AI could revolutionize mathematics. AI systems may lead to a proliferation of formally verifiable proofs that are difficult for humans to comprehend. Extracting human-readable insights from these proofs will become an important task. Tao predicts that there will be an industry of people trying to extract insights from AI proofs that initially don’t have any insight, similar to experimental scientists extracting laws of nature from empirical data.
Analysis
I see AI’s transformative potential in mathematics as a harbinger of its impact across diverse domains. The patterns, lessons, and challenges observed in mathematicians’ adoption of AI tools and LLMs, offer valuable insights for other fields. Reflecting on AI’s potential to revolutionize mathematics, several key points stand out:
- Value of Proof Assistants: There’s a strong consensus that proof assistants like Lean are already valuable tools for mathematicians, even without AI integration. They help formalize proofs, ensure correctness, and facilitate collaboration. Tao highlights the use of Lean in formalizing existing mathematical knowledge.
- Optimism about AI’s Potential: I am incredibly optimistic about AI’s potential to revolutionize mathematics. This includes automating tedious tasks, finding novel proofs, and even surpassing human capabilities in mathematical reasoning. Systems like proof assistants (e.g., Lean) and large language models could help mathematicians formalize proofs, find insights, and automate tedious aspects of research. This is an exciting new frontier. Terence Tao predicts significant progress in AI-assisted proof within the next few years.
- Division of Labor: The division of labor between mathematicians and AI is crucial. Not everyone needs to be a programmer. Some can focus on the high-level mathematical direction while others specialize in formalizing proofs using AI tools. This allows leveraging diverse skill sets. For example, Fields Medalist Peter Scholze collaborated on a Lean project despite limited computer science knowledge, to verify a complex and pivotal proof in the foundations of topology. [A postdoctoral researcher at the University of Freiburg helped bring in about a dozen mathematicians to contribute to formalizing different parts of the proof.]
- Formalization of Mathematics: The ongoing effort to formalize existing mathematical knowledge in a way that is understandable by both humans and computers is a crucial step towards leveraging AI in mathematics. This process ensures that mathematical proofs are not just human-readable but also machine-verifiable, making them universally understandable and reducing the risk of human error.
- Specialization of Proof Assistants: The ease of using proof assistants varies by area of math. More formal fields like logic are easier to encode than “intuitive” fields like topology. Adoption will likely vary by specialization.
- Concerns about AI Hallucinating Proofs: There are potential issues with AI systems claiming to translate high-level proofs to formal code but actually outputting flawed proofs that still pass verification. This could undermine trust in AI-generated proofs.
- Fragile Proofs: Automated theorem proving can result in proofs that are fragile and fail when minor changes are made to definitions or theorems. Proof assistants may produce proofs that are overly dependent on specific lemmas, leading to brittle results.
- Incomprehensible AI-Generated Proofs: AI-generated proofs can be complex and difficult to understand, making them less useful for further analysis and development. While an AI-generated proof might be correct, its complexity can hinder comprehension and practical application. However, one could potentially use another AI model to explain and break down the proof to make it more understandable.
Related Content
- Lessons from the ‘Noisy Factors’ Study
- Financial Machine Learning
- The Financial Services Sector’s March into Generative AI
- Generative AI’s Impact on Healthcare
- 2024 Generative AI in Healthcare Survey Results
- Generative AI in Industrial Applications
If you enjoyed this post please support our work by encouraging your friends and colleagues to subscribe to our newsletter: