Kevin Buzzard, a mathematics professor at the Imperial College in the UK, starts a five-year sabbatical (well, kind of) in October this year. Not only does he get half a decade off teaching and administrative work, but he will also receive nearly 1 million Euros to spend during this time. 

Is he about to embark upon some daring expedition? In a way. Buzzard is about to translate Andrew Wiles’ famous proof of Fermat’s Last Theorem into a form that is legible, and therefore verifiable, by computers. According to one commentator on the platform Reddit, ​“This will either be a big waste of money or something amazing.”

Mohan R, who teaches mathematics at Azim Premji University, would place his bets on ​‘something amazing’, but he does have some concerns, too. Nandita Jayaraj sat down for a conversation with him to find out more.

Nandita: So, Kevin Buzzard has set out to use a software called Lean to verify the 129-page proof of Fermat’s Last Theorem. This is not to suggest that there is any question about the validity of Wiles’ proof; mathematicians (human ones) have already confirmed this. However, if Buzzard is successful, it means that Lean has the potential to become a valuable tool in the arsenal that will take us to a world where machines can do maths. At least that is what some mathematicians and computer scientists say.

Mohan: I would divide us mathematicians into three groups — and I have met at least one example from all these groups! 

1. The very, very optimistic — ones who believe that AI will take the field to a new level. I am among them. 
2. Those who see AI as a negative thing — as they believe mathematics is, and should be, a human endeavour.
3. A large group — who are taking a neutral stance; they are aware of the new developments in terms of implications of AI in mathematical research, in particular about Lean, Coq, and other proof assistants, but they are taking a backseat for now. They want to wait and watch how AI shapes the landscape. 

Nandita: It is not just Kevin Buzzard who is using Lean. It was also recently used by a group of star mathematicians (including Terrence Tao) to verify their proof of an intriguing conjecture proposed by Hungarian mathematician Katalin Marton in the 1990s. While trying to figure out what exactly Lean is, I realised that it cannot prove theorems itself. It is more of an autocorrect mechanism if I understand correctly. 

Mohan: It is important to first realise that Lean itself is not AI. It is one of the many computer tools that can help mathematicians with their proofs. After humans write a proof, we want to ensure that all the steps are correct. Computers can do this now, and a tool that does this is a proof verifier. 

On the other hand, while writing the proof, I may get stuck, or I may end up spending too much time trying to manipulate some mathematical expressions. Computers can help here too. They can suggest what to do next or simplify something. In this case, I am using the tool as a proof assistant. 

So, which one is Lean — a verifier or an assistant? Being relatively new to Lean, I spoke about it with my colleague Divakaran who uses it more often, and he said it was somewhere in between. 

Nandita: It is interesting that despite there being several other tools, Lean is the one making the most news… 

Mohan: Actually, tools like Coq and Isabelle were popular proof verifiers even before Lean came about. I know that Coq was used to formalise (convert to computer code) all school geometry. There have been instances of a large group of mathematicians using various proof verifiers to formalise lengthy proofs of important theorems, such as the Feit-Thompson odd-order theorem and Kepler’s conjecture.

Close to home, IISc mathematician Siddhartha Gadgil used the programming language Scala to improve a proof as part of the popular Polymath project back in 2018. These programs were built by mathematicians and educators, a small community without much support, unlike Lean, which has Microsoft as a parent

Having such strong backing means that Lean’s library is huge and can be accessed by anyone. Many high-profile people are using it and teaching others how to use it. I think the reason Lean is in the limelight is not just because it is being used by mathematicians, but because it is being used by mathematicians who are popular communicators too. 

Nandita: We are not yet at a time where machines can turn into mathematicians. But there are signs that we are getting there. 

Google’s Deepmind laboratory recently made two big announcements: 

1. An AI programme AlphaGeometry, which according to them ​“solves complex geometry problems at a level approaching a human Olympiad gold-medalist”; and 
2. Google’s AI tool FunSearch had come up with a new solution to the cap set problem, famous in the field of combinatorics.

Computer scientist Yuhuai ​“Tony” Wu, has said that he sees a future with an ​“automated mathematician” that has ​“the capability of solving a mathematical theorem all by itself”. Proponents of Lean, including creator Leonardo de Moura say that the software has the potential to tackle the challenges in the way of generative artificial intelligence (AI) becoming a reality in mathematics. 

Mohan: It may happen, but there is still some way to go. If we are talking about creating a computer programme that is as good as a research mathematician, then as Timothy Gowers says, we need anywhere from 10 to infinite years! 

