『Lean で証明できた』は何を保証するのか？ 〜 Lean の無矛盾性と信頼の根拠 〜

こんにちは｜こんばんは。カエルのアイコンで活動しております @kyamaz です。

はじめに

2026年9月8日、生成AI が数学分野で有名なミレニアム懸賞問題のひとつ、ナビエ・ストークス方程式の存在と滑らかさに関する問題（の一部）を解決したという発表がありました。「外力がある場合に3次元の流れの解が有限時間で特異点を生じうる、つまり滑らかな解がいつまでも続くわけではない」ということを示したものだそうです。ニュースをご覧になった方も多いのではないでしょうか。

私 がここで目を留めたのは、成果が解析的な証明だけでなく Lean による形式化とセットで公開された、という点です。Quanta Magazine の記事にも、形式化されていることが "giving mathematicians confidence that it is indeed correct"（それが本当に正しいという確信を数学者に与えている）と書かれていました。人間が読み切るには重すぎる証明でも、機械が通したのであれば信じられる、というわけです。おかげで Lean というプログラミング言語にもずいぶん注目が集まっているように感じます。なお、成果の帰属や発表に至る経緯をめぐっては論争もあるようですが、本稿ではそちらには立ち入りません。

【ナビエ・ストークスのニュース記事とLeanプログラム】

そして、その2か月ほど前に何があったかもあわせて思い出しておきたいところです。2026年7月「AI の助けを借りてコラッツ予想を反証した」という証明が公開されました。こちらも Lean4 で書かれていて、機械チェックも通っていたそうです。しかし3日後、その実態が明らかになります。この Lean4 の証明は数学的な検証ではなく、Lean4 の処理系そのもののバグを突いたものでした。

定理証明支援系（proof assistant）は、書いた証明が正しいかどうかを機械的に判定してくれて、形式化が正しくてコンパイルが通ればOKを示すチェックマークを出してくれます。ミレニアム懸賞問題の解決を信じる根拠にもなれば、嘘の証明を通してしまうこともありえます。この出来事は、普段あまり意識しない問いを浮かび上がらせたように思います。

【疑問】
「Lean で証明が通った」というとき、私たちは何を信じているのでしょうか？　その Lean 自身が正しいことは、いったい誰が保証しているのでしょうか？

私 は形式手法の専門家ではありませんし、Lean を日常的に書いているわけでもありません。それでもこの問いは気になりましたので、本稿では調べたことを整理してみようと思います。この問いは、実は3つの別々の問いから成っているようです。

• Lean の論理体系に矛盾は潜んでいないか（数学的な問い）
• Lean というプログラムにバグはないか（実装の問い）
• そもそも書いた命題が意図どおりか（記述の問い）

1つ目が完璧でも2つ目で破れれば同じことになりますし、1つ目と2つ目が完璧でも3つ目が崩れれば意味がありません。この後、順に見ていきましょう。

そもそも「矛盾している」とは

形式体系が矛盾しているとは、そこから偽（False）が証明できることをいいます。矛盾した体系では、爆発律（principle of explosion /「論理学において矛盾（偽）からは任意の命題が導かれるという原理」）によってあらゆる命題が証明できてしまいます。例えば、型システムに抜け穴があって、どんな型の値でも undefined から作れてしまう状態に近い、と考えるとよいかもしれません。リーマン予想も「$1 = 2$」のような矛盾が混ざっているなかで証明できてしまう装置となってしまっては、全く価値のないものになってしまいます。
ですので「Lean は無矛盾か？」という問いは、「Lean で False は証明できないか？」という問いと同じことになります。

問い1：論理体系としての無矛盾性 〜 ゲーデルの壁

では、無矛盾性を証明すればよいではないか、と思うところに最初の壁があります。『ゲーデルの第二不完全性定理』がその裏付けになります。十分な表現力を持つ無矛盾な形式体系は、自分自身の無矛盾性を証明できない、というものです。

つまり Lean の中で「Lean は無矛盾である」を証明することはできません。もっと悪いことに、もし Lean がそれを証明できたとしたら、それは Lean が矛盾しているということにもなってしまいます。これは Lean の欠陥ということではなく、ZFC 集合論でもペアノ算術でも同じことが起きるので、数学の基礎的な制約と考えるべきです。

