「なぜわざわざレアンを採用しないのか？」

2026 年 4 月 23 日

[AUTOMATH、LCF、HOL システム、HOL Light、Lean、形式化された数学]

最近、数学を形式化する提案を行う際には、「なぜ Lean を使わないのか」の説明が必要だと伺いました。これは私がいささか前に離脱した依存型世界から 40 年を経て感じたこととの重なりであり、その理由は cultish な気風、閉鎖性、そして画一化にあります。

Lean は優れた言語であり、使い勝手のよいツール、豊富なライブラリ、そして最近驚くべき成果を挙げている熱心で大規模なユーザーコミュニティを擁しています。しかし、数学の形式化にはおよそ 60 年の歴史があります。現在の進歩に対する過剰な hype の中においても、私たちはどのようにこの道に辿り着いたかを忘れてはなりません。それは群衆に従った結果ではなく、先駆者たちの尽力によるものです。

その始まりは AUTOMATH にありました。前述の hype の一部として頻繁に「Lean が数学の形式化を可能にした」という主張が行われていますが、お詫び申し上げますが、私たちがそれを実現したのは 1968 年のことです。N. G. デ・ブリュインによる AUTOMATH は、既にそのための主要な要素を備えていました。1977 年までには、jutting が AUTOMATH を用いてランドゥーの『解析学の基礎』を形式化することに成功しており、これは純粋な論理から複素数の構築までの内容を扱っていました。Jutting は同値類と有理数集合を用い、実数直線のデデキント完全性を形式的に証明しました。彼の業績はその後 20 年間にわたり、計算能力が劇的に進歩したにもかかわらず、繰り返しませんでした。最終的に実数の形式化は 1990 年代半ばに、HOL Light を用いたジョン・ハリソン氏と、Isabelle/HOL を用いたジャック・フルリオール氏によって行われました。

私は、現在どのシステムにおいてても形式化されているほぼあらゆることは、AUTOMATH でも形式化出来たと考えます。その主な欠点は記法（実におどろおどろしいものでした）と自動化の完全な欠如でした。証明は長く不読になりました。それでもなお、同値類に関する議論においては、おそらく現在も Rocq よりも優れているでしょう。後者の利用者が「setoid 地獄」への批判を繰り返す一方で、Jutting は博士論文で同値類の形式化について感情なく記述しており、さらにはランドゥーの一章を二度にわたって形式化し、同値類を採用した理由としてそれが正しいアプローチであると確信していたからです。

その直後、ボーアとムーアによる仕事が登場しました。これは全く異なる方向からの試みであり、ロバート・ボーア、J. ムーアら多くの協力者たちによって行われました。1973 年に『LISP 関数に関する定理の証明』というタイトルで発表された彼らの研究は、当初はコードの検証を目的としていました。彼らの「計算論的論理」は一般数学に対して明確な限界を持っていましたが、ゴデルの不完全性定理から平方互恵法則、そしてバナッハ・タルスキ定理に至るまで、多様な深い結果の形式化に用いられることはありませんでした。現在の形態は ACL2 と呼ばれ、主にハードウェアの検証に応用されています。異なるアプローチこそが遠くへ進む鍵となります。

さらにその後、LCF、Coq、HOL、そして Isabele の時代が到来しました。画期的だったエディンバラ発の LCF はプログラミング言語理論に限定されていましたが、その証明支援子の méta 言語（ML）として関数型言語を採用するというアイデアは広範な影響を与えました。ケンブリッジ、INRIA、コーネル大学、さらに他の地域のグループも ML を用いたツールの開発に取り組み、初期の HOL、Coq（現在の Rocq）、および Nuprl などを含むシステムを構築しました。HOL グループはハードウェア検証に固執していましたが、浮動小数点ハードウェアの検証が必要となったことで実解析への要求が生じました。やがてジョン・ハリソン氏はオイラーの積分公式を用いた素数定理など、意義深い数学結果の証明に取り組み、さらに著名な 100 の定理をできるだけ多く検証する任務を設定しました。その結果、HOL Light は頻繁に首位を争うことになります。Isabelle が場合によっては HOL Light を上回っているのは、私が彼らの形式化を多数盗用しているためです。

