The proof is not the model. It's the pipeline.

OpenAI's post, dated August 1, says it covers ten results for problems where the main result had seen no progress for at least a decade. 1 The Hacker News item for the post had 462 points when retrieved. 2

The mechanics are more interesting than the headline: OpenAI says its internal model Astra generated the arguments; humans prepared manuscripts; then each argument was formalized as a Lean certificate. The companion repository publishes Lean 4 formalizations and build instructions. 13

That split changes the trust question. A checker can test a formalized statement, but it cannot decide whether a result is important, novel, or well-placed in the literature. OpenAI says the mathematical community still needs to engage with the results and place them in context. 1