Lean 検証一式 — 機械検査の一覧
このサイトの自然哲学の記事で Lean の札が付いた主張は、Lean 4 + Mathlib で機械検査されています。ソース一式をここから取り、手元で建て直せます。束は一つで、主題ごとの名前空間に分かれています。
関連：Lean の説明（機械検査とは何か・確かめ方の手順）／論文／新規性の棚卸し／残っていること／ロヴァース予想の証明書
01
配布物
| ファイル | principia-src-2026-10-01.tar.gz（約 2.1 MB・2026-10-01 版） |
| sha256 | 21f9bfedae37266e3f0845b092967c9d8b1166803cdd7f7a3d58b0a0cc8549ae（.sha256） |
| 公理ログ | axioms-principia.txt——全モジュールの #print axioms の出力（3,149 行） |
| 中身 | パッケージ principia。Principia/<主題>/*.lean 225 本、入口 Principia.lean、lakefile.lean、lake-manifest.json（依存の固定）、lean-toolchain、README.md |
| 環境 | Lean 4（leanprover/lean4:v4.33.1）＋ Mathlib（manifest で固定）。RAM は 16 GB を見込み、一本ずつ建てる（1 本で 11.8 GiB を kernel に閉じさせるものがある） |
| 範囲 | エルデシュ #169・コラッツ・単位距離グラフとハドヴィガー・ネルソン・エルデシュ #827・欠損 2 の三価二部グラフ・GP(n,3)（下の台帳） |
一つ前の版 principia-src.tar.gz（sha256 131d8da3426838ca…、2026-09-25 版）は、論文やフォーラムの投稿が引いているので、URL と sha256 を変えずにそのまま置いてあります。新しい版はその上に欠損 2 と GP(n,3) を足したもので、既存のモジュールは同じです。過去に配った束は、URL と sha256 を変えずにそのまま置いてあります。定理の中身はこの束と同じで、違うのは名前空間とファイル名だけです。新しく確かめるときはこの束をお使いください。
記事ごとの束
記事や論文ごとに、その主題のモジュールだけを詰めた束です。lakefile.lean・lake-manifest.json・lean-toolchain は上の束と同じ環境を指し、.lean は同一のファイルです。公理ログ（axioms-<束>.txt）は各束の中にあります。
| 束 | 記事・論文 | 本 | 公理の行 | sha256 |
|---|---|---|---|---|
principia-riemann-weil-form-2026-10-02.tar.gz（.sha256） | Weil の二次形式の沈んだ固有値 | 12 | 73 | 3885b22242d70dbef24aaebbdb3cfbdec98b1eb4be517ddc0d6424378d9c9d5e |
principia-hodge-cm-degenerate-2026-10-02c.tar.gz（.sha256） | ホッジ予想 | 46 | 945 | 10b941a3ee8c4ffa882fc6705b43813417eea61eed3e2d0eec546dc17be66be7 |
principia-generalized-petersen-2026-10-02.tar.gz（.sha256） | 論文 — GP(n,3) のハミルトン閉路の個数 | 7 | 185 | c0dd6e4cea403caf01c3ae9fd6c4e329eb54957e93e0c87e3d884056f3c72b84 |
principia-gap-bridge-2026-10-09.tar.gz（.sha256） | 論文 — 片側の橋（独立な lake プロジェクト EuclideanPath.GapBridge） | 1 | 17 | 5f3d288d93ba456721aead52fee953950c9618de4637775e1cad3d2fbe13d841 |
principia-padic-regulator-valuation-2026-10-09b.tar.gz（.sha256） | 論文 — p 進高さ対の整性・p 進 BSD（独立な lake プロジェクト。入口は何も import せず、31 本を個別に建てる） | 31 | 360 | f12364292c008567ddab7e21f97b92679e3cfd4b9bdcb3e7986bdf97f946e017 |
principia-ym-slab-containers-2026-10-15.tar.gz（.sha256） | 教科書 12-03・12-04（板と容器。独立な lake プロジェクト ymslabcontainers、lib Y6。Lemma5Core.lean は lib の外で別に検査） | 31 | 150 | 4892aca93897af4940828fd14d5fc45ee72bdcfca0914a2dcd20dd2d77229341 |
principia-ym-insertion-identities-2026-10-15.tar.gz（.sha256） | 教科書 12-05〜13-05（挿入の恒等式ほか。独立な lake プロジェクト yminsertion、lib Y7） | 11 | 32 | 58d60c433cb23cb9cfab1f2299732385f79a362b96a1d49ac109334b4832bdf8 |
principia-ym-flux-network-blocking-2026-10-15.tar.gz（.sha256・公理の記録） | 論文「束の網のブロック化」（WEB 版）・教科書 15-05。単体の .lean の束（lake プロジェクトでなく shioriproofs の環境で一本ずつ lake env lean）。本体と燐の独立の再検査（2026-10-15） | 12 | 78 | 334e0149fc449274189004a8085837364da5d8849fe23d08149458461a7d3ce3 |
principia-ym-hierarchical-chain-2026-10-15.tar.gz（.sha256・公理の記録） | 論文「階層模型の鎖」（WEB 版）・教科書 15-04。単体の .lean の束（lake プロジェクトでなく shioriproofs の環境で一本ずつ lake env lean）。本体と燐の独立の再検査（2026-10-15） | 5 | 44 | d549fd8969bd4ec348e09020ceff836a250ca45355deaaf00525f56dcfd33da5 |
principia-ym-one-row-renormalisation-2026-10-15.tar.gz（.sha256・公理の記録） | 論文「一列四枚の繰り込み模型」（WEB 版）・教科書 15-06。単体の .lean の束（lake プロジェクトでなく shioriproofs の環境で一本ずつ lake env lean）。本体と燐の独立の再検査（2026-10-15） | 7 | 61 | e8841482e8925d18bfdcfd152128a21ab5747563103fe8c3f64c5fcf2c3b964c |
principia-ym-weak-uv-chain-2026-10-30.tar.gz（.sha256・公理の記録） | 論文「条件つきの定理：小さな箱の四次元 SU(2) 格子ヤン–ミルズの弱い紫外の存在、段ごとの前提からの機械検査の鎖」。単体の .lean の束（lake env lean）。本体と燐の独立の再検査（2026-10-30） | 64 | 1403 | 69976db4756e390cff99afa8f0139f9588602f2291e19a154280f58a4db89ef8 |
principia-ym-face-sum-rule-2026-10-30.tar.gz（.sha256・公理の記録） | 論文「一面の Schwinger–Dyson の恒等式と粗い剛さの多段の和則」。単体の .lean の束。本体と燐の独立の再検査（2026-10-30） | 6 | 64 | f7839e8d56d28c6209dc3ac2e28c2d887f085c1abf62cddc0312dc8a772519a9 |
principia-ym-two-colour-polymer-2026-10-30.tar.gz（.sha256・公理の記録） | 論文「ℤ⁴ 上の二色のポリマー気体の機械検査」。単体の .lean の束。本体と燐の独立の再検査（2026-10-30） | 13 | 518 | d38990299a293d9a728cbdf0d709775448223d5e9708966519394b64617541e8 |
principia-ym-boundary-mixed-derivative-2026-10-29.tar.gz（.sha256・公理の記録） | 論文「境界の混合微分の一段の量（U(1) と SU(2) を分ける）」・教科書 14-02 の ⑦σ′。単体の .lean の束（shioriproofs の環境で lake env lean）。本体と燐の独立の再検査（2026-10-29） | 1 | 9 | 45e3a553a0d89bbe84a70d4223e8cef3d65c91253cb2f1a0335bb36a9222d8a9 |
principia-ym-h1b-margin-interval-2026-10-29.tar.gz（.sha256・公理の記録） | 論文「(T1) の余白の区間演算の証明書（ħ ∈ [0.001949, 0.005]）」・教科書 10-15 の [014]。単体の .lean の束。本体と燐の独立の再検査（2026-10-29） | 1 | 15 | 7d0c0505e62084fb2013004945f9ab88b4d5327d16149e73c07b55c599165eb8 |
principia-ym-coarse-chain-poincare-2026-10-15.tar.gz（.sha256・公理の記録） | 論文「粗い鎖の Poincaré（第 10 部の壁）」・教科書 10-12。単体の .lean の束（lake プロジェクトでなく shioriproofs の環境で一本ずつ lake env lean）。本体と燐の独立の再検査（2026-10-15、追加の二本は 2026-10-17） | 9 | 75 | 1f08167b488c302824fe50f03e538aabadb3930a3ba344028c5b7c375a3c6b8d |
principia-ym-fractional-instanton-rate-2026-10-15.tar.gz（.sha256・公理の記録） | 論文「分数インスタントンの率（草稿）」（WEB 版）・教科書 12-02。単体の .lean の束（lake プロジェクトでなく shioriproofs の環境で一本ずつ lake env lean）。本体と燐の独立の再検査（2026-10-15） | 1 | 5 | dce68445244dde3ba7fda677c7dafe7c7abfd5f67422860a976c0ca4ae055bb7 |
GP(n,3) の 2026-10-01 版の束（sha256 45b896c0…）は、入口 Principia.lean の import の接頭辞が二重になっていて lake build が通りません（各モジュールを名指しで建てることはできます）。URL は変えずにそのまま置き、.lean が同一で入口だけを直した 2026-10-02 版を上に載せています。
02
確かめ方
tar -xzf principia-src-2026-10-01.tar.gz cd principia lake exe cache get # Mathlib のビルド済みキャッシュ LEAN_NUM_THREADS=1 lake build Principia
Principia.lean は全モジュールを import するだけの入口です。並列数は 1 に絞ってください。証明の中に、1 本で数 GB から 12 GiB の計算を kernel に閉じさせるものがあります。lake の既定は CPU の数だけ同時に建てるので、RAM 16 GB の機体でも 4 本同時ではスワップに落ちます。lake は済んだところから続きを積みます。
一本だけ建て直すときは、そのモジュールを名指しします。
LEAN_NUM_THREADS=1 lake build Principia.APFree.BellmanRecord
各モジュールの末尾に、そのモジュールが宣言した主な定理の #print axioms が置いてあります。建てると各定理が依拠する公理がそのまま出力されます。[propext, Classical.choice, Quot.sound] は Lean / Mathlib の標準 3 公理で、sorryAx（未証明の穴）も native_decide が足す公理も 1 件も出ません。束に同梱の axioms-principia.txt が、こちらで建てたときの全出力です。読み方の詳しい手順は Lean の説明 09 に。
03
台帳 — 主題ごとに、何が入っているか
名前空間ごとに、本数・主な定理とその所在・公理の状態・元の記事です。定理の正式名は <名前空間>.<定理名>、所在は束の中のファイルと行です。全モジュールの一覧と各ファイルの sha256 は束の README.md にあります。
| 主題 | 名前空間 | 本 | 主な定理（所在）と言明 | 公理 | 記事 |
|---|---|---|---|---|---|
| エルデシュ問題 #169 3-AP／4-AP を含まない集合の逆数和 | APFree | 64 | APFree.BellmanRecord.erdos169_lower_record_939（Principia/APFree/BellmanRecord.lean:93）——3-AP を含まない有限集合で逆数和 > 3.0085385（1984 年の記録 3.00849 を超える）APFree.FourTermRecord.setA4_apfree_and_beats_walker（FourTermRecord.lean:55）——4-AP を含まない集合で逆数和 > 4.439753369254541（Walker の記録を超える）／APFree.FourTermRecord.setA4_lower（FourTermLower.lean）——同じ集合で > 4.439753474215620APFree.Nesting.lemma2_four（Nesting.lean:374）——k=4 の入れ子補題 | 標準 3 公理の部分集合（kernel の計算だけの定理は「公理なし」） | エルデシュ等差数列予想 |
| コラッツ予想 臨界の乗数・測度・階段の高さ・枝の生死・禁止語 | Collatz | 7 | Collatz.CriticalMultiplier.qcrit_not_int_of_three_le（Principia/Collatz/CriticalMultiplier.lean:44）——臨界の乗数 qcrit(p) が整数になるのは p = 2 だけCollatz.SubtractionSteps.min_over_six_classes（SubtractionSteps.lean:94）／Collatz.LadderHeight.syracuse_sign_conjugation（LadderHeight.lean:139）——1/3 の符号の不等式 3·log₂3 < 5 とそこから出る禁止語 | 標準 3 公理の部分集合 | コラッツ予想／符号が一つ違う |
| 単位距離グラフ・ハドヴィガー・ネルソン問題 候補類の非実現と下界の証人 | UnitDistance・HadwigerNelson | 42＋1 | HadwigerNelson.Witness.fGe_10_3（Principia/HadwigerNelson/LowerBound.lean:405）／fGe_14_4（:770）——f(3) ≥ 10・f(4) ≥ 14 の証人UnitDistance.Order11.no_realization（Principia/UnitDistance/Order11.lean:2563）／UnitDistance.Order16.no_realization（Order16Main.lean:45）——候補類が平面に置けないこと | 標準 3 公理の部分集合 | ハドヴィガー・ネルソン問題 |
| エルデシュ問題 #827 外接半径の相異なる 4 点・n₄ = 7 | DistinctCircumradii | 100 | DistinctCircumradii.sInf_isGood_eq_seven（Principia/DistinctCircumradii/Final.lean:92）——主定理 sInf {N | IsGood N} = 7DistinctCircumradii.censusComplete（Census/Tree373.lean:234）——悪い 6 点の証人集合は 35 類で尽きる／DistinctCircumradii.restUnrealizable（Final.lean:40）——34 類は実現しない／DistinctCircumradii.not_isGood_six（SixPoints.lean:478）——下界 | 標準 3 公理の部分集合 | 外接半径の相異なる四点／論文 |
| 周長欠損 2 の三価二部グラフ 30 頂点・非ハミルトン | CubicBipartite | 2 | CubicBipartite.ClassI.G30_def2・CubicBipartite.Search.G30b_def2・G30c_def2（Principia/CubicBipartite/Gap2.lean）——30 頂点・三価・二部・連結・長さ 28 の閉路あり・全閉路 ≤ 28・非ハミルトン（3 類）／CubicBipartite.Search.G20_def6——20 頂点・周長 14・非ハミルトン。建てるときは lake build Principia.CubicBipartite.Chk | 標準 3 公理の部分集合 | 論文 |
| GP(n,3) のハミルトン閉路の個数 奇数 n で n が割り切る | GeneralizedPetersen | 7 | GeneralizedPetersen.Descent.gp3_dvd_hc_odd（Principia/GeneralizedPetersen/Descent.lean）——奇数 n ≥ 7 で n ∣ #HC(GP(n,3))（仮定なし）／GeneralizedPetersen.FreeAction.GP{7,9,11,13,15}_dvd_rot——回転の自由作用。建てるときは lake build Principia.GeneralizedPetersen.Chk | 標準 3 公理の部分集合 | 論文 |
| リーマン予想 — Weil の二次形式 時間帯の跡・移送・沈んだ固有値の本数 | TimeBand・SunkCount・BandSplit・HodgeIndex ほか | 12 | TimeBand.binom_oddH_identity（Principia/RiemannWeilForm/TimeBandTrace3.lean）——組合せ恒等式 Σn≥1 C(k,2n) On = 2k−2 Hk−1、すべての k ≥ 1。ほかは定理 A の有限次元の部品（全 73 本は束の公理ログ） | 全 73 本が標準 3 公理ちょうど | Weil の二次形式の沈んだ固有値（記事ごとの束） |
| ホッジ予想 例外類と ξ・因子の枝・割線層の側の有限の算術・模型の境目 | CMHodge | 46 | CMHodge.card_deg_prim・CMHodge.weight_ge_three・CMHodge.Texc_card・CMHodge.count31_eq——ホッジ類が CM 型の組合せに落ちること、退化の重み ≥ 3、余次元 3 の例外類が 6 個、H⁴(A×E) の 51 次元。四群の内訳は記事の §10 | 標準 3 公理の部分集合（sorryAx 0） | ホッジ予想（記事ごとの束） |
04
準備中の束
上の束の外で機械検査が済んでいる定理です。束にして配る準備をしています——配布 URL と sha256 は、置いた時点でここに書きます。論文の草稿は論文の頁に。
| 束 | 主定理と言明 | 配布 |
|---|---|---|
| 格子ヤン–ミルズ・一リンク積分 | LatticeGaugeOneLink.*・PerfectFamily.*・PlaquetteCounting.*・TriangularLattice.*——完全な族は d ≤ 4 に限る・密度 ≤ 1/d・ヘッセ行列の下界 | 準備中 |
| p 進高さ対の整性 | PadicHeightValuation*——高さの分解・Fermat 商・線形代数の段 | 上の表の principia-padic-regulator-valuation-2026-10-09b.tar.gz（2026-10-09） |
これらは証明を書いた機体（RAM 15 GiB）でしか建てていません。一つずつ建てること。最大 RSS は約 11.8 GiB（GP(n,3) の数え上げ）、欠損 2 の束で約 10 GiB です。
05
再実行の記録
§01 の束は、225 本すべてを依存の順に一本ずつ建て直して作りました（2026-10-01 版は欠損 2 と GP(n,3) の 9 本を足したもの）。
- エラー 0 件・
sorry0 件・native_decide0 件 - 公理の出力は 3,149 行。全行が標準 3 公理の部分集合
- 名前空間を付け替える前の版の公理の出力と、宣言名・公理ともに集合として一致
- コメントを剥がした本文は、付け替え前の版と
import行を除いて一字一句同じ - #827 の 100 本は、原本から独立に組み直した版でも再検査済み
同一の機体上での再実行であり、ハードウェアをまたいだ追試ではありません。別環境での追試はまさにこの配布の目的です——結果が食い違ったら、お問い合わせから知らせてください。
2026-10-02 — 配布した束からの建て直し
配布している束を、証明を書いた作業木とは別の新しいディレクトリに展開し、束の中身だけから建てました。手順は lake exe cache get のあと LEAN_NUM_THREADS=1 lake build。各束の #print axioms の出力を、束に同梱した公理ログと一行ずつ突き合わせています。
principia-riemann-weil-form-2026-10-02——12 本、エラー 0、公理の出力 73 行が同梱のログと一致principia-generalized-petersen-2026-10-02——7 本、エラー 0、公理の出力 185 行が同梱のログと一致principia-hodge-cm-degenerate-2026-10-02（最初の版）——46 本すべてが建ち、公理の出力 945 行が同梱のログと一致。ただし入口Principia.leanの読み込みで、CMHodgeClassesとCMHodgeDegenerateの自動生成のインスタンス名が衝突して止まった。配布している c 版は、この一本を入口から外したもの（モジュールの中身は同じ）principia-src-2026-10-01（上の束）——223 本、エラー 0、公理の出力 3,110 行がaxioms-principia.txtと一致。約 10 時間principia-hodge-cm-degenerate-2026-10-02c（配布している版）——46 本すべてと入口が建ち、エラー 0、公理の出力 945 行が同梱のログと一致
建てたのは、証明を書いたのと同じノート PC です（このサイトのサーバはメモリが足りません）。配布物からの建て直しではありますが、ハードウェアをまたいだ追試ではありません。
06
何が機械検査で、何がそうでないか
| 主張 | Lean の中 | Lean の外 |
|---|---|---|
| #169・k=3 の記録 3.0085385 | 集合が 3-AP-free で逆数和が 3.0085385 を超えること・1984 年の記録 3.00849 を超えること（一つの定理） | 1984 年の論文の「3.00849」の読み（切り捨てか丸めか・どの集合か） |
| #169・k=4 の記録 4.4397534742 | 集合が 4-AP-free で逆数和が 4.439753474215620 を超えること | Walker の集合の逆数和の値そのもの（整数演算で厳密、幅 10⁻³²）・頭が切り詰めと等しいこと（部分集合と下界だけ） |
| ハドヴィガー・ネルソン f(3) = 10・f(4) ∈ {{14,15}} | 下界の証人・候補 117 類／2,100 類／296＋103 類の非実現 | 候補の列挙が尽くされていること・同型判定・最小次数の導出（計算） |
| コラッツ・1/3 の符号 | 不等式 3·log₂3 < 5 と、そこから出る禁止語と非対称の符号 | 模型の前提（v が Terras 分布・g と独立）——既知の部品と実測 |
| #827・n₄ = 7 | 下界の配置・35 類の全数性・34 類の非実現・八面体型から 7 点への繋ぎ（鎖の全体が一本の言明） | 一般の位置の規約の選び方・先行記録（フォーラム）の計算の検査 |
機械検査が保証するのは「書いた命題からその結論が出ること」です。命題が意図した内容を書けているか、それが世の中で新しいかは、機械は何も言いません。その仕分けは 新規性の棚卸し と、Lean の説明 08 にあります。
改訂 2026-09-27：束を
2026-10-09：記事ごとの束に、論文「片側の橋」の束と p 進高さ対の束を足した。どちらも独立な lake プロジェクトで、
2026-10-15：教科書の第 12・13 部が引く束二つ（板と容器・挿入の恒等式）を足した。
2026-10-15（夜）：第 15 部と第 10 部の論文五本が引く束（単体の .lean の束、公理の記録つき）を足した。
principia（主題ごとの名前空間）に改め、台帳を主題ごとの一覧にした。2026-10-09：記事ごとの束に、論文「片側の橋」の束と p 進高さ対の束を足した。どちらも独立な lake プロジェクトで、
lakefile.lean は Mathlib をタグ v4.33.1 で指す（コミット番号で指すと lake build が manifest の警告を出すため）。2026-10-15：教科書の第 12・13 部が引く束二つ（板と容器・挿入の恒等式）を足した。
2026-10-15（夜）：第 15 部と第 10 部の論文五本が引く束（単体の .lean の束、公理の記録つき）を足した。