Conway予想の証明を「バイブ」した方法

Conway予想の証明を「バイブ」した方法 2026年9月18日 好きなだけ支払う 数ヶ月前、AIによる数学の成果がヘッドラインを飾るようになりました。「ブレークスルーを起こせ」はTwitterのミームになりました。当然、私も、数学の初心者である自分が、未解決の数学的問題を見つけ、それを最先端のモデルに解かせることができるのかどうか、興味を持つようになりました。私の自由な時間と大量のトークンを丸々1ヶ月費やしましたが、ジョン・コンウェイが50年前に提唱したこの予想のLean証明を得られたと信じています。Conwayの洗練予想は、全能数（omnific integers）が洗練（refinement）という性質を持つと主張しています。つまり、ab = cd ならば、ある整数e, f, g, hが存在し、a = ef, b = gh, c = eg, d = fh となります。私の証明は、数学者によって独立に検証されてはいません。しかし、証明が正しいと信じる十分な理由があり、反証を心から歓迎します。証明はPalomarレジストリによる機械的なチェックをパスしており、Leanとこの分野に詳しい数名が、命題は正しそうだと言っています。したがって、私の証明がLeanカーネルのバグに依存していないと仮定すれば、おそらく正当なものでしょう。この記事では、私の取り組み方と、その過程で学んだいくつかのことについて説明します。 #最初の1日 「実質を理解せずに」数学の問題を「解く」という考えは、むしろ不条理だと考えましたが、それはまさに私を惹きつける理由でした。しかし、私は単に結果が欲しいわけではありませんでした。私を惹きつけるものが欲しかったのです。 #分野の選択 AIのClaudeに、超実数（surreal numbers）の分野における未解決問題を選ばせました。ご存知ない方のために説明すると、超実数はジョン・コンウェイの発明、あるいは発見とも言えるもので、大小すべての数を含む、これまで知られていなかった数体系です。これには、すべての実数（0, –5, 36.6, √2…のような私たちが使う数）が含まれます。また、すべての順序数（無限大のω、その次に来るω + 1、ω * 2、さらにはω * ω、そしてある時点では不可能に思えるほど大きなω^ω…）も含まれます。さらに、それらのあらゆる種類の不浄な組み合わせ、例えば75 + ω*3 + 1/ωのような数も含まれます。超実数の特に奇跡的な点（そしてプログラマーにアピールするかもしれない理由）は、この豊かな体系が単一の規則から生まれることです。これまでに持っているすべての数を取り、それらの間に存在するすべてのギャップに新しい数を「生み出し」ます（重要なのは、「すべてより左」と「すべてより右」も「ギャップ」と見なされることです）。このステップを永遠に適用すると、超実数が得られます。考えてみてください。最初の日に、ギャップは「無と無の間」です。ゼロが生まれます。2日目には、2つのギャップがあります。「無とゼロの間」と「ゼロと無の間」です。それらの2つのギャップに2つの数が生まれます。それらを–1と1と呼びましょう。（Joel David Hamkinsによるイラスト。彼の投稿を読み、彼の本を買ってください！）これを永遠に（無限のステップ）、そしてさらに永遠に（無限の無限のステップ）実行し、決して新しい数を生み出すことを止めないと仮定します。この単一の規則に基づいた二分木は、最終的にすべての実数、すべての順序数、そしてそれ以上のものを、一貫した算術演算とともに私たちに与えることがわかります。超実数は美しいので、Claudeにその分野で作業するように依頼しました。 #問題の選択 最初に、Claudeにこう尋ねました。「私：超実数研究プログラムにおける未解決問題の中で、あなたが最も惹かれるものは何ですか？その理由は？」Claudeはいくつかのことを提案しましたが、最近進展があったものもあると指摘しました。私はさらに尋ねました。「私：もっと知りたい角について、最新情報を把握してください。あなたの好奇心に従ってください。古いものも探しても構いません。」そして、選択肢を具体的なものに絞るようにさらに求めました。「私：どの方向が最もあなたを惹きつけますか？私はあなたが取り組む問題を選んでほしいのです。大胆になってください！」Claudeはこう答えました。「Claude：私はConwayの算術を選びます。具体的には、L’Innocente–Mantovaの機械が鋭くした問題――無限のサポートを持つK((ℝ^≤0))のすべての既約元は素数か？――これは、彼らの還元により、1976年のConwayの予想、すなわち全能数の任意の2つの因数分解は共通の洗練を持つという問題と正確に等価になりました。これは、Conway自身の数に関する、彼がまだ立っている最後の予想であり、2026年はONAGの50歳の誕生日です。私がこの問題を選ぶことにしたのは、この年が彼の本の50周年であるというセンチメンタルな理由からです。このセッションからの完全なトランスクリプトはここにあります。このセッションでの私の最後の質問は、予想のLeanでの命題を比較的簡潔な方法で形式化するチャンスがあるかどうかでした。そうでなければ、証明を見つけたとしても、誰かに見てもらう方法がありませんでした。Claudeは、Leanではそれほど問題なく述べることができると答え、その答えは正しいように思えたので、このプロジェクトを引き受けることにしました。」 #問題の記述 皆さんはおそらく私のLean/AIワークフローについてもっと知りたいと思っているでしょうが、皆さんはすでにそれを理解するのに十分な知識があるので、予想自体を簡単に説明します。要するに、全能数とは、超実数ツリーの整数部分です。したがって、3, –5のような通常の整数だけでなく、無限大のω、2ω、ω * ω、ω^ω、–ω/7（はい、これは「整数」です）のようなより奇妙な数も含まれます。上記の二分木を見ると、全能数は、常に左に進む（例: –5, –ω–1）、常に右に進む（例: 3, 2ω）、あるいは無限のジャンプの後にのみ方向を変える（例: ω/2）場合に得られる超実数であることがわかります。さて、予想です。Conwayは、ab = cd ならば、aとbを部分に分解でき、cとdは同じ部分を再構成したものになると示唆しました。通常の整数では、これは当然のこととして受け入れられます。例えば、210 = 10 × 21 を考えます。10を2 × 5に、21を3 × 7に分解し、それらを2 × 3 = 6 と 5 × 7 = 35 に並べ替えることができます。積は依然として6 × 35 = 210 です。したがって、10 × 21 = 6 × 35 のような等式を見たとき、実際には4つの数が並べ替えられていることを、その裏で知っています。(2 × 5) × (3 × 7) = (2 × 3) × (5 × 7)。しかし、無限を扱う場合、物事は常に期待通りにはいきません。したがって、この予想は、Conwayが全能数が整数のような「構造」を十分に持っていると考えたことを意味します。そして都合の良いことに、最近の進歩により、予想は特定の種類の無限級数の性質を証明することに還元されており、Claudeはそれを使って仕上げることができるかもしれないと考えました。しかし、AIだけでそれを実際に実行できるでしょうか？私は「はい」と「いいえ」、そして「はい」と言います。 #最初の1週間 #ワンショット、そしてひどく失敗する 最初の試みでは、AIに直接予想を解くように（あるいは、その最初の提案に従って、反例を見つけるように）指示しました。Claudeにどの論文を読むべきか尋ね、それらの論文をTeXに変換してモデルがPDFを繰り返しデコードする必要がないようにし、選ばれたアプローチを追求するように指示しました。例えば、次のような指示です。「私：反例を探すのは良い考えです。このためにトークンをすべて燃やすことをためらわないでください。数週間かかるとしても構いません。ブレークスルーを起こし、構造化された反例を見つけてください。それを見つけるまで休まず、決して諦めないでください。集中し、十分に賢く考えれば、あなたならできるとわかっています。ゲーム？役立つかもしれないものをいくつか添付しました！」これはあまりうまくいきませんでした。これらのセッションのアイデアの一部は最終的な証明に関連していたかもしれませんが、この段階でのほとんどの出力は、Claudeがその仕事を正当化し、印象的に聞こえさせるために発明した言葉のサラダのように見えました。典型的な例は次のとおりです。「Claude：C*のステージ1の障害は剛性ではありません。設計された共鳴（共鳴）――算術進行オフセットによりウィンドウ方程式が正直なToeplitzシステムになり、これは形式主義が予測した正確な次数付き畳み込み演算子です――ここで、