AI が書いた証明を、Lean というソフトウェアに検査させる。そんな話をよく聞くようになりました。 その Lean は、数学の土台としてよく使われる集合論 ZFC よりも強い体系です。 ここで「強い」とは、相手の体系が矛盾しないことを、自分の中で証明できる、という意味です。 では、なぜ Lean はそこまで強いのか。そして、これほど強い体系を、何を根拠に信頼すればよいのでしょうか。 この回では、 ・体系の「強さ」とは何か（無矛盾性の証明と、ゲーデルの第2不完全性定理） ・Lean はどのくらい強いのか（不完全性定理の条件と、到達不能基数） ・Lean の強さはどこから来るのか（宇宙の階層と、Prop の非可述性） ・強さの具体例（フェルマーの最終定理） ・強い体系を信頼する根拠（自分の中では証明できない無矛盾性と、「Lean で確かめた」を信頼するための4つのこと） を順に話します。 YouTube 版（画面つき）: https://youtu.be/df2ZA-x0yaw 前回（形式検証入門2）: ep03 ◾️チャプター 0:00 オープニング 0:42 01 「強い」とは何か 2:08 02 Lean はどのくらい強いのか 4:05 03 強さはどこから来るのか 6:16 04 強さの具体例：フェルマーの最終定理 7:20 05 強い体系を信頼する根拠 10:36 06 まとめ・論計舎のご案内 ◾️訂正 ・2:47「完全性定理が当てはまりません」は、正しくは「不完全性定理が当てはまりません」です（プレスバーガー算術の話）。 ・10:16「この体系の矛盾性を」と 10:44「体系の矛盾性についての」は、どちらも正しくは「無矛盾性」です。 ・11:11「数学を学ぶのです」は「数学を学ぶ場です」です。 ◾️注意 番組で紹介した Lean の無矛盾性の証明（Carneiro 2019）は、当時の Lean（Lean 3）の型理論について、ZFC に「到達不能基数が n 個ある」（n はいくつでも）という公理を足した体系を仮定する、紙の上の証明です。Lean 4 で加わった機能まで含めた証明は進行中です。前回の回で話した Lean の中での形式化（lean4lean-model）は、到達不能基数が無限個並ぶという、これより強い仮定を置いています。また、前回確認した時点では、その証明の本体は未完成（sorry）でした。 ◾️補足 ・5:52「すべてのほげほげについて」の「ほげほげ」は、どんなに大きな宇宙のものでもよい、という意味の置き場所です（たとえば「すべての型について」）。そのように量化してできた命題も Prop に留まる、というのが Prop の非可述性です。 ・8:26「1個ある、2個ある、ぶらぶらぶら」は、「到達不能基数が n 個ある」という公理を、すべての自然数 n について足すことを指しています。 ・番組の「自分の無矛盾性」は、体系の証明可能性を素直に書き下した文のことです。公理を表す式の選び方によっては、そこから作った「無矛盾性の文」が体系の中で証明できてしまう例も知られています（Feferman 1960）。 ・第2不完全性定理の条件「自然数の算術を十分に展開できる」は、証明の符号化とその性質を体系の中で扱えるだけの算術、という意味です。 ◾️出典 【Lean の強さと無矛盾性】 M. Carneiro, "The Type Theory of Lean", master's thesis, Carnegie Mellon University, 2019.（§1.2） https://github.com/digama0/lean-type-theory/releases/tag/v1.0 B. Werner, "Sets in Types, Types in Sets", TACS 1997, LNCS 1281. https://doi.org/10.1007/BFb0014566 Foundation（Lean の中で ZFC の無矛盾性を証明：zfc_consistent） https://github.com/FormalizedFormalLogic/Foundation/blob/master/Foundation/FirstOrder/SetTheory/Universe.lean M. Carneiro, "Lean4Lean: Verifying a Typechecker for Lean, in Lean", TYPES 2025, LIPIcs 384, 2026. https://doi.org/10.4230/LIPIcs.TYPES.2025.2 lean4lean-model（Consistency.lean） https://github.com/digama0/lean4lean-model/blob/master/Lean4LeanModel/Consistency.lean 【宇宙の階層と Prop の非可述性】 Lean Language Reference「Universes」 https://lean-lang.org/doc/reference/latest/The-Type-System/Universes/ S. Ullrich, "An Extensible Theorem Proving Frontend", PhD thesis, Karlsruhe Institute of Technology, 2023.（§1.3.2） https://lean-lang.org/papers/thesis-sebastian.pdf mathlib4 Counterexamples/Girard.lean https://github.com/leanprover-community/mathlib4/blob/master/Counterexamples/Girard.lean 【フェルマーの最終定理の例】 C. McLarty, "The large structures of Grothendieck founded on finite-order arithmetic", Review of Symbolic Logic 13(2), pp. 296–325, 2020. https://doi.org/10.1017/S1755020319000340 W. Wheeler, "Andrew Wiles' Proof of Fermat's Last Theorem, As Expected, Does Not Require a Large Cardinal Axiom", arXiv:2309.07151, 2023. https://arxiv.org/abs/2309.07151 【不完全性定理とその条件】 M. Presburger, "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt", 1929. S. Feferman, "Arithmetization of metamathematics in a general setting", Fundamenta Mathematicae 49, pp. 35–92, 1960. 【「Lean で確かめた」を信頼するために】 Lean Language Reference「Axioms」（#print axioms） https://lean-lang.org/doc/reference/latest/Axioms/ Lean Kernel Arena https://arena.lean-lang.org/ ◾️問い探しから伴走するセッション・コース https://ronkeisha.com/session/ ◾️論計舎webサイト https://ronkeisha.com ◾️川井 新（かわい しん）のX https://twitter.com/squawai