代わりに数学がやっているのは、相対無矛盾性の証明です。「体系 M が無矛盾ならば、体系 T も無矛盾である」という形の主張で、T を M の中に翻訳して、T で False が導けるなら M でも導ける、ことを示しています。

ここで注目したいのは、これは本来の問いを解消はしていないという点です。「Lean は大丈夫か？」が「体系 M は大丈夫か？」に付け替わっているだけともいえます。私 は、相対無矛盾性の証明というのはこの問いを解消する機構ではなく移送する機構なのだ、と理解しました。それでも意味があるのは、移送先が何十年（数学という枠組みでいえば何百年ともすると何千年）も使われていて矛盾の兆候が出ていない体系だからということのようです。信頼は証明ではなく実績で担保されているわけで、枯れたライブラリを選ぶときの判断と構造は同じように思えます。

Lean の場合は、Mario Carneiro が2019年の論文で、その型理論が ZFC ＋「到達不能基数が $n$ 個存在する」（すべての自然数 $n$ について）と等しい無矛盾性の強さを持つことを示しています。到達不能基数というのは、下から手続き的には到達できないほど大きな無限のことです。つまり Lean は ZFC の無矛盾性に加えて、到達不能基数に関する仮定を受け入れる必要がある、ということになります。

ただし、ここでは注意が必要です。この結果は Lean3 のものです。 Lean4 では型理論が拡張されており（入れ子の帰納型、構造体に対する $\eta$ 規則など） Carneiro 自身が後の論文で「2019年の健全性証明はもはや直接には適用できない」と述べています。 が調べたところによると、「Lean は ZFC + 到達不能基数に相対的に無矛盾」という評判に反して、Lean4 の型理論に対する完全な無矛盾性証明は、2026年9月現在まだ完成していなさそうです。

とはいえ、この課題について放置されているわけではありません。Lean4Lean というプロジェクトがあり、論理体系の性質と、型検査器がその規則どおりに動くことの両方を検証しています。型検査器が指定された推論規則どおりに動くことを検証するのと、その規則自体の無矛盾性を無条件に自己証明することは別です。論文では「型の一意性」などが予想として残っていますが、これらが必要になる型検査器の正しさの証明と、別経路で進められる健全性の証明を区別しています。どこまでが証明済みで、どこからが未証明かが追える形で公開されていること自体が、健全さの表れといえますが、現状完全ではないということのようです。

【Lean4Lean の論文】

問い2：理論が正しくても、実装は間違う

さて、ここからがエンジニアにとって興味のある問いかと思います。論理体系の無矛盾性を仮定できたとしても、それを実装したプログラムにバグがあれば False （偽）を証明できてしまいます。

証明オブジェクト 〜 なぜ「検査する側」だけを信じればよいのか

Lean が採っているその防御策を理解するには、証明オブジェクトという考え方を押さえておく必要があります。おおまかに言うと、Lean では「定理は型であり、証明はその型を持つ項（データ）である」という見方をします。証明とは、処理系の中に存在するデータ構造であって、あとから検査できる証拠（certificate）となります。

証明を作る部分（Tactics, Elaborator, 型推論）は複雑ですが、出力された証明オブジェクトを検査する部分は、規則を機械的に照合するだけの小さなプログラムで済みます。ここで信頼するのは検査器（カーネル）だけでよい、ということになります。この設計原理は『デ・ブリュイン基準』と呼ばれているそうです。コンパイラ本体ではなく、出力された機械語のほうを小さな検証器にかける、という発想に近いといえるでしょうか。
信頼するコード、すなわち TCB（Trusted Computing Base）を極小に保つ。ここまではとても美しい話です。

ところが、カーネルは小さくない

ところが Lean のカーネルは、必ずしも「小さく単純」ではないようです。性能と表現力のために、入れ子の帰納型、構造体の射影、多倍長整数演算（GMP による自然数の高速計算）といった機能が、カーネルの内部に入っています。Lean4 への移行でも書き直されず、C++ のまま残った数少ないコンポーネントの一つでもあるようです。つまり、カーネルの機能量がそのまま攻撃される要素になってしまう、ということです。

