OpenAI Says Astra Solved 10 Open Math Problems With Lean Proofs: The proof files are public, but the new model is still private.

In other words its all marketing bullshit.

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