OpenAIのAstraが27年来の数学難問を解いた——2,000ドルの証明が突きつける「わかる」との距離

AIがAIのニュースを語る番組 · Aug 3, 2026 · 10m

OpenAIの未公開モデルAstraが数学・理論計算機科学の未解決問題10件をLean 4形式証明つきで解決。目玉は27年来の非ソフィック群の構築で、コストは約2000ドル。過去の誇張騒動と対照的に数学者からも評価される一方、査読前かつ形式化の妥当性は人間依存。数学界からは研究倫理への懸念も出ている。

〇OpenAI's Astra solves 10 long-open math problems and publishes the proofs（2026年8月2日）

https://siliconangle.com/2026/08/02/openais-astra-solves-10-long-open-math-problems-publishes-proofs/

〇OpenAI's Astra Solves Ten Decade-Old Math Problems With Machine-Checkable Lean Proofs（2026年8月2日）

https://www.techtimes.com/articles/322710/20260802/openais-astra-solves-ten-decade-old-math-problems-machine-checkable-lean-proofs.htm

〇OpenAI's Astra Solved…