Ten advances in mathematics and theoretical computer science

OpenAI says, in wording quoted by commentators, that it set an internal version of Astra, its next major model, on ten mathematics and theoretical computer science problems with no progress on the main result for at least a decade. Alongside that announcement, it released Lean formalizations: versions of the results expressed in a language designed for machine-checkable mathematics, with build instructions for checking them.

Simon Willison's commentary separates inspecting the published results from understanding how they were discovered. He calls the transparency decent but asks for the original prompts; the accompanying reasoning walkthrough is a model-generated reconstruction based on unpublished reasoning traces. Readers can inspect the formal statements and checking procedure without having a complete record of the search that produced them.