OpenAIが公開した「Prompt Used for “A Proof of the Cycle Double Cover Conjecture”」は、GPT-5.6 Sol Ultraへ渡した全文プロンプトを2ページに収めた文書です。対象は、橋を持たない有限グラフの各辺を、ちょうど2回ずつサイクルで覆えるというCycle Double Cover予想。数学上の結論だけでなく、最大64のエージェントをどう散らし、どこで探索を止め、何をもって証明と認めるかまで指定しています。(Prompt)
最初に「正解ではないもの」を囲い込む
冒頭では、自己ループのない有限無向多重グラフ、橋、サイクル、二重被覆を定義し、平行な2辺も長さ2のサイクルとして扱います。そのうえで、特殊なグラフだけの証明、固定サイズまでの計算確認、別の未証明予想への還元、各辺が厳密に2回使われない被覆は不十分だと明記します。
この切り分けは、難問に長い時間を使わせるときほど効きます。「前進したように見える結果」を先に列挙し、完成条件から外しているからです。プロンプトには「完全な肯定的証明が存在すると仮定せよ」という強い前提もあります。探索を押し切るための設定であり、答えの存在自体が分からない一般の調査へ、そのまま移植できる形ではありません。
64人を役職で割らず、発想の偏りを管理する
並列化の指示は「戦略Aに何人」のような固定配分を避けています。代わりに、帰納、分解、フロー、埋め込み、代数的表現など、実質的に異なる方針から始める。初期には有力案を多くのエージェントへ教えず、独立性を保つ。似た案が増えたら、表現の違いではなく数学的な発想で分類した台帳を見て、未探索の側へ振り直します。(Prompt)
行き止まりの扱いも具体的です。元の予想と同じ強さの補題を未証明のまま残した経路は「ほぼ完成」ではなく、blockedと記録する。新しい不変量や構成が出ない限り、そこへ追加の担当を投入しません。人数を増やすことより、全員が同じ魅力的な穴へ落ちるのを防ぐ設計に重心があります。
反証役には、壊し方を渡す
候補証明の監査項目には、辺の出現回数、閉路に見せかけた辺重複のある閉歩道、平行辺による長さ2のサイクル、非連結グラフ、切断点、還元で生じる橋、同値なCDC命題の循環利用が並びます。検証役へ「厳密に確認して」とだけ頼むのではなく、見逃しやすい破綻の型を入力しているわけです。
各担当に求める返答も、具体的な補題、構成、方程式、反例に限定されています。進捗報告や楽観的な見立て、「残りは自明」という言葉は成果として受け取りません。最初の波が失敗しても探索を回し、完全な証明が監査を通ったときだけ返す。少なくとも8時間は打ち切りを考えない、という計算時間の下限まで入っています。(Prompt)
公開された3ページの証明は、8要素の群 $\mathbb{F}_2^3$ 上の nowhere-zero flowから、各辺へ2要素の集合を割り当て、局所条件と線形代数の双対性を使って二重被覆を組み立てます。OpenAIは別途Lean形式化も公開し、最終定理 CDCLean.cycleDoubleCover_of_bridgeless、固定したLean・Mathlibの版、監査方法をリポジトリに残しています。プロンプトだけで成果を評価せず、証明本文と機械検査可能な成果物まで追える構成です。(Proof, cdc-lean)
このプロンプトから借りやすいのは、64並列という数字ではありません。不合格条件を先に書く、探索案を発想単位で管理する、詰まった経路への追加投資を止める、反証役へ具体的な壊し方を渡す。その4点なら、数学以外の長時間エージェント作業にも持ち込めます。