The number that matters is 460,000: lines of formally checkable proof that OpenAI posted to a public GitHub repository on August 1 to back ten claimed advances in mathematics and theoretical computer science. The blog post announcing them, dated the same morning, says the results came from an internal version of Astra, which it calls 'our next major model.' Each of the ten results ships with a Lean certificate, a machine-checkable formal proof, in the repo github.com/openai/ten-proofs under an Apache-2.0 license. We checked the files: every one of the ten compiles against Lean 4.32 and mathlib, and none contains a 'sorry' placeholder or a custom axiom, the two usual escape hatches.
The ten, as OpenAI states them: new upper bounds for high-dimensional sphere packing down to the Cohn-Elkies threshold; exponentially improved bounds for binary and spherical codes; a construction of non-sofic groups; a counterexample disproving Connes's rigidity conjecture; lower bounds for the permanent, including an arithmetic-formula bound of order n to the fourth over log n; an exponential parallel-repetition theorem for quantum games; polynomial-factor hardness for the closest vector problem; a sharp answer to Ehrhart's volume conjecture; a superexponential lower bound for multicolor triangle Ramsey numbers, which would settle Erdos problem 183; and counterexamples to the compactness and degeneracy conjectures, settling Erdos problems 146 and 180. OpenAI's framing is that each problem had been stuck for at least a decade. That framing is theirs, and so is the figure of roughly $2,000 in compute at Sol API rates for all ten.
Here is what is independently verifiable today, and it is more than nothing and less than proof. Verifiable: the repository exists, all ten Lean files are in it, the contents are as described above, two companion PDFs (the paper and the model's reasoning walkthroughs) download, and the repo ships configurations for independent kernel checking. Not verifiable yet: nobody outside OpenAI has reported rebuilding the proofs; no human mathematician has peer-reviewed them; and there is no expert confirmation that the formalized statements say what the informal theorems say, which is the step formalization can silently break. The strongest not-yet-ratified signal: erdosproblems.com, the reference tracker, still lists problem 183 as open with a $250 prize, while a smaller tracker already marked it solved on August 1. Thomas Bloom, who maintains that site, called the announcement 'big news' and 'as far as constructions go, this is big,' in posts quoted by The Decoder; we could not retrieve them directly.
On naming, precision matters because this is the reference people will link back to. The blog says 'an internal version of Astra, our next major model.' The phrase 'next major model family' comes from OpenAI researcher Noam Brown, who added, 'unfortunately no Millennium problems (yet),' and noted the model failed at other major problems. Everything else about the family is reported, not confirmed: The Information, via The Decoder, has Astra as a new class alongside Sol, Terra and Luna, with the GPT-6 versus GPT-5.7 decision undecided and no release date. OpenAI's own ethics note is worth quoting whole: 'claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system's contribution and the nature of genuine human intellectual work,' and the company says it takes responsibility for correctness while the arguments were model-generated. That is the right sentence to hold them to when the rebuilds come in.