ハクソク

世界を動かす技術を、日本語で。

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

7時間前原文(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だけを満たす。
└
> Leanの面白いところは、Leanが言語で、ほとんどの人が話しているのはMathlibというライブラリだってこと。Mathlibについて読んだ限りでは、クリエイターたちは非常に実用的で、だからこそ古典論理をLeanの型にエンコードしていて、直観主義的論理はちょっとだけ使っているんだ。コンピュータサイエンスの人たちは今、自分たちのCSLibに取り組んでいるよ。https://www.cslib.io https://www.github.com/leanprover/cslib 直観主義的論理は実際には計算内容にしか関係ないから（数学的な議論を計算可能な構造に変えるのが目的だから）、彼らがこの問題にどう対処するかを見るのが楽しみだね。Leanでアルゴリズムを書くと、すでに何らかの構造に制限されているから、その目的にはそれが必要な論理かもしれない。
└
>排中律、つまり何かが同時に真でも偽でもあり得ないってやつだね。これは排中律じゃなくて、「矛盾律」だよ。排中律ってのは、pが真か、pの否定が真のどちらかってこと。 https://en.wikipedia.org/wiki/Law_of_noncontradiction
└
構成的数学を受け入れる五段階: 否認、怒り、交渉、抑うつ、受容。アンドレイ・バウアーによる構成的数学の講演が、先端研究所で行われたよ。 https://www.youtube.com/watch?v=21qPOReu4FI http://dx.doi.org/10.1090/bull/1556
Isabelle/HOLは言語としてはいいけど、ツールには深刻な欠陥があって、純粋なデスクトップファーストアプローチ以外でも問題がある。言語自体はLeanとは違う（必ずしも良いとは限らない）けど、依存型についてのいくつかのポイントには同意するよ。両方の言語は、主に異なるトレードオフをしているみたいで、個人的にはそれは公平だったし、それぞれのドメインにとってかなり効率的なツールに成長したと思う。「証明」のドメインは広くて、異なるパラダイムにはそれぞれ強みと弱みがあるから、Leanはこのスペースの別の部分に特化しているだけだね。Sledgehammerはいいけど、Lean用の同等のものが移植されたり作られたりするのは時間の問題だと思う。探索的なフェーズで使うのもいいかもしれないけど、リソースをたくさん使うし、証明を簡潔にするけど、通常は公開コードで証明の全ステップを直接見たいな。「Sledgehammerで」みたいな半魔法的な表現よりもね。Isabelle自体で作業するのは、Leanと比べると痛い（特に開発者とのコミュニケーションが）。メーリングリストでの「バグはない、予期しない動作があるだけ」みたいな発言は、子供っぽいしプロフェッショナルじゃないと思う。Leanや関連システムのRAM消費についての指摘も、IsabelleのRAMへの貪欲さを考えるとちょっと冗談みたいだね。
└
> ただ、通常は公開コードで証明の全ステップを直接見たいな、「Sledgehammerで」みたいな半魔法的な表現よりも。これに関する一つの問題は、UNSATのためのすぐにチェックできる証明書を考えるのが簡単な問題ではないってことだ。これは実質的に形式的な証明を書くのと同じことだね。
└
最後に確認したとき、Isabelle/HOLはカスタムEmacsモードをインターフェースとして使ってたよ。（他のHOLと混同してるかもしれないけど）。
└
> Sledgehammerはいいけど、Lean用に同等のものが移植または作成されるのは時間の問題だと思う。Sledgehammerが何か全然知らないけど… > それは証明を簡潔にするけど、私は通常、公開されたコードで「sledgehammerによる」とかの半魔法的な表現よりも、証明の全ステップを直接見たいな。この説明だと、sledgehammerはMathlibの`grind`と同じに聞こえるね。 https://leanprover-community.github.io/mathlib4_docs/Init/Gr...
著者はLeanについて深刻な誤解をしているようで、驚きだね。彼はこの分野にかなり詳しいみたいなのに。具体的には、著者はLeanが証明オブジェクトを保持していて、チェックされる最終的な証明が一つの巨大な証明オブジェクトで、すべての定義が展開されているという印象を持っているみたいだ。「これらの巨大な項は不要だけど、それでも保持されている」（TFA）。これは真実からほど遠い。Leanは、著者がLCFで大切にしているのと全く同じ最適化を実装している。比喩的に言うと、「証明のステップは実行されるが記録されない、まるで小さな黒板を使っている数学の講師が、後の部分のために証明の早い部分を消していくように」（TFAからリンクされたブログ投稿より引用）。`theorem`（`def`ではなく）がLean4で書かれると、その証明オブジェクトはもはや使われない。これは単なる最適化ではなく、言語の重要な部分なんだ：定理は不透明だ。証明項が破棄されない場合（破棄されないかどうかはわからないけど）、それはインタラクティブモードでのユーザーの可視性のためだけだろう；カーネルは証明オブジェクトが何であったかを気にしないし、気にすることもできない。
└
依存型理論における証明オブジェクトは、単に型に属する項のことだよね。つまり、Leanの実装はそんな項を構築せずに証明を作れるってこと？
文脈から切り離されて見ると、思わず二度見しちゃう名前の一つだね。「Leanや紫の飲み物は、レクリエーション用の薬物として使われる多成分飲料だ。オピオイド薬を含む処方箋グレードの咳や風邪のシロップを混ぜて作る」っていうのは、CSの最も難しい問題の一つである「名前を付けること」が今も続いていることを証明してる。
「今日、どんなシステムでも形式化されているほとんどすべてのものはAUTOMATHでも形式化できたと思う。その主な欠点は、記法が本当にひどかったことと、自動化がまったくなかったことだ。証明は長くて読みにくかった。」これは、今日の好きなモダンな言語でプログラムできるものは、50年前にアセンブリでプログラムできたと言っているようなものだね。技術的にはそうだけど、経済的には違う。
└
そうだね、アセンブリ言語は一般的にチューリング完全だよね。証明エンジンでのパラレルは何になるんだろう？
なんか、Pythonの科学計算における短所を指摘する記事みたいだね。もちろん、ただし、ある程度良いツールの周りにコミュニティが臨界質量を持つようになると、それが他のほとんどのことを上回るんだよね。勢いがついて、みんながチュートリアルや解説、より良いドキュメントを書き始める。そうすると、脱出速度に達する。Leanも、テレンス・タオが強力な支持者/応援者としているから、その流れにいる気がする。 「でも言語Xの方がいい」って主張する人たち…間違ってるわけじゃないけど、重要な議論をしてるわけじゃないよね。みんなが知っていて使えるもので、改善にもっと多くの人の時間がかかっているものよりも良いのか？「悪い方が良い」状況のような気がするし、あるいは「良くて人気があるのが十分良い」って感じかな。
└
> 「ある程度良いツールの周りにコミュニティが臨界質量に達すると、それが他の多くのことを上回る」 これはAIの時代ではあまり重要じゃなくなったね。AIは大量のコミュニティ製のライブラリを必要としないし、自分で書けるから。プログラマーとは違って、実際に仕様書やドキュメントを読むから、ネット上にチュートリアルがたくさんあっても必要ないんだ。（チュートリアルはドキュメントや仕様の投影に過ぎないしね。）AIは仕事市場がない言語を避ける必要もない。なぜなら、キャリアを築くのではなく、目の前の仕事をこなせばいいから。これによって、小さな言語やDSLが今まで使われなかったところでも使われるようになると思う。AIがプログラミングの言語単一文化（上位20はほとんど同じデザインのわずかなバリエーション）を終わらせるかもしれないと思ってる。
みんなLeanは関数型プログラミングにすごくいいって言うけど、Agdaから来た私には、ちょっと使いづらくなった感じがする。タクティクスも良いって言われてるけど、私はCoqのタクティクスの方がパワフルで使いやすいと思ってる。これが全部「赤ちゃんアヒル」の感覚かもしれないけど、今のところLeanの強みは何かのベストではなく、すべてにおいてそこそこ良くて、コミュニティが大きいことだと思う。ポイントは分かるし魅力もあるけど、少しの美しさや力が失われてしまうのが悲しいな。
└
でも、これは両方の後に来るんだよね。もしかしたら「何でも屋」って感じかもしれないけど、他の言語がニッチなままでいる中で成功した理由があるんだと思う。
└
言い換えれば、ネットワーク効果だね。私の視点では、ネットワーク効果はその瞬間感じるほど長続きしないと思ってる。例えば、すべてにおいてそこそこ良くて大きなコミュニティがあるだけが重要なら、Perlは今でも大きな存在であるはずだよね。似たような例はたくさんあるし。Leanの場合、大きなライブラリを持っていることが本当に大きな違いを生むんだ。PerlがCPANを持っていたことで大きなブーストを得たのと同じようにね。（CPANはCTANの模倣だけど、TeXの代わりにプログラミング言語用のもの。）でも、スケーリング法則に基づくと、ほとんどのユーザーにとって大きなライブラリの価値はライブラリのサイズの対数に沿って成長するはずだよ。（関連するスケーリング法則については、https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do... を見てね。）ライブラリが小さいと、これが超えられない壁のように見えるけど、使いやすさの要素が重要になるためには、その規模に合わせる必要はないんだ。数学ライブラリの移植はLLMにとって良いターゲットだと思う。ソースは検証済みで、ターゲットも検証可能だし、推論の道筋も一般的に移植できるからね。これとは逆に、LLMのおかげで、マイノリティプラットフォームで作業することは、思っているほどの障壁ではなくなってる。もし彼らのライブラリがあなたのプラットフォームに移植できるなら、あなたの証明も彼らのプラットフォームに移植できる可能性が高いよ！
└
ちなみに、今はRocqだよ: https://en.wikipedia.org/wiki/Rocq
└
Agdaの関数型プログラミングの何が好きなの？聞くところによると、依存型パターンマッチングがすごく評価されてるみたいだけど、Leanはその点でかなり不利だと思う。でも、Agdaが「普通の」FPに対してフレンドリーだと思うかどうか、もしそうならどういうところがそう思うのか、気になるな。
一番大事なのは、もっと多くの証明を形式化して、ライブラリや基盤作業を強化し続けるための勢いを保つことだね。その勢いがLeanで一番強いなら、それでいいと思う。同時に、機械での検証が進むにつれて、新しいシステムへの移行も簡単になるだろうね。すでにClaude Codeのような一般的なエージェントを使って強力にサポートできるから。