OpenAI's Astra claims ten long-open math results

OpenAI says an internal version of Astra produced ten results for mathematics and theoretical-computer-science problems whose main results had seen no progress for at least a decade, using roughly $2,000 of model tokens at Sol API rates. The company’s technical announcement says humans prepared the arguments as manuscripts and the model formalized each one in a public Lean repository, extending the research trajectory behind OpenAI’s earlier Erdős-conjecture disproof. Research-tool builders should file away the workflow—not just the claims: cheap candidate generation becomes more useful when it ends in machine-checkable artifacts, though independent mathematicians still need to judge novelty and significance.