draft v0 — 各判定は要再audit STEP 未採番 2026-09-18

適用03 — Lean4 / Mathlib を超える

c 層分離。カーネル最良、仕様層は分母が存在しない。

藤本 伸樹 ／ Rei-AIOS ／ prior-art audit v0

draft v0 — 各判定は要再audit。STEP 未採番。素材のみ。shared tree 不触。 作成: 2026-09-18 / 前提: decision-device-type-prior-art-audit-v0.md の4フィールド（同日）、wolfram-verdict-device-audit-v0.md（同日） 関連: [[lean4-verification]] / [[proof-pipeline-device-map]] PIN 1・PIN 5・PIN 6 / [[rei-compression]] STEP 1894 / STEP 1886

0. 位置づけ — 前2件と結論が違う

前2回の audit（オートマトン、ウルフラム）はどちらも「対象装置は c（較正）を持たない」で終わった。Lean にはこの論法が通らない。

Lean 4 のカーネル判定は、3回の audit で扱った装置のうち最も較正されている。

Mathlib は毎日、全コーパスを nanoda（Rust による独立カーネル）で再検証している。lean4lean は Mathlib 全体を通している（58.79分 vs C++ カーネル 44.54分、1.32倍）。Lean Kernel Arena は 24 個の独立カーネル実装を「誤って受理した無効証明の数 → 誤って却下した有効証明の数 → mathlib テストの検査時間」の順で並べている。

したがって本 audit の主張は前2回と別の形になる：

Lean が保証していない層に空きがある。Lean の中を作り直す余地ではない。

1. 「超える」の分岐

分岐 内容 判定 理由
A. Lean5（基礎理論の置換） 観察的型理論 / cubical / HoTT へ移行 KILL §3.1。提案が世界に存在せず、Lean 2 は HoTT モードを実際に持っていて捨てた
B. Mathlib2（ライブラリの作り直し） モジュール化された後継ライブラリ KILL §3.2。誰も提案していない。mathlib3→4 の移植コストが上限を示している
C. カーネルの独立実装で信頼を上げる 別言語で第 N 番目のチェッカを書く CONFINE 既に 24 実装ある。参加はできるが「超える」ではない
D. TCB と証明書サイズの測定層 検査パイプラインの信頼と costs を測る CONFINE（要警告） §4。彼が既にいる場所だが prior art が今まさに埋まっている
E. 仕様層に判定器を置く 「S は意図した命題か」を測定・ゲートする装置 SURVIVE §3.3。ここだけが空いている

2. Lean 4 を層に分けて4フィールドで型付け

前2回と同じ D = (V 値域, e 誤り率, t 全域性, c 較正)。Lean は単一の判定器ではなく層の積み重ねなので、層ごとに型が違う。 これが本 audit の中心的な観察。

層 V e t c 総合
カーネル（項が型に属するか） {accept, reject} ≈0 全域 24 実装による再検査、毎日の全コーパス再検証 3回の audit で最良
公理フットプリント 公理の集合 — — #print axioms は任意。Mathlib の daily CI は permitted_axioms を持つが unpermitted_axiom_hard_error: false（報告のみ、非致命） opt-in
native 評価（native_decide / ofReduceBool） {accept, reject} 非ゼロ（コンパイラ全体と全 @[implemented_by] を信頼） 全域 外部チェッカは検査不能（lean4lean は reduceBool を実装しない） 穴。Mathlib は linter で禁止
elaborator / メタプログラム — 非ゼロ（環境を直接改変できる） — leanchecker --fresh が緩和策だが PR ごとの CI には無く nightly cron のみ 24時間の窓
statement（命題そのもの） — 未測定 全域 なし。どの証明支援系もゲートしない ここが空いている
definition（定義が概念を捉えているか） — 未測定 — Mathlib のレビュー指針は「(very difficult!)」という人手の問いのみ 同上

2.1 カーネル層 — 較正されている、が但し書きが3つ

較正の実体（本物）：