2014 年までには、これらのシステムを用いて一連の高水準な結果が形式化されていました。以下は比較的自由なリストです： - 4 色定理 - 奇順位数理系定理（odd order theorem） - 選択公理の相対的整合性 - ゴデルの第二不完全性定理 - トム・ヘールズによるケプラー予想の証明

これらの定理はほとんどが長く複雑な証明を持っていました。それらの形式化は多大な労力を要し、定理に関する残存的な疑念を解消する上で極めて重要な役割を果たしました。にもかかわらず、数学者たちはあまり感銘を受けませんでした。例外として著名なのは集合論者のダナ・スコット氏とケン・クヌーン氏です。

Lean 自体の開発については詳しくありませんが、そのことが数学界にどのように広まったかについては少し知っています。数学者たちは懐疑的に注目を集めており、上記の証明には mainstream な数学で一般的であるような洗練された構成（グルテンディエックスキームやペルフェクトイド空間など）が含まれていないことに気づいていました。トム・ヘールズは、そのような定義だけのライブラリを構築するアイデアを抱き、その目的のために Lean を選択しました。彼はニュートン・インスティティートの『Big Proof』プログラムにおいて、多くの類似のアイデアが議論されました。ケビン・バザード氏はこの話を聞き、Lean を教育に試してみることになりました。それ以降はご存知の通りです。

Lean コミュニティの重要な一環として、Rocq 全体を通じて支配的であった「構成論的証明（constructive proof）」への奇妙な執着を手放しました。以前に議論したように、直観主義哲学はラッセルのパラドックスの後を継ぐ形で生じました。それは実数に対して特に重要な意味を持っていました。マルティン＝ローフ型論理が明らかに直観主義的形式化であることは確かですが、Rocq についてはそう明確ではありません。それでもなお、論文から論文まで「構成論的証明」という言葉が使われており、それが非関連な場合や無意味な場合さえあります。この執着は Rocq の数学への適用を妨げ、その分野を Lean に明け渡しました。

すべてが「命題として型（propositions as types）」であるわけではありません。「命題として型」は論理記号 $\forall, \exists, \to, \wedge, \vee$ と型構築子 $\Pi, \Sigma, \to, \times, +$ とを結びつける対偶関係であり、それは美しくて魅力的で理論的にも豊かです。しかし、これが唯一の選択肢ではありません。私は「証明支援子」という用語が、命題として型の原理に従って証明を検証するソフトウェアであると定義されているのを見てきました。もしそうだとすれば、過去半世紀の研究の大部分が無効化されてしまいます。残されるのは Rocq、Lean、そしてマルティン＝ローフ型論理を実装する Agda（AUTOMATH も同様の原理の下にはありません）だけです。AUTOMATH でも $\Pi$ と $\to$ のバージョンは存在しますが、論理は通常の論理学のテキストに見られるような公理を用いて設定されます。デ・ブリュインは 50 年前より早くから、型と命題のカテゴリーを区別する必要性があることを理解しており、いくつかの理由からこれが重要だと指摘していました。最も明らかな理由は、除算演算子が三つの引数を取る必要があり、かつ $x/y$ の値は実際には $y \neq 0$ であるという証明に依存してしまうことです。彼は、証明の非重要性（irrelevance）が必要不可欠であると指摘しました。

また、有識な人々さえ「LCF アプローチとは命題として型と同じものだ」と言うのを耳にすることがあります。これは全くの誤りで、この無知を正そうとするブログ記事が存在しています。

LCF（再び）：私たちは証明オブジェクトが必要ありません！Rocq および Lean の両方では Prop ソートが用意されており、これにより証明の非重要性が保証されます。したがって、与えられた命題に対するすべての証明オブジェクトは同じ値に評価されます。つまりこれらの巨大な項は不要ですが、どうやら保持されているようです。なぜでしょうか？それはロビン・ミルナー氏による LCF における重要な発見です。抽象データ型を提供するプログラミング言語（ML!）があれば十分です。証明コアを抽象データ型の中に置き、推論規則をコンスストラクタに設定すればバング！ proofs は動的にチェックされます。ML の抽象化バリアのおかげで不正は不可能です。

