Find XO: OpenAIが数学の結果約400件を一度に公開し、数学者たちは検証に数年かかるとみている(theverge.com)

- 原文によると、OpenAIが公開したAI生成の数学の結果は約400件で、700編を超える論文にまたがっている。組合せ論、幾何学、整数論、理論計算機科学など複数の分野が含まれる。 - OpenAIは、719編の論文のうち主要な結果の約300件をLeanで形式化したと明らかにした。Leanは、証明が論理的に正しいかをコンピューターが確認する助けとなるプログラミング言語である。原文はこれを約42%と記している。 - 数学者たちは、Leanのコードがあっても、証明が論文の主張と実際に一致しているかは別途確認する必要があると述べた。一部の論文は参考文献が短く、出典の記載が不十分だとの指摘も出ている。 - スタンフォード大学の数学者Jared Duker Lichtmanは、リーマン予想の進展、ホッジ予想の特殊な場合、4次元のKakeya予想に関連する結果を重要だと評価した。これは取材に応じた研究者の評価であり、原文の時点でこれらの結果の検証が終わったとの内容は確認できない。