但し書き1：不一致率が公表されていない。 シグナルは Zulip への pass/fail の二値。「N 宣言中 k 件不一致」を報告した論文もダッシュボードも見当たらない。Kernel Arena はテストスイートに対する誤受理・誤却下の件数を出すが、Mathlib 全体に対する不一致率ではない。

但し書き2：整合性証明は Lean 3 のもの。 Carneiro の Corollary 6.8（verbatim）:

"Lean is consistent if ZFC + {there are n inaccessible cardinals | n ∈ ω} is."

Lean4Lean 論文が自ら述べるとおり、"nested inductive types and η for structures significantly impact the theory, and as a result the soundness proof from (Carneiro, 2019) is no longer directly applicable." Lean 4 の実際の型理論には公表された整合性証明がない。 unique typing は形式化の中で Conjecture 2.7 のままで、"the proof has an error in one of the technical lemmas"。

但し書き3：健全性バグの実測基底率はゼロでない。 Lean 3 は全リリース史でカーネル健全性バグ 0 件。Lean 4 は：

時期 件数 備考
2026-07-28 #14576 nested inductive の phantom parameter。公理なしで False。#print axioms は何も報告しなかった
2026-07〜08 #14498 系 add_opaque のメタ変数/自由変数チェック欠落
2026-07-30〜08-20 カーネル4 + ランタイム2 Lean FRO × OpenAI の bug hunt。各々に実際の False の証明。v4.33.1 で修正

3週間の集中探索で数日に1件のペースで健全性バグが出た。そして nanoda / lean4lean / lean-inductive-models は偽の証明をすべて却下した — 独立チェッカ戦略が実際に機能した実測例。

判定：THEOREM 側は Lean 4 について未完、MEASURED 側は実在するが率が公表されていない。 前2回の「c がない」ではなく「c はあるが数値化されていない」。

2.2 native 評価層 — ここは本物の穴

2.3 sorry の層 — ほぼ閉じている、が1件の事故がある

3. 各分岐の判定

3.1 分岐 A（Lean5 = 基礎理論の置換）→ KILL

提案が存在しない。 FRO の4連続ロードマップ（Y1 2023 / Y3 2025 / Y4-1 2026-09〜2027-02）にカーネルまたは型理論の作業項目が一つもない。Y4-1 の内容は Verso、grind/bv_decide、Lean/Python FFI、そして lake check --paranoid（= 独立カーネルによる再検査）。信頼への投資先が「同じ理論の独立チェッカを増やす」方向に明確に振られている。

de Moura のカーネルバグ postmortem（2026-08-01）の総括は "an implementation bug, not a hole in Lean's meta-theory" / "The elaborator is untrusted by design"。設計上の後悔も基礎の再考も表明されていない。

そして Lean はこの実験を既に一度やって捨てている。 Lean 2 は proof-relevant な HoTT カーネルモードを持ち、ライブラリは約 30,400 行あった（Coq の HoTT ライブラリに匹敵）。Lean 3 で廃止。理由は VM の proof erasure と、equation compiler が axiom K を要求すること。

置換側の最強の論拠（公平に書く）：Abel & Coquand（LMCS 2020）は、非可述 Prop + 証明無関係の等式から発散項 Ω を実際に構成し、"The term Ω also serves as counterexample to normalization in the theorem prover Lean, version 3.4.2" と書いている。Carneiro の TYPES 2025 要旨も "the typing relation is undecidable and Lean underapproximates it, and reduction is not strongly normalizing" と認めている。そして Pujet & Tabareau の CCobs（POPL 2023）は非可述な strict proposition の宇宙を持ちながら正規化と変換の決定可能性を証明している — つまり Lean の看板機能を、決定不能性を払わずに得られることが示された。さらに LICS 2026（Felicissimo ら）が Acc × 証明無関係の残件を扱い Rocq 実装まで出している。

反論（こちらが強い）：Abel & Coquand 自身が "consistency and canonicity is not at stake" と書いている。壊れるのは「開いた項の等式を正規化で決定できる」ことであって、Lean が偽を証明することではない。Carneiro（Zulip）:

"Quotients in Prop are a red herring… The quotient of a Prop is not a thing people ever do." "Without proof irrelevance, it is hard to argue that your logic acts like classical mathematics, because subtypes don't act like subtypes anymore."

