証明パイプライン装置マップ
Device map / prior-art audit

証明パイプライン装置マップ

「全ての未解決問題を証明する装置」を 7 段のピンに分解し、各ピンに既存研究を当てて生存判定をつけたもの。装置・チップ・回路・端子・マシンの提案は、必ずこの 7 ピンのどれかに刺さる。刺さらない提案は用途が定まっていない兆候。

日付 2026-09-07 判定規約 KILL / CONFINE / SURVIVE 手持ち資源 Tang Nano 9K, Tang Console 状態 draft v0 — 各判定は要再audit

§0先に引く線

「全ての未解決問題を証明する装置」は原理的に存在しない。根拠は三つ。

  • 不完全性 — 帰納的に公理化された体系では、真だが証明できない算術命題が残る。
  • 決定不能性 — ヒルベルト第 10 問題、停止性、群の語の問題。一様な判定手続きが存在しない。
  • 独立性 — 連続体仮説など。公理の側を拡張しない限り決着しない。

ただし重要な非対称がある。RH・Goldbach・Collatz などの個別問題は、どれも決定不能と証明されてはいない。障害は原理ではなく探索空間である。したがって「一様な全能機械」は不可能だが、「個別問題への装置」は正当な工学対象になる。設計目標はこう書き換わる。

目標:人間+機械の証明パイプラインの単位時間あたり通過量を上げること。および、不可能な領域を装置の外側として明示的に切り分けること。

判定の凡例

KILL既存研究が同じ場所を押さえている。新規性を主張しない。既存物を使う。
CONFINE汎用形では死んでいるが、範囲を狭めれば生きる。狭めた範囲を明記する。
SURVIVE既存研究の射程外。ただし fragile — compose baseline との差分測定が前提。

§1ピン配置

左端の色帯は信頼等級。■ oracle 側は証明書を出せないノード(出力は「予想」以上に昇格させない)、■ certificate 側は出力に機械検査可能な証明書が付くノード。PIN 5 が信頼の基点で、ここより上流の全ての誤りはここで止まるべきという設計になっている。

ORACLE ZONE — 証明書なし / 出力は予想タグ止まり
PIN段ボトルネックの正体判定
1形式化自然言語 → 形式言語。意味の橋渡しが人手KILL
2予想生成候補空間。何を証明しに行くかの選択CONFINE
CERTIFICATE ZONE — 全ての辺に証明書が流れる
3反例掃討帯域と時間。有限化定理が先に要るCONFINE
4証明探索不規則メモリアクセス。memory-boundKILL
5検査信頼の基点(TCB)の大きさSURVIVE
6圧縮・可読化証明物が巨大。側情報の計上規約がないSURVIVE
7統合(端子)体系間の非互換。翻訳の健全性CONFINE

§2各ピンの監査

PIN 1

形式化

KILL
装置の型
マシン(自動形式化機)。往復意味検査つきの NL→Lean 変換。
Prior art
2026 時点で最も混雑している領域。長時間 horizon の Lean 自動形式化(LeanMarathon)、研究数学向け agentic 形式化フレームワークが既に走っている。
判定理由
装置としての新規性が取れない。かつ計算資源で押す領域なので、個人規模の不利が最大化する場所。
生き残る範囲
汎用は放棄。自分固有の記法(D-FUMT₈、ZCE の BNF と 4 口座)の形式化に限れば、そもそも他者が手をつけない。ここは装置ではなく自分の Lean4 作業として続く。
compose
baseline
既存の LLM + Lean の #check ループ。これ以上を主張するなら差分を測る。
PIN 2

予想生成

CONFINE
装置の型
ツール(整数関係検出:PSLQ / LLL)、マシン(OEIS・グラフ探索)。チップ化の余地は LLL の格子簡約アクセラレータに一応ある。
Prior art
Ramanujan Machine が基本定数の連分数予想生成で Nature 2021、後継の Ramanujan Library が整数関係のハイパーグラフ上の自動探索まで到達している。グラフ理論側は Graffiti 系。
判定理由
汎用予想生成機は押さえられている。ただし「どの対象の予想を生成するか」は各自の理論に依存するので、対象を絞れば道具として素直に使える。
生き残る範囲
ZCE の 3 不等式の族、D-FUMT₈ の不動点・完全性まわりなど、自分の体系の中で候補命題を列挙する用途に限定。ここで出たものは全て「予想」タグのまま PIN 5 に渡す。
compose
baseline
mpmath + PSLQ + SymPy を素直に繋いだスクリプト。装置を名乗るならこれとの差分。
PIN 3

反例掃討

