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

OpenAI Says Astra Solved 10 Math Problems With Lean Proofs

OpenAI paired its Astra proof claims with Lean certificates and a public repository. That makes the results checkable, but it does not make the unreleased model or peer review disappear.