OpenAIの内部モデルAstraは、数学および理論計算機科学にわたる10の長年の未解決問題に対する解答を生成し、その論証はLeanで形式化された。これらの結果は高次元幾何学、符号理論、群論、量子複雑性にまたがり、少なくとも10年間進展が見られなかった問いに対処している。

  • 高次元球充填: Cohn–Elkies閾値に至るまでの球充填密度の新規上限。
  • 二進符号および球面符号: いかなる指定された最小距離においても、二進符号の最大サイズに関する指数関数的に改善された境界。
  • ノンソフィック群: グループ論の中核的な未解決問題に対処するノンソフィック群の存在を確立する構成。
  • コンネスの剛性予想: 特定の群がそのフォン・ノイマン代数によって一意に決定されるという長年の予想の反証。
  • 算術回路複雑性: 算術回路および式を用いて永久項を計算するための新規下限。
  • 量子並列反復: 一般的な2人量子ゲームに対する指数関数的並列反復定理。
  • 最接近ベクトル問題: 後量子暗号に関連する最接近ベクトル問題の近似における多項式因子の困難さ。
  • エーハルトの体積予想: 各次元において重心が唯一の内側格子点である凸体の最大可能な体積の決定。
  • 多色ラムゼイ数: 多色三角形ラムゼイ数に関する超指数関数的下限により、Erdős問題183を解決。
  • 極値数予想: 極値グラフ理論におけるコンパクト性および退化性予想に関する結果により、Erdős問題146および180を解決。

OpenAIは、人間が原稿の準備と証明の形式化を行った一方で、数学的論証はシステムによって生成されたことを強調し、帰属および研究におけるAIの役割について疑問を提起している。