Terence Tao

There's a tool that you know is in there somewhere.

and you need to find it.

And so you can, there are various search engines specialized for Mathlib that you can do.

But there's now these large language models that you can say, I need the fundamental calculus at this point.

And I've said, okay, for example, when I code, I have GitHub Copilot installed as a plugin to my IDE.

And it scans my text and it sees what I need.

It says, you know, I might even type, okay, now I need to use the fundamental calculus, okay.

And it might suggest, OK, try this.

And maybe 25% of the time, it works exactly.

And then another 10%, 15% of the time, it doesn't quite work.

But it's close enough that I can say, oh, yeah, if I just change it here and here, it will work.

And then half the time, it gives me complete rubbish.

But people are beginning to use AIs a little bit on top, mostly on the level of basically fancy autocomplete, that you can type half of one line of a proof and it will tell you.

Yes.

Yeah.

So right now I estimate that the effort, time and effort taken to formalize a proof is about 10 times the amount taken to write it out.

Yeah.

So it's doable, but you don't, it's annoying.

But doesn't it like kill the whole vibe of being a mathematician?

Yeah.