Again, you don't need to check the proof, Lean does that. You need to check the statement, which is a much easier task. So yes, you are wrong. Skepticism is good, but it is usually just ignorance.
It's surprisingly easy to prove something subtly different than you intend actually. Digesting and understanding a theorem statement can often take significant time and expertise.
LLMs are very good now - meaning you do actually need to check the proof to make sure a misaligned agent didn't reward hack by exploiting some issue in lean or adversarially incorrectly formalize the statement in a way that's subtly wrong and easy to miss when you're trying to dump 75 trillion proofs on the Internet to drive hype that also makes the proof easier to solve. Probably also something you can use ai to help with though - I'm sure the other lab is having a bunch of llms adversarially review all these proofs since finding issues hypes _their_ IPO cycle. As the software world is learning - don't review ai code until a different ai has reviewed it lol.
What a bizarre take. Skepticism is usually ignorance!?
The should be on AI labs to definitively prove their extraordinary claims, and they should be paying mathematicians to do so given that the results from these machines are so opaque and often nonsensical.
