I have the same questions about human mathematicians!
I can't tell if xkcd #435 is still true, or if math is just as mushy as everything else seems to be. When a math proof can only be understood by a handful of people, what does that mean about that proof? I think the LLMs are pushing a problem that existed already and pushing it further.
That's why OpenAI also published machine-checkable proofs.
The process is very, very faintly similar to running a typechecker over your software sources.
They're publishing machine checkable proofs because that's the only way they, themselves, can check them.
They don't understand the math either.
For 3.5 days we had a machine checkable proof the Collatz conjecture was false. There turned out to be a bug in the machine checker.
Yes, however any LLM agent you asked about that proof could tell you that. (And even most humans who know a little bit about the bug.)
You are right that Lean isn't great in this respect, and people are working on proof formalisations that are less prone to bugs.