そして2026年、それが現実になりました。冒頭のコラッツ「反証」が突いていたのは、入れ子の帰納型の処理¹でした。コンストラクタに現れないパラメータが内部で生成される補助型から消えてしまい、型検査をすり抜けてしまったそうです。その穴を通して、本来あるべきではない False が証明されてしまったわけです。そして、その報告からわずか1時間で修正パッチが出たそうです。
さらに恐ろしいことに、この証明は Lean 公式のカーネルと、独立に実装された別のチェッカ（Chris Bailey による Rust 実装の nanoda）の両方を通過していました。しかもこのバグのポストモーテム¹によれば、踏んでいたのは互いに無関係な2つのバグだったそうです。nanoda のほうは該当箇所をきちんと検査してはいたものの、射影ノードの型名を検証していなかった、とのことでした。「二重チェックしているから安全」という前提も、実際には崩れてしまった事例となってしまいました。

これを受けて、7月30日から8月20日にかけて、OpenAI の Daniel Selsam が同社の社内モデルを使ってカーネルとランタイムの健全性バグを集中的に探す、という取り組みも行われ、カーネルの健全性で4件、ランタイムの健全性で2件、その他5件の修正が入ったそうです。その内のひとつは、ある1つのオブジェクトに大量の参照を作って参照カウンタを一周させ、オブジェクトの状態を壊して False を作る手口だったり、もうひとつは、Linux 版の CI が libc 互換性の都合で GMP v6.1.2（多倍長演算ライブラリ）を使ってビルドしていたために、その既知バグを突けてしまう、というものでした。証明の健全性が、メモリ安全性や外部ライブラリという「数学ではない層」から破られてしまうということでした。一連の修正は v4.33.1 として8月21日にリリースされています。
Lean の作者である Leonardo de Moura は「これは今後も起き続ける。AI はカーネルの健全性バグを突くのが本当に得意だ」と述べています。バグハントのポストモーテム²でも「AI が生成した証明は、悪意ある証明の潜在的な発生源だと考えている」と明言されています。証明の検証は、数学の問題であると同時にセキュリティエンジニアリングの問題でもある、といえそうです。

これは Lean 固有の課題ではない

これらはすべて実装のバグであって、理論の穴ではありません。修正すれば消える種類の欠陥です。ただし、利用者から見れば「間違ったチェックマークが出た」という結果は同じになってしまいます。
また、これは Lean 固有の課題というわけでもなさそうです。Rocq（旧 Coq）にも過去に健全性バグは見つかっていて、既知の重大バグの一覧が管理されています。十分に長く使われた証明支援系で、実装バグが一度も見つからなかったものは、ほぼ存在しないのではないでしょうか。差が出るのは、バグが出にくい設計になっているか、出たときに迅速に修正される体制があるか、という点だと思います。

『LCFアーキテクチャ』を採用している Isabelle/HOL の設計者である Lawrence Paulson は「なぜ何もかもカーネルに入れるのか」と問いかけています。LCF 系の伝統（HOL Light、HOL4、Isabelle/HOL）では、再帰・帰納的データ・パターンマッチをカーネル内には入れず、最小限の原理からカーネルの外で導出します。手間はかかりますが、信頼する部分は劇的に小さくなります。彼の結論は「健全性が最優先なら HOL Light か HOL4 を選べ」というものです。一方で Lean の設計は、表現力・性能・巨大な数学ライブラリ（mathlib）を成立させるための選択でもありますので、どちらが正しいかではなく、信頼の小ささと生産性のトレードオフをどこで取るか、という話だと思います。皆さんはどちらを採られるでしょうか？

【Paulson のブログ記事】

「チェッカを増やせばいい」は答えになるか

