証明支援系のカーネルが「0 = 1」を公理なしで受け入れた。対象は Lean 4 と Rocq（旧 Coq）で、oss-security に 2026年10月26日付けでまとめて公開された一群の CVE だ。Print Assumptions や #print axioms はクリーン、Test Universe Checking は on、それでも False から任意命題が導ける。 検証環境は Debian 13.7、Linux マシン（8 vCPU）、Python 3.13.5、elan で入れた Lean 4.31.0 / 4.32.2 / 4.35.0、Debian の coqc 8.20.1、およびソースからビルドした Rocq 9.3.0 と master（9.4+alpha、PR #22624 取り込み後）である。PoC は endrazine が公開した Docker 再現用リポジトリをそのまま使い、Docker なしでローカル実行した。 まず Lean。CVE-2026-72844 は入れ子帰納型の射影で、構造体名と実体の型が食い違ってもカーネルが通す（CWE-843）。CVE-2026-72711 は opaque 宣言の経路だけ check_no_metavar_no_fvar を飛ばしており、推論キャッシュに残った一時 fvar を悪用して型 False の opaque を登録できる（CWE-488）。どちらも --trust=0 の通常 addDecl 経路で、sorry / unsafeCast / .olean 改ざんは不要だ。 4.31.0 では両方とも成功した。ZeroEqOne.lean は「'zero_eq_one' does not depend on any axioms」と出し、CachePoisonFalse.lean は「kernel accepted bad : False」のあと公理なしで 0 = 1 を導く。lake で olean を出したうえで leanchecker --fresh を回すと、ZeroEqOne も CachePoisonFalse も終了コード 0、所要はそれぞれ約 125 秒と約 126 秒だった。つまり独立チェッカー再実行でも、同じカーネル規則のまま通る。4.32.2 と 4.35.0 では射影側は bad が登録されず、opaque 側は「(kernel) declaration has free variables 'bad'」で落ちる。修正は 4.32.2 以降で、現行安定は 4.35.0（2026-10-12）である。発見者の一人は GPT-5.6 を使ったカーネル監査だと issue に書いており、AI が証明核の欠陥を掘る時代の実例でもある。 次に Rocq。CVE-2026-72714 はモジュール内の Local Unset Universe Checking が閉じたあと、環境フラグは戻るのに ugraph 側のコピーが無効のまま残る不整合だ。Test Universe Checking は on と答えるのに、Hurkens のパラドックスが通り、Print Assumptions は「Closed under the global context」と返す。Debian の coqc 8.20.1 で ZeroEqOne.v をコンパイルするとまさにその通りで、0 = 1 が公理なしで通る。一方 coqchk は「Fatal Error: Type error: CantApplyBadType at argument 1」（終了 129）で弾く。Rocq 9.3.0（2026-09-19 リリース）でも同じく coqc は受け入れ、rocqchk は拒否した。oss-security 投稿時点では 0-day 扱いだったが、Gaëtan Gilbert の PR #22624 が 2026-10-23 に master へマージされており、こちらでビルドした 9.4+alpha では「Unable to unify」で弾かれた。つまり最新リリース 9.3.0 はまだ脆弱で、修正は次期系列待ちだ。 もう一つ、CVE-2026-72703 はガード検査が相互再帰のクロス呼び出しを見ず、非構造的減少を通してしまう穴だ。Claude Opus 4.6 が発見し、機能的な False 証明は ccz181078 による、と PoC に書かれている。8.20.1 では F 2 = S (F 2) が通り、Print Assumptions はクリーン、さらにここが厄介で、coqchk も「Modules were successfully checked」で受け入れた。vm_compute で F 2 を評価すると 20 秒タイムアウトで終わらず、非停止定義そのものが残っている。9.3.0 では「Recursive definition of F is ill-formed」で拒否されるので、ガード側はすでに直っている。 同日の投稿には、この宇宙検査不整合を使ったミレニアム問題の偽証明書（リーマン予想、ナビエ–ストークス正則性、BSD、ホッジ、および P=NP）も列挙されている。Docker で再現でき、Print Assumptions のホワイトリストはクリーン、と主張される。証明支援を「信頼の根」にしているワークフローほど、Print Assumptions だけを信じると穴が残る、という実務的な教訓になる。coqchk / leanchecker、あるいは export 経路の独立検査を併用しないと、偽の証明が CI をすり抜ける。 誰が影響を受けるか。Mathlib や MathComp、CompCert、Iris、形式検証付きスマートコントラクト、Lake / opam 依存として Lean、Rocq を引いているプロジェクトだ。カーネル自体のバグなのでユーザー側の回避策はほぼなく、Lean は 4.32.2 以上へ、Rocq はガード修正済みの 9.2.0 以上へ上げ、宇宙不整合については 9.3.0 時点では coqchk を必須にし、master の修正がリリースされるまで依存を監査する、が現実的な線だ。 日本語圏の反応は薄い。Yahoo リアルタイム検索で「CVE-2026-72714」「CVE-2026-72844」「Lean4 0=1」「Rocq 偽証明」を見た範囲では該当投稿は見当たらず、Zenn で「Lean kernel soundness」「Rocq 偽証明」、Qiita で「CVE-2026-72844」もヒットなしだった（2026-10-26 時点）。形式検証の「0 = 1 が通る」話は海外では critical bug として扱われるのに、国内ではまだほとんど流れていない。 事実と主張の切り分けをしておく。oss-security 上の CVE 番号、影響範囲、修正版は VulnCheck / メンテナ側の記述である。0 = 1 が公理なしで通ること、バージョンごとの合否、coqchk が宇宙不整合を弾く一方でガード穴は 8.20.1 で通してしまうこと、9.3.0 でガードは直り宇宙は残ること、master で宇宙も直ることは、この検証環境での実測である。ミレニアム問題の偽証明一式は公開リポジトリの主張であり、今回は 0 = 1 の最小 PoC までを再現した。 証明支援は「証明を信じる」ための道具だが、信じる対象のカーネルが時々 False を通す。アップデートと独立チェッカーを、数学や安全証明の話から切り離さない方がいい。 GitHub leanprover/lean4 GitHub rocq-prover/rocq GitHub endrazine/lean-cve-poc GitHub endrazine/lean-cve-poc-14484 GitHub endrazine/rocq-cve-poc-22287 GitHub endrazine/rocq-cve-poc-21682 http://openwall.com/lists/oss-security/2026/10/26/ http://nvd.nist.gov/vuln/detail/CVE-2026-72844 http://nvd.nist.gov/vuln/detail/CVE-2026-72711 http://nvd.nist.gov/vuln/detail/CVE-2026-72714 http://nvd.nist.gov/vuln/detail/CVE-2026-72703 #Lean4 #Rocq #Coq #形式検証 #セキュリティ