[jw1224]

> If we […] tried to use these systems to solve the kinds of problems we need Einsteins, Hawkings and Taos for, then we would be in for one miserable disappointment after another

We can literally watch Terence Tao himself vibe coding formal proofs using Claude and o4. He doesn’t seem too disappointed.

https://youtu.be/zZr54G7ec7A?si=GpRZK5W1LDvWyBBw

[wizzwizz4]

He's the only person I know of who can actually get good results out of these systems (though I know several people who claim they can). What he's doing is fundamentally not the same thing as what most "vibe coders" are doing: take the autocomplete away, and he's still a talented mathematician.

[gjm11]

Sure, but what he's doing is very much not using Claude or o4 to do things we need Terence Tao for.

I'm not saying today's AI systems aren't useful for anything. I'm not saying they aren't impressive. I'm just saying they're nowhere close to the "Einstein, Hawking and Tao in your house" hyperbole in the OP. I would be very, very surprised if Terence Tao disagreed with me about that.

[mufthun]

You can literally watch Terrence Tao stream himself formalizing existing proofs that he already formalized before.