CONFINE
装置の型
チップ/回路(剰余算アレイ、多倍長 Montgomery 乗算器、NTT)+マシン(分散掃討)。
Prior art
Collatz は GPU 実装で 268 級まで検証済み(さらに上限を伸ばす報告あり)、Goldbach は GPU 加速の公開フレームワークが 2026 に出ている。ハードウェア側は ZK 証明向けの NTT/MSM アクセラレータ(TCHES 2024–2025、FPGA / AI ASIC 転用)が既に高度に最適化された多倍長演算器を提供している。
原理的制約
無限領域の掃討は証明にならない。装置が証明を出せるのは、先に人間側が有限化定理を出した場合だけ(四色定理の 1476 配置、ケプラー予想の LP 化、Boolean Pythagorean triples)。「有限化 → 掃討 → 証明書 → 検査」の順を崩すと機械は何も証明しない。
生き残る範囲
演算器を自作するのは KILL(ZK ハードに完敗する)。生き残るのは掃討の被覆台帳に証明書を付ける部分——範囲分割が全域を漏れなく覆ったことを機械検査可能にする層。ここは意外と整備されていない。
compose
baseline
GMP + CUDA + シャード管理スクリプト。差分は「被覆の完全性が検査可能か」の一点に限る。
PIN 4

証明探索