そして代替側は誰も百万行の古典数学ライブラリを運んだことがない。Cubical Agda は最も成熟した代替だがライブラリは自称 "experimental" で、閉じた整数項が簡約されずに 10〜20 GB のメモリを食う issue がある。CICobs の機械化されたメタ理論は ℕ のみをカバーし、スケーリングの主張をしていない。

決定的なのはリスクの形：Lean の 2026 年の実際の健全性事故は実装バグ（nested inductive の射影）であり、基礎の置換はこの種のバグを何も防がない。新実装は同種のバグを大量に再導入する。

3.2 分岐 B（Mathlib2）→ KILL

真剣な後継提案・モジュール化再設計・フォークは存在しない。 探して見つからなかった（不在証明ではない）。

規模（commit 534cf0b, 2026-02）：308,129 宣言 / 7,563 モジュール / 宣言依存辺 8.4M / import 辺 23,570。1.9M 行、約30名のメンテナ、開いた PR 約1,500〜2,600。

移植コストの上限値：mathlib3→4 は 3,112 ファイル（96.8%）/ 1,053,081 行（98.7%）、2023-07-16 完了宣言。集中的な人力移植期は約8ヶ月。移植ノートは 5,000 件超発生し、2025 年初頭でまだ約1,500件が未解決。自動翻訳（mathport）があってこれ。

構造批判は既にある（Li, Peng, Severini, Shafto 2026）：ファイル配置と名前空間は互いに一致する（NMI 0.71）が、論理的依存構造とは乖離する（NMI 0.34）。宣言依存の 50.9% が名前空間境界を越え、モジュール内に留まるのは 9.6% のみ。依存辺の 74.2% は合成されたもの（typeclass と coercion の elaboration が生成し、ソースには現れない）。import 利用率の中央値は 1.6%。

ただし monolith は integration を生む機構である。ℝ が距離空間であることが自動的に一様空間・位相空間であることを含意し、ライブラリ中の全定理が適用される — この合成的一般性こそ分断された生態系が持たないもの。分割提案は「その integration をどう保つか」を説明する義務を負う。

進行中の唯一の組織的手当ては Mathlib Initiative（Renaissance Philanthropy / Alex Gerko 資金、2025-07-24）で、D1 = レビュー遅延の職業的解消、D2 = 下流プロジェクト間のバージョン同期ツール。モジュール化も分割も統治変更も提案していない。

対照アーキテクチャの教訓：AFP は 1,029 entry / 608 著者 / 約 325,900 補題 / 約 543 万行を、査読付き・entry ごとバージョン管理で運用している。だが FSE 2024（Luan ら）が 21,000 超の theory / 約1,000万行を4リリース間で回帰テストし、12,079 件の互換性問題を検出、うち構文エラーの 37.7% 以上が Isabelle 標準ライブラリの変更に直接起因。分散化は破壊を消さず、移動させるだけ。

3.3 分岐 E（仕様層）→ SURVIVE

問題の形：カーネルは「この項はこの型に属する」を保証する。その型が意図した意味を持つか、環境が誠実に構築されたか、どこかの段階がカーネルの代わりにコンパイラを信頼したかは、すべて外側。

Paulson（2022）の言い方が最も簡潔：

"The most important concern is the correct formulation of the definitions and theorem statements: if they are wrong, the proofs mean nothing."

Buzzard（2026）は前提を明示し、それを人間に置いている：

"if humans are agreed that a Lean statement does faithfully capture the idea behind a conjecture, then checking that (possibly AI-generated) Lean code does comprise a proof or disproof of the conjecture is a triviality."

測定されている場所（ひどい数字）：

