OpenAIは2026年10月6日、未公開のAIモデルが未解決の数学研究課題に取り組んで得た372件の数学成果を公開しました。関連する証明や派生結果をまとめたマニュスクリプトの一覧で、一部には証明支援系Leanで形式化した証明も添えられています。[1][2]
今回の発表には、数学者が十分に調べ切れていなかった命題に対して、高性能なAIを使えば網羅的に証明を試みられるという意義が示されたと言えます。証明の方針策定から、検証、結果の整理までを半自動化できれば、これまで一研究者が研究に割ける時間に制約があるために取り残されていた問いが片付けられるようになります。
OpenAIが公表した命題の証明のすべてが数学の方向性を変えるような重要な成果だとは言えないものの、こうした研究の進め方はもはや「数学の工業化」であり、パラダイムの変化に巻き込まれつつある数学コミュニティからは驚愕（もしくは怨嗟）の声が上がっています。最先端のAIモデルを擁する企業から一度に372件という規模の成果が発表されるという事態に際し、その価値と意味について考えてみます。 “数学が工業化される時代：372件の未解決問題に対してOpenAIが証明を公開” の続きを読む