Terence Tao

I mean, we didn't understand, most of us didn't understand the proof.

We understand sort of high-level details.

In fact, there's an ongoing project to formalize it in Lean.

Kevin buzzed it, I think.

It's really difficult to formalize now.

I guess you're right.

The objects that they use, you can define them.

They've been defined in Lean.

Just defining what they are can be done.

That's really not trivial, but it's been done.

There's a lot of really basic facts about

these objects that have taken decades to prove in all these different math papers.

And so lots of these have to be formalized as well.

Kevin Buzzard's goal, actually, he has a five-year grant to formalize Fermat's last theorem.

And his aim is that he doesn't think he will be able to get all the way down to the basic axioms

But he wants to formalize it to the point where the only things that he needs to rely on as black boxes are things that were known by 1980 to number theorists at the time.

And then some other work would have to be done to get from there.

So it's a different area of mathematics than the type of mathematics I'm used to.

In analysis, which is kind of my area, the objects we study are kind of much closer to the ground.

I study things like prime numbers and