対象 測定結果 出典
miniF2F test 16.4% が誤りまたは欠落、59% が過度に単純化、5.3% が証明不能 miniF2F-Lean Revisited 2025
miniF2F validation 19.7% 誤り/欠落 同上
ProofNet 31.8% のエントリに形式化の誤り（→ ProofNet# として修正版） Poiroux ら 2024–25
FormalMATH Lean コンパイル通過 92.4% → 多 LLM 逆翻訳の意味検証が 60.7% を除去 → 31.7% FormalMATH 2025
VPU（verdict は合うが論理的に非同値） 950 中 260 件（約27%） Beyond Solver Verdicts 2026
miniF2F-test の statement 整合 15.2% が不整合 ProofGate 2026 △
横断監査 5 benchmark / 約10,000 問 → 4,833 findings、うち 398 が証明不能または空虚の機械可検証な証明書付き Ammanamanchi ら 2026

測定されていない場所：Mathlib と AFP。 メンテナンス論文 Growing Mathlib（2025）は非推奨化・ビルド速度・技術的負債・レビュー体制を論じ、数学的に誤った定義や命題の話を一切含まない。An Evaluation of the Archive of Formal Proofs（2021）は実際にはウェブサイトのユーザビリティ調査（SUS 72）。分母が存在しない。

そしてどの証明支援系も、健全性チェックを通すまで定義や定理を拒否しない。

現存する最強の実装：Anthropic の FLT ビルド。sorry なし / Lean 標準3公理のみ / 証明ごとの公理を「標準3つ + 宣言された子のみ」に閉じ込め / nanoda による独立カーネル再検査 / FRO の comparator で「証明した命題が Mathlib のみを参照する信頼済み challenge ファイルの命題と一致する」ことを確認 / そして Mathlib 自身の FermatLastTheorem を自分たちの定理から導出する。

最後の一手が要点：anchor-to-reference は「命題は正しいか」を機械可検証な定理に変換する。 信頼済みの錨が1つあればよい。ただしこのビルドも誤った命題の率を報告していない（「偽の補題が1回のレビューを通過し、別のレビューで捕まった」という逸話のみ）。

判定 SURVIVE。空白は2つ：

  1. 成熟した人手ライブラリ（Mathlib / AFP）に対する仕様忠実度の率が測られていない。 benchmark では測られている。人手で高価に書かれ、信頼の主張が最も大きい場所では測られていない。
  2. 健全性チェックを受理条件にした証明支援系が存在しない。

4. ★ STEP 1886 への警告 — prior art が今まさに埋まっている

分岐 D（TCB と証明書サイズの測定）は彼が既にいる場所だが、衝突する既存研究が出ている。

4.1 直接衝突の候補

Szeider, "LRAT-Catcher: Importing SAT Solver Certificates into Lean 4 by Reflection", arXiv:2607.00815（✓ abstract 直接確認）。単著。abstract verbatim:

"We present LRAT-Catcher, a standalone, general-purpose tool that imports a DIMACS formula together with an LRAT certificate into Lean 4 as a theorem. LRAT-Catcher runs the formally verified LRAT checker from Lean core as compiled native code via reflection. … We evaluate the tool against Mathlib's proof-term import and the external checker CAKE_LPR on establishing the Schur number S(4) = 44 and the Ramsey number R(4,4) = 18 as Lean theorems."

cake_lpr との比較測定を既にやっている。 STEP 1886 の compose baseline（cadical → drat-trim / frat-rs → cake_lpr → zstd -19）と対象が重なる。

4.1-bis 【★ CONFIRMED 2026-09-18】v2 の Table 2 + Table 5 実在確認 (Claude Code direct verify、 委託指示書 §3.1 対応)

元の報告（2026-09-18 起草時点、当時未確認、audit trail 保存）: 本 audit の調査過程で「v2（2026-09-07）は題名が "Streaming LRAT Certificates into Lean Theorems" に変わり、7つの proof-import 機構を『追加される信頼コード』『定理の公理』で分類する表と、証明書バイト数 / 解決 CPU / import CPU / 保持バイト数 / 公理リストを同一表の対等な列として報告する表を持つ」という報告を得た。

当時の裏取り状況（当時保存 / land 時点 stale）:

★ 2026-09-18 land 時 direct verify（Claude Code, rei-aios-76 tab、 arXiv https://arxiv.org/abs/2607.00815v2 + https://arxiv.org/html/2607.00815v2）:

