論理の台所

Lean の証明は、決められた公理と推論規則から組み立てられ、カーネルが一歩ずつ検査します。

では、その公理と規則は矛盾していないのでしょうか。それを Lean 自身に確かめさせることはできるのでしょうか。

結論から言うと、できません。

「Lean は無矛盾である」という文は Lean の中で書けます。でも Lean が本当に無矛盾なら、その文を Lean の中で証明することはできません。ゲーデルの第2不完全性定理の帰結です。

この回では、

・「Lean の中で証明する」の3つの意味（数学を証明する／Lean をデータとして書く／Lean について証明する）

・Lean4Lean と lean4lean-model：「Lean は無矛盾」を Lean の命題として書いた実例

・第2不完全性定理と、Lean がその条件を満たすこと

・では誰が保証するのか：外から持ち込む仮定（到達不能基数）と、保証の連鎖

を順に話します。

YouTube 版（画面つき）: 近日公開

前回（形式検証入門）: ep01

◾️チャプター

0:00 オープニング

1:28 01 「Lean の中」の3つの意味

2:18 02 「Lean は無矛盾」を書く

4:26 03 第2不完全性定理

6:40 04 では誰が保証するのか

◾️第2章で画面に出したコード

lean4lean-model の Consistency.lean（master、2026-09-23 版）の定理です。`env.WF` は「宣言の並びがきちんと作られている」という仮定、`VExpr.false` は `∀ p : Prop, p`（「どんな命題も成り立つ」。偽の代わり）です。証明の欄は `sorry` で、最初の引数に仮定 `OmegaInaccessibles`（到達不能基数が無限個並んでいる）がついています。

```lean

theorem consistency (_ : OmegaInaccessibles.{u}) {env : VEnv} (_ : env.WF) (U : Nat) :

¬ ∃ e, env.HasType U [] e VExpr.false := by

sorry

```

◾️出典

M. Carneiro, "The Type Theory of Lean", master's thesis, Carnegie Mellon University, 2019.

https://github.com/digama0/lean-type-theory/releases/tag/v1.0

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

https://github.com/digama0/lean4lean

lean4lean-model

https://github.com/digama0/lean4lean-model

con-leche

https://github.com/leanprover/con-leche

Foundation

https://github.com/FormalizedFormalLogic/Foundation

Lean Language Reference「Axioms」

https://lean-lang.org/doc/reference/latest/Axioms/

◾️補足

・「自身は無矛盾である」は、体系の証明可能性を素直に書き下した文のことです。書き方を工夫すると結論が変わる例が知られています（Feferman 1960）。

・ゲーデル数化については、論計舎の過去の動画「符号化〜数値計算から情報処理へ〜」で扱っています。https://youtu.be/ufBJgGOrpck

◾️問い探しから伴走するセッション・コース

https://ronkeisha.net/session/

◾️論計舎webサイト

https://ronkeisha.net

◾️川井 新（かわい しん）のX

https://twitter.com/squawai

2026年10月6日、OpenAI が数学の研究成果をまとめたリポジトリ openai/math を公開しました。 ユニークゲーム予想の証明など、理論計算機科学の長年の未解決問題について結果を主張しています。 ただし、P vs NP 問題を解決したとはどこにも書かれていません。クレイ数学研究所も、P vs NP を未解決としています。

そこでこの回では、解決が発表される日が来る前に、P vs NP がそもそも何を問う問題なのかを説明しておきます。 解決が近いと予測する回ではありません。

この回では、 ・部分和問題で見る「見つける」と「確かめる」の違い ・決定問題、入力サイズ、多項式時間とクラス P ・証拠と検証器によるクラス NP の定義（NP は Non-Polynomial の略ではない） ・帰着、NP 困難、NP 完全と Cook–Levin の定理 ・P = NP なら、P ≠ NP なら何が言えるのか（言いすぎに注意） ・半世紀以上解けない理由：相対化・自然な証明・代数化の障壁 ・2026年10月の成果は P vs NP とどう関係するのか を順に話します。

YouTube 版（テロップつき）: https://youtu.be/wZRkyPHXKtc

◾️チャプター 0:00 オープニング 1:48 01 見つけると確かめる 2:47 02 決定問題とクラス P 5:52 03 証拠と検証器、クラス NP 9:01 04 帰着と NP 完全 13:00 05 P = NP なら、P ≠ NP なら 16:23 06 なぜ半世紀以上解けないのか 18:51 07 2026年10月の成果に戻る

◾️訂正（言い間違い） 2:16ごろ　2 の 100 乗は「およそ 1.27 × 10 の 30 乗」で、31桁です。 4:32ごろ　「探さないと分からなそうに見える」ことと「速く解けない」ことは別、が正しい言い方です。 5:33ごろ　指数の例は「1.0001 の n 乗」です。 11:03ごろ　SAT は、式全体を「真」にできるかを問う問題です。 13:53ごろ　充足可能ならそのまま、不可能なら偽に固定します。 16:02ごろ　P ≠ NP は「すべての入力が難しい」という意味ではありません。言っているのは最悪の場合の難しさです。 18:32ごろ　障壁は「P ≠ NP が正しい」ことの証拠ではありません。 20:55ごろ　「P ≠ NP という主張なら、どんな手法で、相対化・自然な証明・代数化の障壁をどう越えたのか」が正しい言い方です。

◾️補足 ・Cook–Levin の定理：Cook の論文は1971年、Levin の論文は1973年です。 ・素数判定が P に入ることの証明（Agrawal–Kayal–Saxena）は2002年に発表、論文の掲載は2004年です。 ・自然な証明の障壁の「標準的な暗号の仮定」は、強い擬似乱数生成器が存在するという仮定です。 ・openai/math の結果は、いずれも OpenAI による主張として紹介しています。専門家による独立の検証はこれからです。

