解法: ケプラー予想の形式的証明:HOL LightとIsabelleによるFlyspeckプロジェクト(2015年)
ざっくり言うと
ケプラー予想が、人間の査読者だけでなくコンピューターが一行ずつ検証できる証明を得たとき、数学者たちは新しい種類の確信を得た——それは電卓の算術が正しいという確信と同じ種類のものである。Flyspeckは、機械検証された奇数位数定理、機械検証されたCコンパイラ、機械検証されたオペレーティングシステムのカーネルといった、他のわずかな巨大な形式化プロジェクトと肩を並べ、百年来の未解決問題が原理的には論理的な基盤まで完全に検証できることの証拠となっている。
詳しい解説
形式化された主定理は次のように述べる:任意の詰め込み に対して、ある定数 が存在し、任意の半径 について、半径 の容器内にある球の中心の数は を満たす。 とすることで、古典的な形のケプラーの密度限界が得られる。証明スクリプトは再生可能な形式で保存されているため、普通のコンピューターを持つ読者は誰でも、主定理のHOL Lightによる検証全体をおよそ四十分で再実行でき、これは背後にある何千ページもの場合分けではなく、証明支援系の公開された小さなカーネルだけを信頼すればよい独立した検証である。
Flyspeckの規模——著者たちによってFeit–Thompsonの奇数位数定理、検証済みCコンパイラCompCert、検証済みマイクロカーネルseL4に匹敵すると評されている——は、完全な形式的検証が、ソフトウェアの一部だけでなく、最も難しい古典的な未解決問題に対しても現実的な選択肢であることを確立する助けとなった。またそれは、後の形式化プロジェクトが基礎とする、実解析・複素解析のための再利用可能なHOL Lightライブラリを後に残した。