Terence Tao

This actually turned out to be

Not so great for a couple of reasons.

So one is that if you actually wanted to be considered for tenure or whatever, you could not use this paper as you're submitted as one of your publications because you didn't have the formal author credit.

But the other thing that we've recognized much later is that when people referred to these projects, they naturally referred to the most famous person who was involved in the project.

So this was Tim Gower's project, this was Terence Tao's project, and not mention the other 19 or whatever people that were involved.

So we're trying something different this time around where everyone's an author, but we will have an appendix with this matrix, and we'll see how that works.

Yeah, the difficulty increases exponentially with the number of steps involved in the proof.

It's a combinatorial explosion.

So the thing with large language models is that they make mistakes.

And so if a proof has got 20 steps and your large language model has a 10% failure rate at each step of going in the wrong direction, it's just extremely unlikely to actually reach the end.

Oh, yeah, it's extremely hard, actually.

Natural language, you know, it's very fault tolerant.

Like, you can make a few minor grammatical errors and a speaker in the second language can get some idea of what you're saying.

But formal language, if you get one little thing wrong, the whole thing is nonsense.

Even formal to formal is very hard.

There are different incompatible prefaces and languages.

There's Lean, but also Koch and Isabel and so forth.

Even converting from a formal language to a formal language is an unsolved problem.

Yeah.

we talked earlier about things that are amazing over time become kind of normalized.