はじめに

定理証明支援系のLeanに最近興味津々だが、原理がよくわからない。なんでプログラム組んだだけで証明したことになるのだろうか？
例として挙げられる
$$1+1 = 2$$を定理証明系で証明します、というのが妥当なのは「なんとなく」はわかる。ただ、数学の証明だと標榜しているのだからなんとなくわかるからといって、これが証明でござい。とされてもまともな数学者は受け入れないだろう。
なにかしらプログラムを組んで実行orコンパイルすることと、証明することとの間に、その行われる数学の証明と同等以上の厳密な関係が存在するはずである。それはなんだろうか？

書いてみたら適当なブレインストーミングになってしまいました。オチ無しです。

ケプラー予想の計算機による証明の仕方について

この謎を解き明かすには、計算機による数学の証明が数学者に受け入れられた例を探すのが順当だと思われる。計算機による数学の定理の証明というと四色定理の証明が有名だが、アッペルとハーケンの証明は定理証明支援系は使っていないのでこの場合あまり参考にはならない。
数学者にも受け入れられている計算機による数学の定理の証明というと、おそらく一番有名なのはケプラー予想の証明ではないだろうか？（少なくともこういう記事→溝口佳寛・田上真著「ケプラー予想の計算機による証明と検証について」が数学セミナーという雑誌に掲載される程度には受け入れられていると言える。本当に完全に受け入れられているか、と言われると、それは知りません。）

ケプラー予想と言うのは、3次元ユークリッド空間における球充填問題に関する予想で、「面心立法配置を含む六方最密充填配置のアレンジだけが最密充填を与えるという予想」である。接吻数問題ともいうらしい。
問題は非常にシンプルだが、厳密に証明せよと言われると非常に難しい問題ということである（詳しくは上のリンク先の記事を参照）。

トーマス・ヘールズは、1992年に予想に対する証明の道筋を計算機プログラムを用いて考え、1998年に、その証明を完成させた。その論文の総ページ数は250ページを超え、計算結果は３ギガバイトを超える。計算機のプログラムが相当部分を占めるこの論文の査読は難航し、4年以上続けられた。そして、2002年に査読者たちは99％正しいことは確認できたが、完全な確信は得られなかったということで査読を諦めてしまった。このことを受けて2003年1月に徹底的に精査するという意味を持つFlyspeckプロジェクトが立ち上げられ、計算機による証明を計算機により検証するという試みが開始された。さらに、それから10年以上の時を経て、2014年8月10日付で、ケプラー予想の計算機による証明の検証が完成したとウェブサイトに公表された[3]。

ということである¹²。

Flyspeckプロジェクトの目的は、ケプラー予想の形式証明を構築することです。
The purpose of the flyspeck project was to produce a formal proof of the Kepler Conjecture.

形式証明を構築するということはなんとなくわかる。でも、形式証明を作ってそれを数学者の頭の中で動かして妥当とならないと数学の証明にはならないのではないだろうか。なんで、数学者の頭の中ではなくて、計算機で動かして問題なかったら数学の証明が正しいということになるのだろうか。少なくとも、まず計算機上で、現代数学の共通基盤といわれるＺＦＣ（ツェルメロ＝フレンケル集合論）を構築するとかしないといけないのではないだろうか。でも、寡聞にも聞いたことがない。

Flyspeckプロジェクトの基盤

Flyspeckプロジェクトはどういう基盤の元、数学者に認められた（？）のか？

使用した定理証明支援系：古典的 高階述語論理（Higher Order Logic） に対する証明支援系のHOL Light
・Coq[Rocq]で使われているCICでもなく、Agdaなどで使われているマルティン＝レーフの型理論でもない、高階述語論理（Higher Order Logic）を用いている³。

なんで 高階述語論理上でケプラー予想を証明＝＝現代数学の意味で正しい となるのだろうか？
と思っていてヘイルズの論文を調べてみるとこういう仕組みらしい。

