Ten advances in mathematics and theoretical computer science

OpenAI's Astra model has solved or made progress on ten longstanding mathematics problems spanning areas like geometry, coding theory, and quantum complexity, with solutions formalized in Lean (a computer-verified proof system). The company emphasizes responsible attribution, stating that AI-generated proofs should be honestly credited to the AI system rather than claimed as human work.