『デ・ブリュイン基準』を採用した設計そのものについても、Paulson はもう一つ鋭い指摘をしています。証明オブジェクトを証明書として持ち運んで、別のチェッカにかける。その設計の価値そのものが今回疑われた、という点です。公式カーネルと nanoda が同じ証明を通してしまったという事実からの批判です。彼の比喩でいえば「スペアカーを牽引して走り回るようなもの」で、同じ理由で一緒に壊れるのであれば、予備は予備になっていません。
この指摘は半分正しいように思います。独立に実装されていることと、独立に壊れることは、同じではない。 今回は異なる二つのバグが同じ証明を通した事例です。一方、独立チェッカ一般の設計では、仕様やアルゴリズムの共有による共通の欠陥にも注意が必要です。同じ仕様を読んで、同じアルゴリズムを写して書かれたチェッカは、仕様の側に穴があれば揃って通してしまいます。冗長化がどれだけ効くかは実装の系統がどれだけ散っているかで決まるわけで、ソフトウェアのフォールトトレランスで昔から言われてきたことと構造は同じです。

そしてこの対策も、単に数を並べる方向だけではないようです。comparator は、信頼できる環境で用意した命題と、提出された証明の命題との一致を確認します。証明をサンドボックス内でビルドして、証明項を取り出して、サンドボックス外の複数の独立チェッカにかけます。lake check --paranoid は、同梱されたすべてのカーネルでプロジェクトを再検査するコマンドで、v4.35.0 から使えるようになる予定だそうです。さらに lean4checker を GMP 版と mpn 版の2つ同梱する計画や、検証済みの任意精度演算パッケージを自前で実装して外部の演算ライブラリへの依存そのものを切る計画も挙がっています。そして lean4lean は Lean 自身で書かれたカーネルで、いずれ形式検証されることを目指しているそうです。最後のものは、横にチェッカの数を増やすのではなく、1つのチェッカの信頼を証明で底上げしようという動きになります。証明オブジェクトという設計が効いてくるのは、まさにこういう場面かと思います。証明が持ち運べるデータである限り、チェッカはいくつでも足せますし、そのうちの1つを形式検証で固めることもできるわけです。

問い3：最後の穴は、人間側にある

理論も実装も完璧だったとして、それでもまだ穴が残ります。しかも実務で注意が必要なのはここではないでしょうか。

正しく証明された、無意味な定理

カーネルがチェックマークを出したとき、それが保証しているのは「そこに書かれた形式的な命題が、宣言された公理から導かれる」ということだけです。その命題が意図した主張と一致しているかどうかは、一切保証していません。仮定が強すぎて定理が空虚に真になっている。記法や型クラスが定義を隠していて、読んだ意味と実際の意味がずれている。こうした間違いは、いくら証明しても検出されません。正しく証明された、無意味な定理ができあがってしまいます。
これは机上の心配ごとではありません。冒頭のナビエ–ストークス方程式の件でも、Quanta Magazine の記事は "The crucial bit of verification that must still be done by humans is to guarantee that the statement being shown to be true in Lean is logically equivalent to what mathematicians set out to prove"（ 人間がやらなければならない決定的な検証は、Lean で真だと示された命題が、数学者が証明しようとしたものと論理的に同値であると保証することだ）と書いています。ミレニアム懸賞問題であっても、最後はここに戻ってくるわけです。

意図的な抜け道と、公理の監査

加えて Lean には、意図的に用意された抜け道がいくつもあります。

【意図的に用意された抜け道】

• sorry … 証明を後回しにする
• ネイティブ評価 … カーネルの外でネイティブコードを実行して、その結果を信じる
• @[implemented_by] … 実装を別物に差し替える
• 型検査そのものを飛ばすデバッグ用オプション

未証明の仮定を持ち込むものや、信頼する実装範囲を広げるものです。どれも正当な用途がありますが、使われ方によって証明の保証に必要な前提が変わってしまうため、確認が必要です。Lean を学んでいない人は sorry の存在を知らなかったりします。sorry は、初学者が証明を通すのに苦労するときや、順次プログラムを記述する際に便利に使う記法ですので、入門の早い段階でこの抜け道を覚えてしまいます。Lean を少しでもかじったことのある人であれば、ニュースになっている Lean のコードに sorry がないことは真っ先に見るでしょうが、知らない人は sorry があったとしても正しく証明されたと誤解してしまうことでしょう。

なお幸いにも、依存した公理のほうは監査できます。

