ケプラー予想と Flyspeck ── 査読者が確かめきれなかった証明を機械が検証する

Flyspeck は、ケプラー予想の証明を、定理証明支援系と呼ばれるソフトウェアの中で一歩ずつ機械検証した国際共同計画である。2014年8月10日に完成した。きっかけは、Thomas Hales と Samuel Ferguson が1998年に発表した証明を、Annals of Mathematics の12人の査読団が何年かけても確かめきれなかったことだった。査読者が「ほぼ確か」としか言えなかった証明に、機械が最終的な保証を与えた ── それがこの出来事の意味である。

四色定理（1976年）が「計算機を使った証明を信じてよいか」という問いを生んだとすれば、Flyspeck はその問いに「計算機にもう一度、論理の規則で検査させる」という答えを、大規模な証明で実際に示した例である。

1611年の予想と1998年の証明

Flyspeck 論文によれば、Kepler は1611年の小冊子『六角形の雪について』で、合同な球を3次元空間に詰めるとき、面心立方の詰め方より密度の高い詰め方はないと述べた。論文はこれを離散幾何学で最も古い問題と呼び、Hilbert の第18問題の一部にもなったと書いている。1950年代には László Fejes Tóth が首尾一貫した証明の方針を示し、計算機が使えるかもしれないと示唆した。

Hales の回顧によれば、Hales と Ferguson は1998年8月に解決を発表し、証明を一連のプレプリントとして arXiv に載せた。証明は、膨大な場合分けと、線形計画や非線形不等式などの計算機計算を組み合わせたものだった。

12人の査読団と「99%」

Annals of Mathematics は、Hales の回顧によれば12人の査読団をこの証明に充てた。George Szpiro の著書によると、査読を率いたのはブダペストのレーニ研究所の Gábor Fejes Tóth で、2002年7月、査読者たちは証明が正しいことに99%確信していると報告した。誤りは見つからなかったが、計算機の部分まですべてを確かめることはできなかった。

Flyspeck 論文は、出版の遅れは査読者が複雑な計算機証明の検証に苦しんだためで、最終的に証明は査読者の完全な認証なしに出版されたと書いている。論文が引く Lagarias の言葉によれば、この証明の性質上、人間がすべての段階を確実に確かめるのは難しかった。Hales 自身は2022年の回顧で、査読は何年も長引き、査読者が疲れ果てて手を引くまで続いたと振り返っている。Annals は計算機を使う証明について、計算部分は1行ずつは検査しないこともあるという方針を出した。

Flyspeck ── 証明を機械に読ませる

Hales は2003年1月、ボルチモアの合同数学会議で、証明を形式化する計画を発表した。名前は「Formal Proof of Kepler」の頭字語 FPK を英単語に膨らませたもので、experimentalmath.info のブログによれば、Hales は完成に20年かかると見積もっていた。

形式化とは、証明のすべての段階を、論理の基本規則だけから組み立て直し、定理証明支援系（proof assistant）に検査させることである。Flyspeck は2つのシステムを使った。HOL Light は、論理の中核（カーネル）が数百行しかなく、すべての推論が最終的にそこを通るよう設計されている。Isabelle は、平面グラフの分類という巨大な計算部分の検証に使われた。

規模は大きかった。論文によると、証明に必要な数百の非線形不等式は領域を分割して2万3,000個超になり、その HOL Light での検証には Microsoft Azure 上で約5,000プロセッサ時間を要した。32コアで並列に回したため実時間は1週間未満で、検証は2014年7〜8月に行われた。同年10月には Radboud 大学で約9,370プロセッサ時間をかけて再検証し、同じ結果を得た。主定理の部分は、記録形式なら2GHz の CPU で約40分で検算できるとされ、論文は読者自身に検算を勧めている。

査読者の役割はどう変わったか

Flyspeck 論文は、証明支援系は数学の査読者を検証の過程から大きく外す、と書く一方で、人間の監督が不要になるわけではないと続けている。必要なのは、正しい定理が形式化されたか、承認されていない公理が加えられていないか、といった監査であり、その大部分は専門の数学者でなくても証明支援系に慣れた人なら行える、という。論文は監査に関する別の論文を引いて、監査人は悪意を前提にすべきだとも書いている。

この転換で恩恵を受けたのは、まず査読の負担を背負っていた数学者たちである。Flyspeck の論文は22人の共著で、ベトナムをはじめ各国の研究者や博士課程の学生が加わった。支援には NSF のほか Microsoft Azure Research、ベトナムの数学研究所などが名を連ねる。 ケプラー予想の形式証明は、その後の AlphaProof（2024年）のように、AI が証明支援系 Lean の中で証明を探す研究の前提にもなった。機械による検証で「確かさ」を担保するという考え方は、エルデシュ問題と AI（2026年）の時代にも引き継がれている。流れは AI と数学の年表 で追える。