腾讯混元 AI「Hyra」が加法組合学の50年未解決問題を解明

記事の3ポイント

1. 1

   50 年未解決問題の完全解答

   Hyra は加法組合学における和集と差集の拡大指数に関する半世紀以上の難問に対し、2 が上確界であることを証明する一連の集合を構成し、完全な答えを提供した。

2. 2

   AI による数学的推論の新記録

   Hyra は既存の AI 補助手法で到達していた約 1.28 の指数値を超え、自然言語での数学的構成と証明を提案することで、計算機科学と数学の融合領域における新たな可能性を示した。

3. 3

   形式化証明と公開データの提供

   同モデルが導出した核心となる数学的証明は Lean 4 で形式化され、論文預稿、明示的な構成法、および形式化コードがすべて公開されたことで検証が可能になった。