OpenAIの次期主力AIモデル「Astra」が10件の数学・理論計算機科学の課題で新成果、証明をLean 4で形式化し機械検証可能に https://gigazine.net/news/20260803-openai-astra-lean/ #gigazine