重要な留保を伴う形式的な主張

ソフトウェア開発者のダン・アブラモフは、AIモデルと約1か月取り組んだ結果、数学者ジョン・コンウェイがomnific integersについて提示した予想のLeanによる証明を作ったと述べている。結果は9月18日に公開されたが、確定した数学上の突破口として扱うべき段階ではない。アブラモフは、独立した数学者による検証が済んでいないと明言している。

アブラモフの説明によると、提出した証明はPalomarレジストリーの機械的な検査を通過した。Leanと当該分野に詳しい人々も、形式化された命題は妥当に見えると伝えたという。Leanのカーネルは、各証明段階が宣言された仮定から導かれるかを検証するため、こうした検査には意味がある。しかし、それだけで、符号化した命題がコンウェイの意図した予想を完全に表していることや、構築過程で問題のある仮定をすべて避けていることまで確立するわけではない。

予想が扱う内容

コンウェイの細分化予想は、超現実数の体系に含まれるomnific integersの因数分解に関わる。単純化して言えば、2つの積が等しいとき、それらの因数を4つの成分に細分化し、等式の両辺にまたがって組み直せるというものだ。普通の整数にも同様の性質がある。同じ数の2通りの因数分解は、両辺を説明できる、より小さな因数へ分解できる。

超現実数は、なじみのある整数や実数を大きく超え、無限に大きな値や無限に小さな値も含む。その構成は、既に作られた数の集合の間に新たな値を置くことから始まり、超限的な段階へ続く。omnific integersは、このはるかに大きな体系の中で整数に相当する部分を形成する。そのため、有限の整数では当たり前に見える性質でも、この設定では本格的な証明が必要になり得る。

アブラモフはClaudeに超現実数研究の未解決問題を提案するよう頼み、その後この問題を選んだ。そして、主張の形式化と証明を試みる過程でモデルを使った。彼の説明は、過去の数学研究が問題をどう帰着したかについて、モデルが初期に間違えたことも記録している。システムの提案には、なお確認と修正が必要だったことを強調する事例だ。

なぜ検証がなお不可欠なのか

形式化では、証明支援系が内部の論理的な段階を検査するため、証明の精査を容易にできる。しかし、専門家の検証が不要になるわけではない。数学者は依然として、定義が既存の文献と一致するか、取り込んだ結果や仮定が適切か、主張する定理が歴史上の予想に対応するかを調べる必要がある。

したがって、この出来事は、報告された成果であり、精査への呼び掛けであると理解するのが最も適切だ。専門家が定式化と証明の両方を確認すれば、AI支援の探索と証明支援系が、非専門家による難しい研究課題への取り組みをどう助けるかを示せるかもしれない。それまで、最も確実に言えることは、より限定的である。機械に受理されたLeanの成果物が存在し、著者は予想を証明したと考えているが、その主張が未検証であることを率直に認めている、ということだ。