Computer Proofs and Artificial Intelligence in Mathematics

At some unspecified future time, mathematicians would be replaced by computers.

Paul Cohen

Paul Cohen made a prediction in the late 1970s that mathematics could be automated, including the writing of proofs. In his article ‘How Close Are Computers to Automating Mathematical Reasoning?’, Stephen Ornes highlights the creativity, intuition, inductive reasoning, and deductive logic that go into conjectures and proofs, and discusses the views of many mathematicians on whether computers can replace them. He says, “Some mathematicians see theorem provers as a potentially game-changing tool for training undergraduates in proof writing. Others say that getting computers to write proofs is unnecessary for advancing mathematics and probably impossible.”

An informal discussion on this topic, ‘Computer Proofs and Artificial Intelligence in Mathematics’, took place in the Department of Mathematics, Indian Institute of Science (IISc), Bengaluru, with Professor Kevin Buzzard (Imperial College, London), Professor Viraj Kumar (Kotak IISc AI-ML Centre (KIAC), IISc), Professor Siddhartha Gadgil (Department of Mathematics, IISc), faculty, and students from IISc. How would artificial intelligence (AI) impact mathematics, research, and teaching?

“The system confidently does the wrong thing.”, said Kevin, talking about ChatGPT. Viraj expressed that there is a risk that students will learn to trust GitHub Copilot blindly. It is important to critique and check the code, which is what Viraj teaches his undergraduate (UG) students. This also becomes a good way of getting the students to focus, says Viraj. According to Siddhartha, ChatGPT may start with ‘rubbish’ answers, but it could improve with the correct prompts. On Siddhartha’s page on ‘Artificial Intelligence and Mathematics: My experiments in automating mathematics’ is an account of his conversation with ChatGPT.

Kevin suggests that interactive theorem provers (ITPs) be taught to final year UGs and not first-years, as the former would know the underlying mathematics, and they could teach the computer what they have learnt in the class. In Kevin’s experience with first year UG students, the weak students struggle with the mathematics while the smart students face the challenge of doing the same problem on an ITP. Kevin suggests working with individuals who have been exposed to advanced mathematics, and not with first-years.

Given these tools, what would be the required capabilities of next generation mathematicians (present-day undergraduates)? Kevin says we need more theorems included in the database, and if the computers cannot do it, then the students could be encouraged to do it!  Additionally, if a system can translate hard algebraic statements into Lean, a massive database is possible. It is necessary for computer scientists to work with mathematicians to achieve this.

One limitation of such a system is that its creativity appears to be restricted to proofs coded up by humans and limited combinations thereof. To improve the system’s creativity in arriving at new proofs, is it possible to feed an exploratory proof, possibly nonsense generated by randomness, and check with Lean if the proof is good? Given many proofs for a theorem, can the model come up with a different proof? Which theorems should be included in the library? Can the system tell us about the holes in the library? What makes a theorem elegant or useful? Can artificial intelligence quantify usefulness, surprise, elegance? Such questions were put forth during the discussion.