未確認のまま保留（元報告の詳細のうち原文で verify できなかったもの）:

結論 revise (§4.1-bis の 判定 update):

4.1-ter ★ より重要：2026年に Lean 証明書取り込みの研究群が立ち上がっている

v2 の件より、同じ著者と周辺が2026年に同種の論文を連続して出していることのほうが STEP 1886 にとって重い。

Szeider, "PBLean: Pseudo-Boolean Proof Certificates for Lean 4", arXiv:2602.08692（✓ abstract 直接確認）。abstract verbatim の要点：

"In contrast to external verified checkers that produce verdicts, our integration yields Lean theorems that can serve as composable lemmas in larger formal developments. … This closes the trust gap between solver output and problem semantics since the constraint translation and its correctness proof are both formalized in Lean."

verdict と theorem を明示的に区別し、その差の対価を測っている：CAKEPB が Paley(101) を1秒未満で検査するのに対し PBLean は約200秒、約200倍のオーバーヘッドが「単独の verdict でなく合成可能な Lean 定理を得る」代金。

そして本 audit §2.2 に直撃する事実：PBLean の reflection は Lean.trustCompiler（コンパイル済みネイティブコードがカーネル評価と一致するという公理）に依拠する。つまりスケールのためにカーネル層の信頼を native 層の信頼と交換している — Mathlib が linter で禁止しているまさにその経路。論文自身が、この公理を回避する明示的 proof-term 構成は小規模インスタンスまでしかスケールしないと認めている。

同時期の隣接研究（題名のみ確認、内容未読 △）：

含意：「ソルバの証明書を Lean に取り込み、外部検証済みチェッカと比較し、信頼の対価を測る」という研究領域が 2026 年に急速に形成されている。STEP 1886 の compose baseline は、この群との差分を明示しない限り新規性を主張できない。v2 の有無にかかわらず、この節が反証条件 (a) の実質的な発火条件になる。

4.2 PIN 6（圧縮）への既存数値

Schur number five 論文（Heule 2018）が既に報告している（✓ 二次確認）:

"proof compression shrinks DRAT proofs of Schur number problems to approximately 45% of their size, while LRAT proofs are reduced to about 30% of their size."

理由も述べられている — DRAT は大きな数をほとんど含まないが LRAT はヒント索引という大きな数を含むので、LRAT の方がよく圧縮される。同論文は同じ含意証明について圧縮済み DRAT 0.88 PB vs 圧縮済み LRAT 2.18 PB（LRAT はバイト数で約2.5倍払って線形時間検査を買う）も出している。

STEP 1886 §5 の反証条件 (d)「zstd -19 が 30% 未満圧縮率」 は、この既存数値に照らすと発火しない見込みが高い（既存報告は 70% 圧縮）。反証条件としての識別力が弱い可能性がある。要再設計の検討対象。

4.3 TCB 測定の現状 — 空白は本物だが狭い

「複数パイプラインを横断して TCB を SLOC で測った公表研究はない。」 最も近いもの：

研究 何をしたか 限界
Wiedijk, Seventeen Provers（2006） 17 系の "small proof kernel (de Bruijn criterion)" 行 二値のチェックボックス。唯一の SLOC は Harrison 自己申告の HOL Light 433 行 OCaml
Monniaux & Boulmé, CompCert の TCB（ESOP 2022） 実在する TCB の最も丁寧な列挙 行数を出していない
cake_lpr Table 1（TACAS 2021） 4つの検証済み SAT チェッカを3軸で比較（"Unverified Extraction" vs "Binary Code Extraction" を含む） 順序尺度（+/−/×）であって数値でない
GRAT（Lammich, CADE 2017） 自己申告の実数値：形式化 約5k行 + 汎用 Isabelle ライブラリ 約3.5k行 + 未検証パーサ 40 LOC。C++ 生成器 約3k行は明示的に信頼外 単一システム

Lean 4 カーネルの SLOC は公表されていない。（調査中の実測値：commit 35485b87 の src/kernel/ が .cpp 5,753 + .h 2,275 = 8,028 行、src/util/ が 3,947 行。これは本 audit の wc -l であって引用可能な公表値ではない。）