◾️出典 OpenAI「openai/math」（2026-10-06 公開、確認したコミット adc7f12）https://github.com/openai/math OpenAI「Sharing AI progress in mathematics」（2026-10-06）https://openai.com/index/sharing-ai-progress-in-mathematics/ Clay Mathematics Institute「P vs NP」（2026-10-07 閲覧）https://www.claymath.org/millennium/p-vs-np/ S. A. Cook (1971), "The complexity of theorem-proving procedures", Proc. 3rd ACM STOC. https://doi.org/10.1145/800157.805047 L. A. Levin (1973), "Universal sequential search problems", Problemy Peredachi Informatsii 9(3). R. M. Karp (1972), "Reducibility among combinatorial problems", Complexity of Computer Computations. M. Agrawal, N. Kayal, N. Saxena (2004), "PRIMES is in P", Annals of Mathematics 160(2). https://doi.org/10.4007/annals.2004.160.781 T. Baker, J. Gill, R. Solovay (1975), "Relativizations of the P =? NP question", SIAM J. Comput. 4(4). https://doi.org/10.1137/0204037 A. A. Razborov, S. Rudich (1994), "Natural proofs", Proc. 26th ACM STOC. https://doi.org/10.1145/195058.195134 S. Aaronson, A. Wigderson (2008), "Algebrization: A New Barrier in Complexity Theory", Proc. 40th ACM STOC. https://doi.org/10.1145/1374376.1374481 L. Fortnow (2009), "The status of the P versus NP problem", Communications of the ACM 52(9). https://doi.org/10.1145/1562164.1562186

◾️問い探しから伴走するセッション・コースhttps://ronkeisha.net/session/

◾️論計舎webサイト https://ronkeisha.net

◾️川井 新（かわい しん）のXhttps://twitter.com/squawai

「AIがフェルマーの最終定理を証明した」。2026年9月、そんなニュースが流れました。

では、この結果で何が保証されたのでしょうか。

実際に行われたのは、新しい証明の発見ではなく「形式化」です。

すでにある証明を Lean という言語のコードに書き直し、カーネルと呼ばれる小さなプログラムに一歩ずつ検査させたのです。

人間が1300万行を読み直さなくても信頼できるのは、何を信頼するかが変化したからです。

ただしこの変化の後でも、機械だけでは確かめられないことが残ります。

この回では、

・形式検証を支える3つの部品（形式言語・推論規則・カーネル）

・1300万行の証明を信頼するために確認すること（検査の仕組み・使われた公理・命題と定義）

・Lean での実演：書き間違えた仮定が通ってしまう例、#print axioms と sorryAx

・カーネルが確かめないこと：命題と定義は意図どおりか

を順に話します。

YouTube 版（画面つき）: https://www.youtube.com/watch?v=O1jC1apGAIc

◾️チャプター

0:00 オープニング

1:18 01 証明を検査する仕組み

2:36 02 信頼の置き場所

4:01 03 Lean で確かめる

6:32 04 カーネルが確かめないこと

8:08 05 「AIが証明した」と聞いたら

◾️実演で使った Lean のコード

書き間違えた仮定（「n > 2」のつもりが「n < 2 かつ n > 2」）。満たせない仮定からは何でも導けるので、1行で通ってしまいます。

```lean

theorem flt_oops (a b c n : Nat) (h : n < 2 ∧ n > 2) :

a ^ n + b ^ n ≠ c ^ n := by

omega

#print axioms flt_oops

-- 'flt_oops' depends on axioms: [propext, Quot.sound]

```

正しく書いた命題（Mathlib の FermatLastTheorem と同じ形）。証明は sorry で空けてあります。

```lean

theorem flt (a b c n : Nat) (hn : n ≥ 3)

(ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) :

a ^ n + b ^ n ≠ c ^ n := by

sorry

#print axioms flt

-- warning: declaration uses `sorry`

-- 'flt' depends on axioms: [sorryAx]

```

◾️出典

Anthropic「Formalizing Fermat's Last Theorem」（2026-09-04）

https://www.anthropic.com/research/formalizing-fermats-last-theorem

◾️問い探しから伴走するセッション・コース

https://ronkeisha.net/session/

◾️論計舎webサイト

https://ronkeisha.net

◾️川井 新（かわい しん）のX

https://twitter.com/squawai

第2回｜チャーチ＝チューリング・テーゼとは何か

前回置いた「計算とは何か」という問いに対して、

20世紀の論理学者たちは、ひとつの大胆な合意に到達しました。

それが、チャーチ＝チューリングの定立です。

この回では、

- チャーチ＝チューリング・テーゼが「定理」ではない理由

- 定立が受け入れられている理由

- 「計算できる」という直観と、形式的なモデルの関係

といった点を軸に、

計算可能性という概念がどのように定立されたのかを整理します。

代わりに、このテーゼがどのような態度表明として受け入れられてきたのかを見ていきます。

第1回｜「計算できる」は、当たり前ではない

コンピュータが身近になった今、

「計算できる」という言葉は説明不要のように見えます。

しかし実際には、

この言葉は長い時間をかけて、ようやく形を与えられたものでした。

この回では、

- 人間が行う計算とは何か

- それを「手続き」として捉えるとはどういうことか

- なぜ20世紀にこの問題が切実になったのか

を手がかりに、

後続回で扱う「チャーチ＝チューリング・テーゼ」への準備を行います。