When students go to university
to study mathematics, the undergraduate fantasy that we teach
is that we have this bedrock of axioms and everything is built solely on
these axioms through deductive argument, and that we have a towering edifice
of brilliant mathematics, all of which is solidly established
in an incontrovertible way. it's a beautiful kind of conception, the problem is that's not true. It's not even close to the truth. It's almost impossible
to live up to that fantasy. Some of the top mathematicians
in the world have been looking at this as a philosophy question, I've been actually working with A.I. If you start always inputting your ideas or proofs into a machine,
at what point does the machine do a better job of helping
guess the next step? Obviously this is something very
hot right now. It's moving fast
and the question becomes, well, what is it we want from proofs? What have we
historically needed from proofs? What is it we believe when something's proved and how does AI change that? These are massive questions that that are popping
out of the woodwork right now. I'm Andrew Granville, I work in analytic number theory. When I was young. I worked on Fermat's
Last Theorem before it was proved. Today, I work in ideas of L functions
and multiplicative functions. But I'm interested
in all different aspects, including computational
and algorithmic questions. I've long been interested in popular
writing in mathematics. My sister is a writer. We've been thinking
it would be fun to do a graphic novel in mathematics, so we worked together
to develop it and eventually wrote it. In the graphic novel,
I felt like there was room for us to develop philosophy, A philosopher of mathematics. Michael Hallett, read it and he was very interested in the way we portrayed mathematics being done. You cannot prove them
because you cannot go back to anything more primitive
than those propositions themselves, they are not in need of justification. Talking to Michael,
I realized there is this debate of what it is we mean
when we say we've got something proved. So Aristotle said that to prove
something is true, to establish it's true, your argument should rest on what he called primitives, things
you already knew to be true. And eventually there's got to be some atoms there, the so-called axioms
that you rest all your arguments on. the basic things you cannot define,
so like point, line, plane, if you're talking about geometry,
you can't define those. What you do instead is lay down
some axioms about them. The phrase that comes to my mind
is these truths are self-evident. Um, which, you know, is interesting at many levels when you compare it to mathematics. I mean, there's a certain arrogance
about it. The way it's traditionally been done
is that we publish papers and there's papers that put in journals or books,
and those books are put in libraries. And then when we wanted to verify a truth,
we go to the library and we check out the book and we'd
see if it was exactly as we wanted it. It would help us gain new understanding, or we'd have to revise
what was in those books. Today, The artificial intelligence
that is used for proof they're doing something similar, except
they're going to store that information within the program. So programs
like Lean have a library of things already proven based on axioms
and then with suitable work, and it's complicated, a mathematician can input their proof
into Lean and verify all the steps of logical,
at least according to Lean. So what does Lean do? I think I have a proof of a theorem
and I want a formal proof. I've written something that I am a bit
iffy about. I don't want to get into all of the details
of the ins and outs of know, as you sort of go back to the Tree of Knowledge,
everything's really going to work. So the idea is to input that into Lean. It acts like an obnoxious colleague
who just won't let go. If they don't understand, they will not
stop pestering you with annoying questions. But sometimes those colleagues
actually help you because by explaining it to them
you realize, Oh yeah. Oh, it's simpler than I thought. This is particularly famous example
by Peter Scholze. He had a very, very difficult proof
that he wasn't 100% sure of. He would try and say, well, this is true and you should know this Lean and Lean would say, I didn't know this at all. You're going to have to explain this better. The bits where he had been uncomfortable
with what he'd written, it was where it asked the most questions. So he felt okay, that was verification
and it was sensibly asking the right questions. So it's an exciting time. The question is, will machines
change mathematics? How do you get computers
to lead you in a proof, not just follow you or make suggestions,
but prove things itself? This is something in its infancy, a lot of the work on computer
generated proofs up to now has not done much of consequence. Very interesting within itself,
but not in the bigger picture. But there are some very interesting,
exciting new ideas, which one has some optimism
that we may see the start of generating
interesting new proofs? And so this starts
to become a little frightening, I mean, we value our profession. We value our work by the profundity of proofs. But if we can rely on a machine to get all the details
right, well, most of the details right, then who are we? What is our training? What is it that we value? So when we don't need to think about proof, then we're not going to be trained
in thinking about proof. So who are we going to become? We're going to become more like physicists,
probably and say any old nonsense, and just hope the computer verifies it. I think it's very hard to predict
what even will be the point of doing mathematics in 30 or 40 years time. The idea of computer generated proofs these present new possibilities. Over time, we see, of course, more and
more things that computers are able to do, and its very unclear what limits there are.
