Alexy interviews Sir Timothy Gowers on the Future of Math and AI

Interview recorded at Station F, Paris, at GOSIM AI on May 6, 2026.

Alexy Khrabrov speaks with Sir Timothy Gowers, Fields Medal-winning mathematician, professor at the Collège de France and the University of Cambridge, and a leading voice on automatic theorem proving. The conversation covers how mathematicians actually discover proofs, Lean, why formal textbook style can obscure understanding, the rise of Lean and auto-formalization, AI-assisted mathematics, and why mathematical understanding still matters in an age of increasingly capable AI systems.

Transcript

Alexy: Hello everybody, I'm Alexy Khrabrov, head of community at Lakesail. We are here at GOSIM AI Paris with Sir Timothy Gowers, professor at the Collège de France and the University of Cambridge, Fields Medal winner in mathematics, and a leading combinatorics researcher. Timothy, you keynoted the conference. Can you tell us how you came here and what you spoke about?

Timothy: I came because I was invited, and although I am a mathematician, I am also very interested in automatic theorem proving. I have a group in Cambridge devoted to getting computers to do mathematics.

Timothy: Our focus is somewhat different from much of the current work in that area. A lot of what is happening now could be called prompt engineering: giving problems to language models and improving the prompts so the models solve them more effectively. We are interested in something more fundamental: understanding how human beings solve mathematical problems.

Timothy: That is a mysterious question. In a very general sense, mathematics should not be fully algorithmic. If you ask whether an arbitrary mathematical statement has a proof, you run into issues related to incompleteness; there is no general algorithm that can do all of mathematics. But humans do mathematics because we do not usually work on arbitrary mathematics. We work on interesting mathematics.

Timothy: We are trying to understand what makes interesting mathematics tractable for human mathematicians with limited resources. If we understand that, perhaps we can teach AI systems to do mathematics better. That is why I am interested in AI, and a conference like GOSIM AI Paris is a good place to meet people and hear how others are thinking about it.

Alexy: One thing in your keynote struck me deeply. I went to one of the best math schools in the Soviet Union, though I probably should have studied history. I love Cicero and the humanities, but in the Soviet Union the humanities were constrained by Marxism-Leninism, so math was the path for people who wanted to do something real.

Alexy: I often found mathematics antisocial. Math books gave dense statements, then an answer, and in between phrases like "it is an exercise to the reader" or "it easily follows." I thought I was not smart enough because it did not follow easily for me.

Alexy: In your keynote, you said this is a poor way to help people understand mathematics. You also said LLMs often imitate that antisocial mathematical style because they learn from books written that way. It made me realize that mathematics could be more humane. You said you are interested not only in the result, but in how a mathematician arrived at the result. How do you approach that?

Timothy: At the beginning of the twentieth century, mathematics was put on a rigorous footing. People developed axioms such as ZFC and formalized what mathematical proof means. That was extremely important and positive, but it had an unfortunate stylistic consequence. Mathematicians began writing in a formal logical style, and something of the human process was lost.

Timothy: I have tried to counteract that throughout my career, long before AI or automatic theorem proving entered the picture. I examine how I come up with proofs, and I revisit arguments I learned as a student. Instead of merely accepting them, I ask how someone could have thought of that argument in the first place.

Timothy: Sometimes, especially after teaching a proof, I suddenly see how it could have been discovered. For me there has always been a strong link between explaining mathematics well to humans and explaining it well to computers. I hope that, in the future, we will teach computers to think about mathematics in a more human way, and then they will be able to explain their work to us better.

Timothy: At the moment, AI systems often copy the style of textbooks and simply give the answer. Sometimes that is not what you want.

Alexy: I remember that vividly from school. School 57 in Moscow was one of the most famous math schools in the Soviet Union. Many graduates became professors; others became very successful in computers and business. To enter the math class, you had to pass a series of exams.

Alexy: I once read a number theory book and memorized a proof mechanically. During an exam I explained the steps until I forgot the next one. The examiner looked at me as if the conclusion should naturally follow, but I had not understood the underlying idea. I had only memorized the moves. That experience made me think I did not really understand mathematics, but perhaps the problem was that the explanation had been too mechanical.

Timothy: A good measure of understanding a proof is how much you can compress it. At the lowest level, you memorize each line and what comes next. At a better level, you remember five key ideas, with routine calculations between them. At an even better level, you see that those five ideas are all expressions of one idea. At the deepest level, the whole proof feels like the obvious thing to do.

Alexy: That matches my experience with integration and algebraic manipulation. People can learn to move symbols mechanically without understanding the principle. Children often do this too: everything seems fine until they encounter something slightly out of distribution, and then the understanding collapses.

Alexy: I want to zoom in on formal methods. In the 1990s, formal methods seemed like a small academic niche, disconnected from the real world. Then Leslie Lamport showed practical uses of TLA+, including work connected to systems such as Amazon DynamoDB. More recently, Lean and proof assistants have become prominent in mathematics. Do you see this as a breakthrough?

