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.
We’re reaching a point where the interesting part isn’t just whether an AI found the proof: it’s whether anyone outside the company can reproduce the result. Publishing Lean proofs is great. Keeping the model closed means the process stays a black box.
We’re reaching a point where the interesting part isn’t just whether an AI found the proof: it’s whether anyone outside the company can reproduce the result. Publishing Lean proofs is great. Keeping the model closed means the process stays a black box.