かつて私は、この 50 年前のアイデアを「命題として型の世界」の人々に説明しようと試みたことがあり、その経験は surreal でした。対象となったのは学生ではなく、関数型言語の起源についての知識が当然であるべき世界的な第一人者でした。説明にかなりの時間がかかりましたが、彼も完全に納得したようには見えませんでした。前述の閉鎖性の一つの例です。

RAM 災害（RAMmageddon）の時代において、何の意味もない巨大大きな項のために十数メガバイトを浪費するのはばかげています。むしろ、これらの無用なものをエレガントに表現する研究さえ行われています。

なぜ Isabelle を使うべきでしょうか？まず明らかなところから始めましょう：もしあなたが同僚が Lean を使っている場合、あるいは重要な前提条件が Lean のライブラリにある場合は、当然ながら Lean を使用するべきです。しかし、自由を選べる状況であれば、このブログの目的の一つはあなたが Isabelle を検討する理由を与えたいというものです。これには以下の点が含まれます： - 最強の自動化機能。毎日のように「ハンマー」という言葉が使われることに惑わされないでください：sledgehammer に匹敵するものはありません。それ以外にも多くの機能が備わっています。また、ここではコンピュータ代数についても触れる必要があります。 - 読みやすさにおける最善の選択。このブログでは多数の例を提示しています。 - 依存型がないため、宇宙のレベルや初心者を陥らせるような奇抜な性質はありません。Lean の mathlib や Rocq の SSReflect および Mathematical Components では依存型の使用は推奨されていません。

依存型を用いる際の重要な困難の一つは、適切に実行される場合、型チェックが決定不可能になることです。これは等式が決定的に判断できず、初期段階ではこの事実が当然であると考えられていたためです。しかし 1990 年頃にはこの見解も変わりました。型チェックを決定可能にするために、等式は定義的等式または意図的な等式へと準下げされました。そのため $T(N+1)$ と $T(1+N)$ は異なるタイプとなります。この制限は証明に現実の影響を与えますが、定義的等式のテストを行うこと（今もまだ！）は重い計算負荷を伴います。

公平にいえば、2017 年の私に Isabelle がどのような数学を処理できるかを尋ねた場合、私はもっと慎重だったでしょう。依存型が必要なのは以下のようなことを扱うためだと考えられがちです： - 体の拡大 - p 進数 - グルテンディエックスキーム

しかし私たちの中にも多くの人が調査を行い、多くを学びました。その解決策は、すべてを型として強制することをやめることです。

将来において、Lean は多くの点で正しく進歩します。そして Lean は読みやすさを備え、埋め込まれた証明ブロックをサポートする潜在的な力を持っています。今、ユーザーコミュニティはこれら機能を最大限に活用すべきであり、Isabelle のユーザーは既にそれを行っているからです。究極的な透明性とは、コンピューターがチェックできる証明オブジェクトではなく、実際に人間が読むことができる証明テキストにあるのです。

AI の台頭はこれらの違いをより明確にしています。AI による証明はおおむね複雑で不器用ですが、sledgehammer を使うことで整然と整理できます。それらは適切に構造化されており（私の限られた経験に基づくものですが Claude を使用して）、過度な詳細性にも関わらず読みやすいものです。何が起きているかを見極めることができ、簡素化の道を探ることができます。また、最近の研究では言語モデル自体が sledgehammer を呼び出すことも可能になりました。最後に、AI は容易に読みやすい構造化された証明を一つの証明支援子から別の支援子へ翻訳できます。すると、どちらを選ぶべきかを心配する必要がなくなります。

[Mizar について：お詫び [2026 年 4 月 15 日追加]
たまたま Mizar についての記載を忘れてしまいました。数学の形式化の歴史には Mizar とその膨大な数学ライブラリに関する議論が不可欠です。この欠落をさらにひどくしたのは、Isabelle の Isar 言語が Mizar から大きく影響を受けていることです。次のブログ投稿では Mizar について記述する予定です！約束します！]