To use Lean, you need to be able to formalise mathematical statements. A statement that may seem simple to us, such as ​‘the sum of any even numbers will always be even’ will not be understood by a computer as it is. We even have to explain to it what we mean by an ​‘even’ number. This process of translation is called formalisation. 

As of now, learning Lean is a very steep learning curve. It reminds me of when the typesetting system​LaTeX was introduced. In its early years, it was very difficult for people to use. But over time, it became much more usable and we all picked it up. Today, LaTeX is standard for all mathematicians to use. Lean is not yet at that level.

Nandita: But this didn’t stop Kevin Buzzard from starting the Xena Project in 2017, right? He seems to believe that you can teach undergraduate students how to use Lean and formalise mathematics in their curriculum. Other mathematicians, like Athina Thoma and Paola Iannone, are exploring if tools like Lean can change the way undergraduates think about proof. As an undergraduate maths teacher in India, you must have some ideas about the use of AI in the classroom. 

Mohan: Kevin Buzzard’s primary aim was to create a library where lots of basic results are already available in Lean. Unless this foundation is built, every time we try to formalise higher mathematics, we will have to spend our time formalising the basic statements within it. Buzzard sensed that for Lean to fulfil its potential, undergraduate-level mathematics would need to be formalised. He thought learning Lean could be integrated with the undergraduate first-year course called ​‘How to Write Proofs’. But after teaching the course, he realised that it was not going to be easy. 

Interested students were indeed willing to be trained, but it was much harder to do it on a larger scale. When learning to write proof itself is a big skill, trying to learn Lean parallelly was not a good idea. Many students were not finding it useful. This will change in the future if Lean becomes a lot simpler to learn, and if developers come up with programmes that can read proofs that are human-written and convert them into Lean code. 

Nandita: A way to automate the formalisation process… 

Mohan: Yeah. That is what I think will be coming next.

Nandita: This past year, AI has become part of the vocabulary of the urban upper-middle class and ChatGPT has a lot to do with it. I am aware that academic communities are abuzz with debates on how to tackle its misuse by students. 

Mohan: If you ask it to write you an essay, ChatGPT certainly can, but as far as I understand none of the Generative Pre-training Transformers (GPTs) are very efficient in solving even basic arithmetic. That said, maths teachers may have problems when the capabilities of these tools improve. But I think this too can be a positive thing. 

For example, I see students struggle to understand what a proof means, what makes an argument sound. Teachers should give each student personal feedback, but this is impossible if I am teaching a class of 100 students. 

I imagine that 10 – 15 years in the future we may have a ChatGPT interface where a student can write a proof which would be auto-converted into code that could be fed into Lean or any other tool. The computer will be able to tell them if their reasoning is perfect, and whether there are any gaps. They would not require a teacher every time. This could solidify their understanding of how to do mathematics. 

Would they at some point be able to ask the tool to create a proof for them? Probably, but in my opinion, this won’t take them very far. Computers have limitations. You have to tell them what and how to think, give them the right prompts. And that requires a lot of effort. 

Nandita: What about the mushrooming concerns about AI taking away jobs? According to a 2023 report by Microsoft, 74 percent of Indian workers are worried about this. Satya Nadella added fuel to the fire when he warned that displacement of human jobs was indeed to be expected. 

Mohan: A lot of people are now graduating with PhDs in mathematics, and already many of them struggle to get jobs. Until they can get a stable job, these young PhDs join institutes as Research Assistants (RAs). A primary job of these RAs is to verify the work of mathematicians. 

For example, they are asked to check for gaps in a 20-page long proof and are promised a publication at the end. That is how it works today, but this scenario may completely be disrupted as AI gets more efficient. If my computer can do it, why would I hire a new RA? I may prefer to invest my funds to boost my computing power than to pay a human for the job. So emerging young maths PhDs will have to be top of the game to get a job. 

Nandita: That is scary. Although, it could be an opportunity for graduate students to get ahead of the curve and skill up, right? For example, a PhD student who is a seasoned formaliser and a user of Lean may now be a very attractive hire. 

Mohan: Certainly. But that is also something I am afraid of — that mathematics will become an elite game that demands that people not only have the right mindset but have also received the ​“right” training. If only people who know AI get the jobs, then mathematics will turn exclusionary. 

However, we can begin working on such issues by integrating AI tools into the curricular experiences of mathematics teaching and preparing students for new jobs that will be created.

About Mohan R

Mohan R is a faculty member at Azim Premji University.

About the Interviewer

Nandita Jayaraj is a Science writer and Communications Consultant at Azim Premji University.

Know more about the Mathematics programme at Azim Premji University: