OpenAI、社内AIがリーマン予想の関連難問を証明と主張 論文722本をGitHubで公開

OpenAIは10月6日（現地時間）、社内のフロンティアモデルが生み出した数学の新たな成果を、論文の原稿や「Lean」による形式証明とともにまとめて公開した。公開先はGitHubのリポジトリで、現時点で722本の原稿が収録されている。多くには形式証明が付くが、すべてではない。形式化していない結果には問題が含まれる可能性があるとして、見つかれば速やかに修正すると添えている。

面白いのは、この発表が「論文を出した」というより「計算の明細を出した」形になっている点だ。OpenAIによれば、評価期間中に与えた問題は約4000問で、その中から一定の重要性を満たす722本に絞り込んだ。1件あたりの計算量は平均で「ChatGPT Pro」の思考機能を約3時間使った分に相当するという。成果を派手な数字で語るのではなく、どれだけ試して、どれだけ捨てたかを見せる。公開にあたっては数学者の独立組織AGMAIの提言を参考にしたとされ、数学界が求めてきた情報の出し方に寄せた動きだといえる。

ただ、引っかかるのは背景である。9月にはナビエ・ストークス方程式を解決したとする発表が、先行研究を進めていた数学者から経緯を問題視され、論争になった。今回の公開は、その信用を立て直すための見える化として読むのが業界的には自然だ。数学では主張より検証が勝つ。Leanの形式証明は検証を機械にやらせる仕組みであり、AI企業が自社の基準で採点を済ませるのではなく、外からの確認を通せる形にしたかどうかが本当の評価軸になる。

中小企業の実務に引き寄せれば、ベンダーがAIの成果や性能を発表したときに、「誰が検証したか」「どんな条件で試したか」「何を捨てたか」の3点を聞く習慣をつけるといい。派手な数字より、その数字の作り方を説明できない相手は、導入後の検証も任せにくい。