Hacker News Reader

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.

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.

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