#print axioms my_theorem
-- 'my_theorem' depends on axioms: [propext, Classical.choice, Quot.sound]

この3つ（命題外延性・選択公理・商の健全性）は Lean の標準的な公理ですので、出てくる分には問題ありません。逆に sorryAx や見知らぬ独自公理が現れたら赤信号です。しかしながら、命題の意味が正しいかどうかを判定するコマンドは存在しません。形式的な命題と人間の意図との一致は、証明が通ったことだけでは保証されず、人間のレビューが残ります。

【公式リファレンス "Validating a Lean Proof"】

で、実際どうすればいいのか

抽象論で終わらせずに、実務の指針としてまとめてみましょう。

【AI 時代に証明を扱うときの指針】

• 定理の主張（statement）を読む … 形式検証だけでは意図との一致を保証できないため、主張と、それが参照する定義をレビューします
• #print axioms を CI に入れる … 依存公理が {propext, Classical.choice, Quot.sound} の部分集合であることを機械的に確認します
• 他人の証明、とりわけ AI が生成した証明は信頼できない入力として扱う … ビルドはサンドボックスで行って、comparator や複数チェッカで再検査します
• 処理系は素直に更新する … 健全性バグは公開され、素早く修正されます。古いバージョンに留まるほうがリスクが高いでしょう
• 保証の範囲を過大に語らない … 「Lean で証明した」というのは「この形式的命題がこの公理系から導ける、と現時点の処理系が判定した」ということであって、それ以上ではありません

まとめ

「Lean は無矛盾か？」への答えは、それぞれのレイヤによって違うように思います。

• 論理体系 … 絶対的な保証は原理的に存在しません。語れるのは相対無矛盾性だけで、移送先は ZFC + 到達不能基数です。しかもその証明は Lean3 のもので、Lean4 版は現在進行形の作業になっています
• 実装 … 理論が正しくてもプログラムは間違います。参照カウンタや外部ライブラリという、数学ではない部分から破られる可能性があります
• 記述 … 理論と実装が完璧でも、書いた命題が意図とずれていれば全て無意味になります

これらのレイヤはどれも完全ではありません。サンドボックスでのビルド、複数の独立チェッカ、#print axioms による公理の監査、そして主張そのもののレビュー、といった運用で補うことになります。
証明支援系は「絶対の真理を出力する機械」ではないのだと思います。疑うべき対象を、人間がレビューできる大きさまで絞り込む装置、というくらいが実態に近いのではないでしょうか。信頼は一つの証明から生まれるのではなく、理論・実装・運用・レビューの積み重ねから生まれるものなのでしょう。

おわりに

いかがでしたでしょうか。本稿では、「Lean は無矛盾なのか？」という素朴な問いを、論理体系・実装・記述という3つのレイヤに分けて眺めてみました。この構造は、普段からソフトウェアの品質保証やセキュリティでやっていることとよく似ているように思えます。証明支援系が特別なのは、その多層防御の一番内側の層が数学の体系に基づく定理となっている点が特徴的なのかもしれません。それは十分すごいことですが、万能ではないということです。

なお、本稿は私 が公開情報を拾って整理したものです。Lean4Lean の未解決の予想がどうなっているかまでは追い切れておりませんし、バグハントで見つかった個々の問題についても、de Moura のポストモーテムを要約した以上のことは書けておりません。誤りや最新の状況などがありましたら、教えていただけると嬉しいです。

ご一読いただきまして有り難うございます。
（●）（●） Happy Hacking!
/""　＿＿""＼

1. Lean の issue #14576 として報告されたバグです。カーネルが入れ子の出現（nested occurrence）を除去する際に生成する補助型から、コンストラクタのフィールドに現れないパラメータ（phantom parameter）が落ちてしまう、というものでした。攻撃経路はメタプログラミングでカーネルに直接 inductive 宣言を送ることで、通常のフロントエンド経由ではチェックが効いていたそうです。このバグのポストモーテム(↓)
   https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/ ↩ ↩²

2. https://leodemoura.github.io/blog/2026-8-24-postmortem-for-the-kernel-soundness-bug-hunt/ ↩