Yes, Lean verified proofs could be wrong, but the chances for that are much smaller than human not spotting error (in absence of formal verification). IIRC the main concern that Tao voiced are indeed impenetrable proofs that humans won't understand, but not concerns about truthfulness (I might have missed something though, so if he or other Fields medalists have talked about that recently I'd be grateful if you could link it).

> These things are ok-ish to halfway decent at coding tasks with a ton of babysitting and still make tons of extremely simple errors almost constantly, why should math be any different?

1) AI is winning programming competitions, 2025 was probably the last year we've had human participant winning* 2) Math is different because there's formal verification.

* Of course competitive programming is different than enterprise programming, but competitive programming is closer to math.