Timothy: It is certainly a breakthrough of one kind. The old argument was that mathematicians did not need the extra guarantee of formal verification. If a result was important, many people would read it; if there was a serious mistake, someone would usually find it. If it was not important, perhaps it mattered less.

Timothy: The other old argument was that formalizing a proof in Isabelle, Coq, Mizar, Lean, or another proof assistant took vastly more effort than writing a conventional proof. It was not worth it for most mathematicians.

Timothy: Two things have changed. First, conventional proofs have become more complicated, and some are so long that there is genuine worry about correctness. Fermat's Last Theorem, for example, took a long time to check.

Timothy: Second, Lean has developed, and people have built more tools and expanded mathlib. The barrier to formalization has fallen. Undergraduates can now formalize deep pieces of mathematics even when they do not fully understand them, as long as they can translate the proof line by line.

Timothy: So a phase transition has taken place. Another phase transition may be coming: auto-formalization may become good enough that people can formalize mathematics without learning Lean in depth.

Alexy: Vibe formalization.

Timothy: Exactly. One immediate consequence may be that journals no longer send articles to referees to check proofs in the traditional way. Computers could check the correctness of the proofs, leaving journals to judge whether the result is interesting.

Alexy: Do you think proofs will become fully automatic, with no human in the loop?

Timothy: I think that will happen eventually. I do not know how long it will take.

Alexy: Would you be comfortable publishing a proof if a Lean verifier said it was correct?

Timothy: If I judged the result interesting enough, I would be at least as comfortable, and probably more comfortable, with a proof verified in Lean than with a conventional proof checked by a referee who may not have read every detail carefully. The current system is far from perfect and depends heavily on webs of trust and acquaintance.

Alexy: You mentioned in your keynote that recent models can operate at the level of graduate students, at least some of the time. You also expressed concern that students may delegate low-level work to LLMs instead of doing it manually.

Alexy: In coding, the consensus has shifted quickly. The best developers use AI tools and become even more productive. Perhaps the same could happen with mathematics. Lean may become approachable because machines handle much of the formalization. Could this become part of mathematical education, with students working alongside Lean or a similar tool from the beginning?

Timothy: I do not know whether we will teach Lean directly, because learning Lean creates an additional barrier. The way you do mathematics in Lean is somewhat different from normal mathematics and can feel less intuitive, though perhaps that is because I grew up the other way.

Timothy: It may be something better than Lean: a platform with Lean running in the background, but with a more user-friendly interface. You might write in a higher-level language, perhaps integrated with LaTeX, while Lean or another proof assistant verifies what you write as you go. Lean could also be combined with automatic theorem proving tools. I think we will get to that stage.

Timothy: There is a race between people developing such platforms and AI systems becoming better at mathematics on their own. A very nice future would be one in which platforms make it easy to do mathematics and formalize it as you work: tools that help you think at your screen. Many people, including my group in Cambridge, are interested in this. If such a platform exists, AI systems can also be trained to use it. That is an opportunity for developers: building such a platform would have real impact.

Alexy: Let me close with a broader question. I come from the Soviet Union, where math and physics education were strong. Many people here come from China, India, France, and other places with strong STEM traditions. In some of those cultures, there is less sense that mathematics is only for certain people.

Alexy: We may be the last generation educated without AI. Now many people say you do not need to know anything because AI will solve it for you. AI is all math underneath, all matrices all the way down, but practical AI work is increasingly removed from the math. Many people can use AI tools without understanding gradient descent, matrices, quantization, or the underlying systems.

Alexy: As a professor of mathematics, how do you see the role of math as a foundation of science? Will we preserve it, or will it become a specialized niche?

Timothy: I do not know what will happen, and I am worried about it. In a panel on AI and education, someone said that we can outsource knowledge, but we cannot outsource understanding. I think that is true.

Timothy: If a society does not have a significant number of people who understand mathematics at some level, we risk becoming passive consumers under the control of these systems. On the other hand, people who do make the effort to understand mathematics will have a large advantage. If you know mathematics well, you will be better at using AI for mathematical work and better at understanding what the tools can and cannot do. I hope that message gets through.

Alexy: Do you still see young people entering mathematics who can become great mathematicians?

Timothy: I am lucky to be at Trinity College, Cambridge, where we regularly see incredibly strong mathematicians. They are still being produced somewhere and finding their way to Trinity. For the moment, the very best students are still noticeably ahead of what AI can do. There is hope for the future of mathematics.

Alexy: What do you hope to have achieved by next year?

Timothy: In my keynote I mentioned a platform my group is developing to encourage people to produce not just proofs, but transparent proofs where you can see where the ideas come from. My short-term hope is that this platform will be much more developed and that we can demonstrate it as a good way to think about mathematics.

Alexy: If you are ever in the San Francisco Bay Area, please come give a talk and demo the platform at our AI meetup. Or send a student. We would love to play with it. Thank you so much.

Timothy: Thanks a lot.