astra closed ten open problems in mathematics

https://openai.com/index/ten-advances-in-mathematics/

openai published ten solutions to mathematical problems where the best known result had not moved for at least ten years. All of them were found by an internal version of astra — the next big model — and the tokens spent on the search cost about $2000 at sol api rates. Each proof was written in lean and put into the openai/ten-proofs repository; next to it lie a paper and transcripts of the model’s reasoning.

$2000 for ten results of the “a decade without progress” kind is the number that will be quoted most often. But it counts only the tokens spent searching for a solution, at api rates: it leaves out training the model, the work people did on the manuscripts, and the failed attempts on other problems. The real cost may be several times, if not an order of magnitude, higher.

And if for some reason you are still not a millionaire — here are ready-made business ideas based on these problems, as suggested by Opus 5 ultracode:

• Expert testimony in patent and arbitration disputes over coding and compression.
• Compressing the model and the runtime kernel to fit the customer’s hardware.
• Verifying technical claims before a deal.
• A voice codec for narrow channels.
• Pessimistic join size bounds for query planners.
• A codec and channel simulator for DNA storage.
• Constellation shaping for satellite and laser links.