So youre suggesting they secretly have Einstein standing in the server rack, making loud fan noises with his mouth and just typing really fast?

Either the problems were solved or they weren't. If they were, then that's evidence enough; doesn't matter if they model isn't publicly available.

Having those sudden breakthroughs come from a person or even a large group of mathematicians, suddenly and all at once, would be more surprising than a well-harnessed LLM figuring it out.

With that said, I'm curious about peer review of the actual proofs. Just because Lean builds them doesn't mean they're materially valid. It could very well be that it's completely wrong and it just hallucinated well enough to fool OpenAI into publishing it, which would be a hilarious egg-on-face moment

A few of the erdos problems have been independently verified. It's legit.