「リーンを使えばいいのでは？」

2026年4月27日原文(lawrencecpaulson.github.io)

概要

数学の形式化は Lean 以前から続く長い歴史
AUTOMATH やLCFなど初期のシステムの重要性
Leanの成功と 依存型理論 への批判
Isabelle など他システムの利点と選択理由
AIや今後の形式化数学の展望

数学形式化の歴史とLeanの位置づけ

数学形式化 は約60年前の AUTOMATH から始まった歴史
AUTOMATHは1968年にNG de Bruijnが開発、1977年にはJuttingがLandauの解析基礎を形式化
Juttingは 実数のDedekind完全性 を証明、当時としては画期的な成果
- 証明は長大かつ読みにくく、記法や自動化の欠如が課題
BoyerとMooreは1973年に LISP関数の定理証明 からスタートし、ACL2へ発展
- 主にハードウェア検証で活用、多様な定理の形式化も実現

LCF、Coq、HOL、Isabelleの登場

Edinburgh LCF はプログラミング言語理論に特化しつつ、MLをメタ言語とするアイデアで広範囲に影響
HOL や Coq（現Rocq）、NuprlなどがMLを基盤に開発
John Harrisonは HOL Light で実数や素数定理など高度な数学を形式化
- Tom HalesによるKepler予想証明など、多くの難解な定理も形式化
Isabelle は他システムの成果も積極的に取り入れ発展

Leanの台頭とその背景

数学者は長らく形式化証明に懐疑的だったが、Tom Halesが 定義の大規模ライブラリ構築 をLeanで提案
Kevin Buzzardが教育でLeanを導入し、ユーザーコミュニティが急拡大
Leanは constructive proof への過剰なこだわりを捨て、より広範な数学へ対応
依存型理論や「 propositions as types」の美しさと限界を認識する必要

LCFアプローチと証明オブジェクト不要論

LCFでは 証明オブジェクト は不要、MLの抽象データ型で証明を動的に検証
LeanやRocqでは「証明オブジェクト」が保持されるが、実際には冗長
メモリ消費や計算負荷の観点からも、巨大な証明項は非効率

Isabelleを選ぶ理由

自動化性能（Sledgehammer） が他システムを圧倒
可読性の高さ、依存型を避ける設計で初心者にも扱いやすい
依存型の型検査は本質的に難解で計算コストも高い
- LeanやRocqでも依存型は制限される傾向
数学の様々な分野にも型にこだわらず対応可能

AI時代と今後の展望

AI生成証明は Sledgehammer などで容易に整理・簡略化可能
AIが異なる証明支援系間で証明文を翻訳することも容易に
最終的な透明性は「 人が読める証明文」であり、証明オブジェクトではない

Mizarの重要性

Mizar とその膨大な数学ライブラリの歴史的意義
Isabelleの Isar言語 はMizarから多くを借用
Mizarについては今後改めて詳述予定

まとめ

数学形式化はLean以前から多様なアプローチと歴史を持つ
Leanは多くの長所を持つが、他のシステムや思想も重要
システム選択は目的やコミュニティ、可読性、自動化性能など多角的に判断が必要
AI時代には「どの証明支援系を使うか」の壁は低くなりつつある

Hackerたちの意見

こういうのもっと必要だよね。「まあ、もちろん、ただ...X、みんなそうするから」という集団思考の議論がある一方で、少なくとも代替案を考慮することの重要性を示すしっかりした理由がある。最終的に代替案を却下してみんなと同じ道を選ぶとしても、全体の状況を知っておく方が絶対に良いよ。

└

それは状況次第だね！定番の道から外れるたびに、ドキュメントが少なくなって、バグが増えて（暗い隅っこを探る人が少ないから）、助けを求められる人も減っちゃう。選択肢が20個以上あるなら、標準的なオプションを選ぶのが平均的には正解だから、それを選んでさっさと次に進んじゃえばいいよ。注意力には限りがあるから、すべての依存関係についてリサーチレポートを書くのは、結局コアの問題に取り組めてないってことになる。例外としては、a) 標準ツールが実際には自分のユースケースに合わないと分かったとき、または b) 標準ツールが解決しようとしているコアの問題と大きく重なっているときだね。

