10件の問題の解を見つけるのに必要だったトークンの総数は、仮にSol APIの料金で計算すると、およそ2,000ドルに相当します。これらの解は、筆者らの次の主要モデルであるAstraの社内版によって得られました。人間が同じAstraを使って議論を原稿にまとめ、その後、モデルが各議論をLeanの証明書(Lean certificate)で形式化しました。筆者らは、それぞれの解について、モデルが思考過程を語った記録も公開しています。
5月の反証事例と未解決問題での評価
筆者らは5月に、未発表のモデルを評価している際に発見された、Erdősの単位距離予想に対するAI生成の反証を共有しました。この研究は、すでに数学と理論計算機科学のさらなる進展のきっかけになっています。筆者らは、開発中のモデルを未解決の研究問題で評価することも続けています。
提示された数学上の問題はすべて、それぞれの数学コミュニティにとって大きな関心事であり、そのうちのいくつかは数学全体にとっても広い関心事です。
得られた結果の内容
高次元球充填について、球充填密度の新しい上界がCohn–Elkies閾値まで下がる形で得られました。二元符号と球面符号について、任意に指定した最小距離での二元符号の最大サイズに関する評価が指数的に改善され、高次元の球面符号にも類似の結果が得られました。非ソフィック群の存在を確立する構成が得られ、これは群論の中心的な未解決問題に取り組むものです。Connesの剛性予想は、ある種の群がそのフォン・ノイマン環によって一意に決まるという長年の予想であり、これが反証されました。算術回路計算量の分野で、パーマネント(permanent)を算術回路と算術式で計算する場合の新しい下界が示され、その中にn^4/log nのオーダーの算術式の下界が含まれます。量子並列反復について、一般的な2人用量子ゲームに対する指数的な並列反復定理が得られ、これは古典的な計算量理論の基本原理を拡張するものです。ポスト量子暗号に関連する基礎的な格子の問題である最近ベクトル問題について、多項式因子の近似困難性が得られました。Ehrhartの体積予想について、重心が唯一の内部格子点である凸体が取りうる最大の体積があらゆる次元で決定されました。多色ラムゼー数について、多色の三角形ラムゼー数に対する超指数的な下界が得られ、Erdős問題183が解決されました。極値数予想について、極値グラフ理論のコンパクト性予想と退化性予想に関する結果が得られ、Erdős問題146と180が解決されました。
解は社内版のAstraで得られ、その議論を同じモデルを使って人間が原稿にまとめました。
筆者らは、帰属(attribution)は結果がどのように生み出されたかを正直に反映すべきだと考えています。AIシステムが完全に生成した証明について人間の著作だと主張することは、システムの貢献と、真の人間の知的営みの性質の両方を誤って伝えることになります。筆者らは原稿の準備と、証明のLeanでの形式化(formalize)を手伝い、その正しさに責任を持ちます。一方、数学的な議論そのものは筆者らのシステムが生成しました。
数学研究に貢献できるシステムの登場は、テクノロジー企業だけでは答えられない問いを投げかけています。数学におけるAIの役割については多くの見方があり、筆者らは、AIと数学に関するライデン宣言（Leiden declaration on AI and Mathematics）の署名者を含め、AIの影響を懸念する人々に深い敬意と理解を持っています。
今回共有される10件の結果は、いずれも長年未解決だった問題を解決するか、大きく前進させるものであり、高次元幾何、符号理論、算術回路計算量(arithmetic circuit complexity)、群論、作用素環、量子計算量、格子暗号、極値組合せ論にわたります。
Astraは筆者らの次の主要モデルです。
筆者らは、数学的な議論そのものは自分たちのシステムが生成したものの、原稿の準備と証明のLeanでの形式化を手伝い、その正しさに責任を持ちます。
幅広いアクセスと数学コミュニティへの期待
AIシステムがより高度な研究協力者へと進化するにつれ、科学者と数学者が自分たちの分野の未来を進み、定義していくのを支えるうえで、幅広いアクセスの確保が根本的に重要であると筆者らは考えています。筆者らは、数学コミュニティが今回示した結果に深く取り組み、文脈の中に位置づけ、結果の背後にあるアイデアを新たな研究と発見によって生かしてくれることを望んでいます。