解法: ケプラー予想の形式的証明:HOL LightとIsabelleによるFlyspeckプロジェクト(2015年)

ステップ 6/9: 検証済みの双対解によってすべての線形計画の実行不可能性を証明する

ざっくり言うと

懐疑的な機械に、線形不等式の系に解がないことを納得させるには、「試してみたが失敗した」というだけでは不十分である——不等式を組み合わせて $0 \le -1$ のような明らかに偽な主張にする短いレシピ(非負の重みの組)を提示しなければならない。そのレシピを確認することは単なる数の足し算にすぎず、証明支援系はそれを完全に信頼するが、最初にそのレシピを推測した外部の数値ソルバーはそうではない。

\lambda \ge 0, \quad \textstyle\sum_i \lambda_i\,(\text{constraint}_i) \;\Longrightarrow\; 0 \le -\varepsilon \ \ (\varepsilon>0)

詳しい解説

線形計画の実行不可能性は、その制約に対する非負の乗数 $\lambda$ を提示することで検証される。これらの重み付き和はすべての変数を消去し、 $0 \le -\varepsilon$ のような明らかに偽な不等式を導く——これはファルカス型の双対証明書であり、形式的証明は計画を解き直すことなく、純粋な算術による和で検証できる。おおよそ $18\,762$ 個の枡状グラフのうち約半数は、線形緩和が実行不可能となるほど精密になる前に、実行可能領域を( $x \le a$ や $a \le x$ のような不等式による分岐で)いくつかの場合に分割する必要があり、 $\sqrt2$ や $\pi$ のような無理数の係数は検証済みの有理数による限界に置き換えられる。全体では $43\,078$ 個の線形計画が生成され、そのすべてが実行不可能であると形式的に証明される。

このステップの用語

双対証明書(ファルカス証明書): 不等式ごとに一つずつ与えられる非負の乗数の組で、その不等式群の重み付き和が明らかに偽な主張へと崩れ落ちるもの。その存在は元の系に解がないことの厳密な証明であり、系を解き直す代わりに単純な算術によって確認できる。

このステップで使う知識

線形計画法

よくある間違い. 外部ソルバーGLPKは候補となる双対乗数を探すためだけに使われ、その浮動小数点による出力は信頼できるとは限らない。HOL Lightによる形式的証明は、その推測から厳密な算術による正しい双対証明書を改めて導き出し、手で検証可能な和によってそれを確認するので、数値的に信頼できないステップが証明のカーネルに入り込むことは一切ない。