1.1. 素朴な型理論（Naive type theory）
本節で説明する数学の基礎システムであるHOLは、単純型付きλ計算に基づいている。...コンピュータ・システムは、型によって提供される追加の構造から恩恵を受ける。素朴に言えば、単純な型システムとは、型と呼ばれる、互いに素な空でない集合の可算な集まりである。型の集まりは閉包性を満たす。すなわち、任意の2つの型 $A$ と $B$ に対して、さらなる型 $A \to B$ が存在し、これは $A$ から $B$ への関数の集合と同一視できる。型に加えて、項（term）が存在し、これは型の要素と考えられる。各項 $t$ は一意な型 $A$ を持つ。項とその型の間のこの関係は $t : A$ と表記される。特に、$f : A \to B$ は型 $A \to B$ の項 $f$ を表す。型変数をわたる「型変数」と呼ばれる変数と、項をわたる別の変数の集まりが存在する。
1.2. HOLのモデル（Models of HOL）
型を集合とする素朴な解釈は、厳密にすることができる。我々は、ZFC（ツェルメロ＝フレンケル＝選択公理）集合論の中にHOLのモデルを構築し、ZFCが矛盾していないと仮定すればHOLも矛盾していないことを証明する。...HOLにおける定理とは、数学的公理と論理規則から生成されるシーケントのことである。HOLには定数 FALSE が存在する。以下は、HOLが FALSE を証明しないことを述べるのに等しい。

定理 1. ZFCが矛盾していなければ、HOLは矛盾していない。

T.C.Hales,Developments in Formal Proofsより

てっきりHOL Light上にＺＦＣを構築してその上で、ケプラー予想を証明するのかと思ったら、そうではなく、ＺＦＣの中にHOLを作ってその中で証明するという戦略をとるようである。詳しいことはわからないが、それならなんとなく腑は落ちる。

でも、これってこのケプラー予想の証明の場合だけではないか？Leanとかは別原理で証明しているのでは？

さらなる疑問

ケプラー予想のようにＺＦＣの中に定理証明支援系の論理体系をＤＳＬ（ドメイン固有言語）のように構築して、数学的基盤の担保を取るのであれば、別にCICもCoCもマルティン＝レーフの型理論もいらないのではないか？なんでこぞって定理証明支援系は基盤に型理論を採用したがるのか理由がわからなくなった。
ＺＦＣの中に定理証明支援系の論理体系を構築するのであれば、圏論を導入する理由もわからない。単純に、集合論 ⊃ 圏論という図式が成立してしまうのではないか。
ＺＦＣの中に定理証明支援系の論理体系を構築する以外に、数学的基盤を担保する方法があるとすれば、どういう方法をとるのだろうか？

ちょっと調べただけなので、疑問ばかりになってしまった。個人的には読んだ限りケプラー予想の証明でカリー＝ハワード同型対応が全然出てこなかったのが一番謎だった。なんで定理証明支援で型理論いるんだろうか？なしでもできるんなら使う必要ないんじゃないだろうか。

追記[2026/1/10]

定理証明支援系一般についてある程度調べてまとめました。

ちなみに、「ケプラー予想の計算機による証明の検証が完成したとウェブサイトに公表された。」とは書いてあるが、査読されたとか、この結果は広く数学者に受け入れられた、とは書いてない。これどういうプロセスで認められるんだろう？ ↩
フィールズ賞受賞者のテレンス・タオ氏がLean4を使って自分の証明のバグを見つけた。というような話を見かけたが、もしかしたら本当にテレンス・タオ氏とかは、自分の証明構築にあたってのツールとして使っているだけなのではないだろうか？Lean4の形式証明を提出してこれが証明でござい、とするつもりは当面ないのではないだろうか。自分の書いた字面を読んだらそのままだし、よく考えると当たり前な気がするが、そういう定理証明支援系で動かせる形式証明を提出して証明完了と認められるまでは大分時間がかかるんじゃないだろうか。 ↩
素朴な疑問として、そもそも型理論使わなくて証明できるのであれば、Leanなどはなんで型理論使う必要あるのだろうか？ ↩