なぜ空白が残るかの構造的理由：433行の OCaml カーネル、8k行の C++ カーネル、HOL4 形式化＋検証済みコンパイラバックエンド、stobj 実装を信頼することで速度を得る ACL2 チェッカ — これらの SLOC は通約不可能。cake_lpr の貢献はまさに信頼の種類を比較可能にした（machine code、extraction gap なし）ことであって、量ではない。横断 SLOC 表を書くには各系で恣意的な境界を引く必要があり、その恣意性は全員が知っている。

判定 CONFINE：空白は本物だが、「誰もやっていない」の理由が「通約不可能だから」である以上、新規性の主張は「測った」ではなく「この境界の引き方で測る、という宣言付きで測った」の形にしか立たない。これは差分候補 (ii)（申告義務）と同じ構造。

5. 最小形

新 arc は立てない。Mathlib に対する仕様忠実度の率を初めて測る1枚が最小。

理由：§3.3 の通り、benchmark では測られ Mathlib では測られていない。その非対称が空白の本体で、他のどの分岐より狭く、個人規模で、既存装置の流用で実行できる。

  1. §2 の層別4フィールド表をそのまま書く（Lean のどの層に c があってどの層に無いかの分離が、本 arc の主張の全体）
  2. 標本枠を宣言する。Mathlib 全体は不可能なので、decide / Fintype / Decidable が付いて plausible が走る範囲に限定する — これが Culik–Yu 的な制約の Lean 版（前回 audit §4 と同じ形）
  3. 既存装置を3つ流用する：
    • anchor-to-reference（Anthropic FLT ビルドの手法）— 独立に書かれた同値命題を導出できるか
    • 反例探索（plausible、Isabelle 側なら nitpick）— 定義が空虚でないか
    • refusal-until-declared（STEP 1894 の機構）— 公理フットプリントと副情報が未申告なら判定を拒む
  4. 各命題に対して verdict を出し、率を報告する。benchmark 側の 16.4% / 31.8% / 27% と同じ単位で並べられる数字を、人手ライブラリについて初めて出す
  5. 反証条件を事前登録（§6）

compose baseline：plausible + #print axioms + comparator を素朴に順に走らせたもの。これで率が出てしまうなら Pattern 5 で KILL。

6. 反証条件（事前登録）

# 条件 発火時の処置
(a) 2026年の Lean 証明書取り込み群（LRAT-Catcher v1 / v2 "Streaming LRAT Certificates into Lean Theorems" ✓ direct verify 2026-09-18 §4.1-bis / PBLean / LeanCSP / Kochen–Specker 等）との差分が明示できない。v2 Table 2 (trusted code added 列) + Table 5 (certificate/solve CPU/import CPU/retained/axioms 5 列) が 先行 evidence として 実在確認済 → STEP 1886 の TCB 定義 + 時間測定 新規性主張 に 直接影響 分岐 D を KILL。STEP 1886 §1・§4 の新規性主張を撤回し、追試または差分測定に位置づけ直す
(b) Mathlib / AFP に対する仕様忠実度の率を測った既存研究が1件でも出る 分岐 E を KILL
(c) plausible + #print axioms + comparator の素朴な合成で率が出る 最小形を KILL（Pattern 5）
(d) 標本枠（Decidable が付く範囲）が Mathlib の代表になっていない 率の主張を標本枠内に限定。外挿は禁止（前回 audit の Culik–Yu 制約と同型）
(e) STEP 1886 の反証条件 (d)（zstd -19 が 30% 未満圧縮率）が Schur 論文の既存数値と識別力を持たない 反証条件 (d) を再設計。「既存報告（LRAT が元の約30%）と有意に異なるか」の形に変える
(f) 「Lean を超える」という語が、§2 の層別表以外の根拠で使われている 語を撤回。「Lean が保証していない層の測定」に降格

恒久禁止事項（Pattern L 予防）：

7. 引用一覧

✓ = 本 audit で直接 fetch し確認 / △ = 二次情報・要確認

直接確認 ✓

二次情報・要確認 △

8. この audit の限界