KILL
装置の型
チップ/回路(CDCL・BCP アクセラレータ、E-graph 合同閉包用の連想メモリ)。
Prior art
FPGA による SAT 加速は 30 年近い蓄積があり、サーベイも出ている。近年も BCP 加速(2024)、現代的 CDCL を FPGA に載せた SAT-Accel(FPGA'25)がある。E-graph 側は egg 以降ソフトウェアで進んでおり、専用ハードは未開拓。
判定理由
本質が memory-bound かつ不規則。学習節データベースが動的に膨張するため、小規模 FPGA には構造的に載らない。E-graph ハードが未開拓なのは「誰もやっていない」ではなく「アクセスパターンが最悪」だからである可能性が高い。
生き残る範囲
手持ち規模では無し。この段はソフトウェア(CaDiCaL / Z3 / cvc5)を使う側に回る。
compose
baseline
該当なし。既存ソルバがそのまま baseline かつ結論。
PIN 5

検査

SURVIVE
装置の型
回路(証明書検査ループの固定回路化)+ 装置(TCB を最小化した検査コア)。
Prior art
ソフトウェア側は決着している。cake_lpr が CakeML 上で LRAT / LPR 検査器を形式検証済みで、SAT Competition の公式チェッカとして使われている。ハードウェア側は FPGA/HMC による resolution proof checking の研究(2018)があるが、その後の展開が薄い。
なぜ生きるか
探索と検査で計算の性質が逆転する。探索は不規則・状態が巨大で FPGA に不向きだが、検査は規則的・状態が小さく・逐次ストリームで FPGA 向き。「探索はソフトウェア、検査はハードウェア」という分割は、この非対称から出てくる。
測る量
速度ではない。①検査行数/ジュール ②TCB の行数(信頼しなければならないコードの量)。後者は規模と無関係な軸なので、個人でも正面から勝負できる。
compose
baseline
cadical → drat-trim → cake_lpr をそのまま繋いだときの検査時間・消費電力・TCB 行数。FPGA 版はこれと同じ証明書を入力にして比較する。
PIN 6

圧縮・可読化

SURVIVE
装置の型
ツール/マシン(証明圧縮器)。既存の超圧縮・ZCE 資産と直結する唯一の段。
Prior art
Boolean Pythagorean triples の証明は 200 TB 級で、この段が実在の問題であることの証拠になっている。形式面では FRAT が solver と elaborator の間の通信形式として既に「圧縮」の役割の一部を果たしており、DRAT/LRAT の trim・elaborate も同様。汎用圧縮器(zstd, brotli)が最終段に噛むのも既定。
なぜ生きるか
証明書は受信側が既に持っている構造が厳密に定義できる、稀な題材である。検査器は節データベースと伝播規則を保持しているので、ZCE でいう Ctx 口座(受信側が既に保持する構造)が推測ではなく仕様として書ける。過去記事で計上漏れになっていた側情報が、ここでは定義から一意に決まる。
fragile な点
FRAT / LRAT elaboration が既に構造的冗長性の除去を担っているため、汎用圧縮率の勝負にすると差分が消える可能性が高い。主張範囲は「圧縮率」ではなく「検査器側既知構造の明示的計上」という会計の側に置くのが安全。
compose
baseline
cadical → frat-rs / drat-trim → zstd -19 のバイト数と検査時間。ZCE 系はこれを下回るのではなく、同じバイト数を 4 口座に分解して見せることが成果物になる。
PIN 7

統合(端子・コネクタ)

CONFINE
装置の型
端子規格+コネクタ。回路のピン配置に相当するのは証明証明書のフォーマット:SAT なら DRAT/LRAT/FRAT、SMT なら Alethe/LFSC、ATP なら TPTP/TSTP、体系間翻訳なら Dedukti。
Prior art
体系間相互運用は Dedukti / Lambdapi と EuroProofNet が本流で、Lean → Dedukti の翻訳は 2026 の博士論文まで出ている。ATP を束ねる側も Sledgehammer / CoqHammer / aesop が既に済ませている。
判定理由
汎用の「証明システム相互運用バス」は KILL。ここに新規性を主張してはいけない。
生き残る範囲
Dedukti の射程は論理体系どうしの翻訳である。射程外なのは非 ATP ノード——数値実測、CAS、計測装置、データベース——を同じ証明書規約に載せる部分。benchtop の計測系と rei-aios の MCP 群を、健全性等級つきのノードとして同じバスに繋ぐ構想はここに入る。
設計の核
すべての辺に証明書を流す。証明書を出せないノードは oracle として型で隔離し、その出力は「予想」タグ以上に昇格させない。CAS も LLM も計測器も、現状すべて oracle 側である。
compose
baseline
MCP のツール呼び出しをそのまま並べたもの。差分は「辺に証明書型があるか」「oracle 出力の昇格が構文的に禁止されているか」の 2 点だけ。

§3物理限界からの見積り

300 K の Landauer 限界は kT ln2 ≈ 2.871×10⁻²¹ J/bit。不可逆ビット演算 2n 回に必要な最小エネルギーは以下(実機はこの 108–1010 倍を消費するので、あくまで下限)。

結論:数学の探索的攻撃はエネルギー壁のはるか手前にある。律速はメモリ帯域と、人間側の有限化・形式化の時間である。「チップを作れば解ける」という筋が弱いことの定量的な理由。
探索規模最小エネルギー人間スケールでの比較該当する実績
2680.85 J単三電池 1 本の 1 万分の 1Collatz 検証の到達点
2803.5×10³ Jノート PC 数分ぶん—
21003.6×10⁹ J約 1,000 kWh(一般家庭の数か月)—
21289.8×10¹⁷ J日本の年間電力消費と同オーダー暗号の安全域
21604.2×10²⁷ J世界の年間一次エネルギーの 10⁷ 倍実質的な壁
22563.3×10⁵⁶ J太陽の年間放射の 10²² 倍不可能

量子計算を入れても構図は変わらない。Grover は非構造探索を二次加速するだけなので 2160 が 280 になるが、決定不能な問題は決定可能にならない。量子が効くのは周期発見に帰着する数論計算(因数分解、類群計算など)という狭い切片で、証明探索一般ではない。

§4手持ち資源での射程

Tang Nano 9K は約 8.6K LUT・0.5 Mb BSRAM 級。CDCL の学習節データベースは載らないので、PIN 4 の方向は最初から閉じている。Tang Console でも桁が変わるだけで、性質は同じ。

開くのは PIN 5 の方向だけである。LRAT の逐次検査ループは、状態が小さく・規則的・ストリーム処理なので、この規模でも1 カーネルの demonstrator として成立する。作るべきものは「速い検査器」ではなく、検査行数/ジュールとTCB 行数を測るための小さな実機である。

ASIC は検討しない。fab へのアクセスも量産理由もない。FPGA で測れる量(電力効率と TCB サイズ)だけが、規模で負けている側から出せる主張である。

§5推奨経路

SURVIVE が立っているのは PIN 5・6 と、PIN 7 の非 ATP ノード部分のみ。着手順はこうなる。

  1. compose baseline を先に測る。cadical → drat-trim / frat-rs → cake_lpr と zstd -19 を素直に繋ぎ、証明書バイト数・検査時間・TCB 行数を記録する。これを測る前に新機構の設計に入らない(Pattern 5 予防)。
  2. LRAT における Ctx 口座を仕様として書く。検査器が入力なしに保持している構造(節データベース、伝播規則、番号空間)を列挙し、ZCE の 4 口座に写す。ここが過去記事の側情報計上漏れを構造的に潰せる唯一の題材である。
  3. 測定プロトコルを先に凍結する。STEP 1766 の方式に倣い、反証条件を先に書く。証明書圧縮は「圧縮率で勝つ」ではなく「口座分解が保存則を満たす」で判定する。
  4. FPGA は最後。検査ループのみの demonstrator。速度比較はせず、ジュールあたり検査行数と TCB 行数だけを報告する。
  5. PIN 7 は規約だけ書いて実装は後。oracle ノードの昇格禁止を型で表現する最小規約を 1 枚の spec にする。バス実装は SURVIVE が確認できてから。

§6主張してはいけないこと

この領域は「世界初」が出やすく、そのほとんどが既に存在する。以下は本マップの時点で明示的に禁止する。