HNの人たちは一般的にプログラマーだけど、必ずしも数学者じゃないから、プログラミングの視点から考える方が関連性が高いよね。残念ながらまだ読み終えてないけど、機能的プログラミングの視点からLeanを扱ったすごく良い本があるよ： https://leanprover.github.io/functional_programming_in_lean/ 自分もLeanを学んでるから、初心者としてちょっと楽観的に見てるかもしれないけど、今の目標は普通のプログラマーが書くようなコード、例えば最近のlean-zipの例みたいな現実の圧縮/解凍アルゴリズムを書くことだよ： https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...

└

1990年代にソフトウェアの正しさを証明する実験があって、最終的な証明注釈に見つかったエラーの方が、正しいと証明されたソフトウェアより多かったっていうのを思い出す。それから、他に2つの障害が見えるんだけど、1つは消えるかもしれない：1. ソフトウェアが何をするべきかを実際に知るのが難しい。ユーザーが実際に何をしたいのか、顧客が何にお金を払っているのか（必ずしも同じではない）を理解するのは複雑なんだ。2. 多くのソフトウェア開発者の仕事の質がひどくて、彼らがJavaや他の言語よりも真実の言語でうまくやれる理由がわからない。反対意見2は、必要なことをやる注意力を持ったAIシステムに置き換わるかもしれないから、もしかしたら状況が変わって価値が出てくるかもね…。

└

この本を読みながら、Leanで基本的なコンピュータ代数簡略化ツールをいじってみたよ。リンクはここね: https://github.com/dharmatech/symbolism.lean C#からのコードを移植したものなんだけど、Leanは驚くほど表現力があるね。

└

非機能型プログラミングはどうなの？FPは、ほとんどのプログラマーにとっては、君がすでに脇に置いた数学と同じくらい関係ないよ。

Leanの面白いところは、Lean自体が言語で、ほとんどの人が話しているのはMathlibというライブラリだってことだと思う。Mathlibについて読んだ限りでは、作成者たちはとても実用的で、だからこそ古典論理をLeanの型にエンコードしているんだよね。直観主義的論理はちょっとだけ。数学用語に不慣れな人のために言うと、古典論理には強力な特徴がたくさんあるんだ。その一つが排中律で、何かが同時に真でも偽でもあり得ないっていうもの。つまり、「真でないことは真である」というのが成り立つけど、直観主義的論理では言えないんだ。もう一つの特徴は背理法で、代替案が無効であることを示すことで何かを証明できるんだ。これらの技術に依存する結果がたくさんあるから、すべてを直観主義的論理でやろうとすると多くの障害にぶつかるんだよね。

└

これが形式的な数学には良いけど、哲学には悪い理由だね。なぜなら、投機的な動きをエンコードできないから。

└

制限や障害がある中で、いつ/なぜ直観的論理を使うことを好むんだろう？

└

「直観的論理」じゃなくて「直観主義的論理」のことだよ。

└

もう一つの特徴は背理法で、代替案が無効であることを示すことで何かを証明できるんだ。Leanに関して言えば、これは古典論理の例ではないよ。「not」の定義に過ぎないから、ある命題が矛盾を引き起こすなら、その命題が真でないと言うのは同じことなんだ。こういう風に証明したい「何か」は、古典論理からのステップが必要なことが多いけど、すべてではないよ。（¬p ⟶ F）⟶ pは古典的；（p ⟶ F）⟶ ¬pは構成的。

└

その一つが排中律で、何かが同時に真でも偽でもありえないっていうものだ。それが矛盾律（LNC）だね。排中律（LEM）は、すべての命題についてそれが真かその否定が真かのどちらかだと言っている。LEM: すべてのpについて、pまたはnot p。LNC: すべてのpについて、not (p and not p)。古典論理は両方を満たすけど、直観主義的論理はLNCだけを満たす。

Hacker Newsで議論の続きを見る

ハクソク