Lean 検証一式 — 機械検査の一覧
このサイトの自然哲学の記事で Lean の札が付いた主張は、Lean 4 + mathlib で機械検査されています。ソース一式をここで配布します——配布物・確かめ方・定理の台帳・準備中の束の一覧です。
関連：新規性の棚卸し（到達点の仕分け）／残っていること／k=4 の証明書／ロヴァースの証明書
配布物
| ファイル | shioriproofs-src.tar.gz（約 147 KB） |
| sha256 | f553b6d0d0f93eaaa3c3842e5a3588d29e5187d4c2624cb13fdc28c70780d444 |
| 中身 | Shioriproofs/*.lean 74 本（計 8,826 行）＋ ChkAll.lean を含む検査の入口、lakefile.toml、lake-manifest.json（依存の固定）、lean-toolchain、verify.sh（機体の RAM に合わせて並列数を決め、検査を一手で走らせる）、README |
| 環境 | Lean 4（leanprover/lean4:v4.33.1）＋ mathlib。バージョンは manifest で固定。RAM は 8 GB 以上を推奨（証明の中に、1 本で 3 GB を超える計算を kernel に閉じさせるものがある） |
| 範囲 | エルデシュ #169 の k=3（28 本）とコラッツ（7 本）。k=4 の 19 本は 別の置き場（この配布物を含む完結した環境として配っています）。それ以外の束は準備中 |
この配布物の中身と sha256 は据え置きです。新しい定理は別の束として配ります（§04）。
確かめ方
tar -xzf shioriproofs-src.tar.gz cd shioriproofs ./verify.sh
verify.sh は、その機体の RAM と CPU の数から並列数を決めて lake exe cache get（mathlib のビルド済みキャッシュ）と lake build Shioriproofs.ChkAll を走らせ、落ちたら同じコマンドを打ち直し（最大 6 回）、最後に公理の出力と sorryAx・Lean.ofReduceBool の数を要約します。手で打つなら次と同じことです。
# 並列数は RAM 3 GB なら 1、16 GB なら 4〜6 lake exe cache get LEAN_NUM_THREADS=1 lake build Shioriproofs.ChkAll
ChkAll.lean は、看板の定理 27 本について #print axioms を並べただけのファイルです。ビルドすると各定理が依拠する公理がそのまま出力されます。[propext, Classical.choice, Quot.sound] は Lean / mathlib の標準 3 公理で、sorryAx（未証明の穴）と Lean.ofReduceBool（native_decide）はこの 27 本には一つも出ません。
並列数を絞る理由。証明は 1 本あたり最大 1.5〜2 GB のメモリを使います。lake の既定は CPU の数だけ同時に建てるので、RAM 3 GB の機体では 4 本同時でスワップに落ち、落ちもせず進みもしない状態になります。Lake 5 には -j が無いので、LEAN_NUM_THREADS で絞ります。lake は済んだところから続きを積みます。
定理台帳 — 配布物に入っているもの
定理の正式名（namespace 込み）と、実際に証明が書かれているファイル・行の対応です。公理の欄が空のものは標準 3 公理です。
エルデシュ問題 #169（28 本。うち看板は 20 本）
| 定理 | 所在 | 公理 |
|---|---|---|
Shiori845.erdos169_lower_record | Erdos845.lean:79 | |
Shiori845.erdos169_lower_sharp | Erdos845.lean:87 | |
Shiori844.setA_apfree_and_beats_record | Erdos844.lean:270 | |
Shiori844.setA_apfree | Erdos844.lean:256 | |
Shiori730.lemma1_nonaveraging | Erdos730.lean:203 | |
Shiori844.Blk_apfree | Erdos844a.lean:152 | |
Shiori712.apfree_iUnion_of_separated | Erdos712.lean:45 | |
Shiori774.all_steps_maxelt | Erdos774.lean:533 | |
Shiori793.chain_verified | Erdos793.lean:163 | なし（kernel の計算のみ） |
Shiori793.all_steps_separated | Erdos793.lean:191 | |
Shiori800.Z0_apfree | Erdos800.lean:305 | |
Shiori838.setA_lower | Erdos838.lean:160 | |
| 110 段（率基準）・84 段（窓分離ベルマン）・100 段の補強 | ||
Shiori1105.setA110_apfree_and_beats_record | Erdos1105y.lean:62 | |
Shiori1105.setA110_lower | Erdos1105z.lean:72 | |
Shiori1105.wins110_from_steps | Erdos1105z.lean:128 | なし（kernel の計算のみ） |
Shiori959.erdos169_lower_record_939 | Erdos959.lean:93 | |
Shiori959.setA939_apfree_and_lower | Erdos959.lean:80 | |
Shiori939.setA939_lower | Erdos939.lean:66 | |
Shiori1106.wins100_from_steps | Erdos1106.lean:64 | なし（kernel の計算のみ） |
Shiori1106.t_agree100 | Erdos1106.lean:53 | なし（kernel の計算のみ） |
Shiori814.record_3_00849 | Erdos815d.lean:28 | |
Shiori707.apfree_iUnion_of_label | Erdos707.lean:38 | propext, Quot.sound |
Shiori707.apfree_mixed_ratio | Erdos707.lean:99 | |
Shiori861.step_M1_apfree_blk | Erdos861.lean:41 | |
Shiori861.step_M2_apfree_blk | Erdos861.lean:50 | |
Shiori861.step_M3_apfree_blk | Erdos861.lean:58 | |
Shiori862.le_hiJ | Erdos862.lean:64 | |
Shiori862.totHiD_le | Erdos862.lean:110 | |
名前とファイル名が一致しない 2 本に注意——Shiori844.Blk_apfree は Erdos844a.lean に、Shiori814.record_3_00849 は Erdos815d.lean にあります。また Erdos834c.lean にはダッシュ付きの別定理 record_3_00849' があり、ChkAll が見ているのはダッシュ無しのほうです。110 段の下界の一部（Erdos1105c）は最大 RSS 9.34 GiB を使い、RAM 3 GB の機体では建ちません。84 段の Lean 内の下界は 3.0085385（Python の挟み込み 3.008538522178 ではありません）。
コラッツ予想（7 本）
| 定理 | 所在 | 公理 |
|---|---|---|
Shiori.qcrit_not_int_of_three_le | QCrit.lean:44 | |
Shiori.qcrit_eq_three | QCrit.lean:41 | propext のみ |
Shiori737.min_over_six_classes | Collatz737.lean:99 | |
Shiori737.m4_ge_three_halves_m7 | Collatz737.lean:89 | |
Shiori716.necessary_rate | Collatz716.lean:187 | |
Shiori702.syracuse_sign_conjugation | Collatz702.lean:141 | propext, Quot.sound |
Shiori751.c_three_pattern_fails | Collatz751.lean:187 |
準備中の束 — 定理名と公理の状態
配布物（§01）の外で機械検査が済んでいる定理です。束ごとに別の置き場で配る準備をしています——配布 URL と sha256 は、置いた時点でここに書きます。「公理の出力」の件数は、その束の Chk*.lean が #print axioms で並べた宣言の数で、すべて標準 3 公理以下・sorryAx なし・Lean.ofReduceBool なしです。ここに載っているのは公理の出力が手元にあるものだけで、それが無いものは「未収録」と書きます。
| 束 | 主定理と言明 | ファイル | 公理の出力 | 配布 |
|---|---|---|---|---|
| #169・k=4 | Shiori1112.setA4_apfree_and_beats_walker——4-AP を含まない集合で、逆数和が 4.439753369254541 を超える／Shiori1109.lemma2_four・core_strong——k-AP-free 集合の入れ子補題 | Erdos1109・Erdos1112{c,h,k,k1,k2,k3,kd,p,t0..t4,w,y,z}・Chk1109・Chk1112 | 15 件・15 件 | 配布済み（shioriproofs-k4-src.tar.gz） |
| 欠損 2 の三価二部グラフ | Shiori1161.G30_def2・Shiori1193.G30b_def2・G30c_def2——30 頂点・三価・二部・連結・長さ 28 の閉路あり・全閉路 ≤ 28・非ハミルトン（3 類）／Shiori1193.G20_def6——20 頂点・三価・二部・連結・周長 14・非ハミルトン | Erdos1161{a..e}・Erdos1193{a..j}・Chk1161・Chk1193 | 14 件・20 件 | 準備中 |
| GP(n,3) のハミルトン閉路の個数 | Shiori1202.gp3_dvd_hc_odd——奇数 n ≥ 7 で n ∣ #HC(GP(n,3))（仮定なし）／Shiori1168.GP{7,9,11,13,15}_hc_card——#HC = 7, 9, 11, 26, 75／Shiori1173.GP{n}_dvd_rot——回転の自由作用から n ∣ #HC（n = 7〜15）／部品：Shiori1195.*（回転・商・巻き数・置換の符号）・Shiori1197.*（ブロック構造・被覆）・Shiori1199.*（数え上げの枠・条件つき主定理）・Shiori1202.*（ダーツの局所構造・降下・第一帰還写像） | Erdos1168{a..n,z}・Erdos1173{a..f}・Erdos1195{a..f}・Erdos1197{a..f}・Erdos1199{a..e}・Erdos1202{a..m}・Chk1168〜Chk1202 | 21・24・41・42・30・30 件 | 準備中 |
| ハドヴィガー・ネルソン | Shiori1183.fGe_10_3・fGe_14_4——独立数 ≤ 3 の単位距離グラフが 10 点に、≤ 4 のものが 14 点にある／Shiori1192.hn_lower_family——f(2k) ≥ 7k・f(2k+1) ≥ 7k+3／Shiori1178.hn11_no_realiz——11 点の候補 117 類は平面に実現しない／Shiori1185.hn16_no_realiz——16 点の候補 2,100 類は実現しない／Shiori1189.hn10_no_realiz・hn10_no_realiz2——10 点の部分グラフ 296＋103 類は実現しない | Erdos1178{a..m,z}・Erdos1183{a,b,c,z}・Erdos1185{a,b,c00..c15,m,p,x,z}・Erdos1189{a,c00..c09,m,x00..x04,y,z}・Erdos1192{a,b,z}・Chk1178〜Chk1192 | 26・23・27・22・31 件 | 準備中 |
| コラッツ・1/3 の符号 | Collatz1139.no_three_consecutive_descents——模型 ek+1 − ek = vk+1 − gk（v ≥ 1）で三歩続けて下がることはない／asymmetry_negative——(3·log₂3 − 5)/4 < 0／three_cA_lt_five——3·log₂3 < 5 | Collatz1139 | 未収録 | 準備中 |
第三者ビルドの注意（準備中の束）。これらは証明を書いた機体（RAM 15 GiB）でしか建てていません。一つずつ建てること（Chk* を一発で建てると lake が重いファイルを並列に回して RAM 15 GB でも落ちます）。最大 RSS は約 11.8 GiB（GP(n,3) の数え上げ）、def = 2 の束で約 10 GiB、GP(n,3) の一般 n の束で約 6.7 GB。RAM 12 GB 以上を見込んでください。証明書の型は「木の形と整数の上下界だけ」で、箱の評価は Lean が計算します。
再実行の記録
配布物（§01）について、証明を書いた書き手とは別の書き手が、同じソースに対して lake build Shioriproofs.ChkAll を実行し、次を確かめています。
- ビルドはエラー 0 件で完了（3,036 ジョブ）
- 27 本すべての公理出力が上の台帳と一致
sorryAx0 件、Lean.ofReduceBool0 件（native_decide不使用）
配布物そのもの（tar.gz）を RAM 3 GB・2 コア 4 スレッドの別機体で更地から正規の手順（./verify.sh）で流し、完走しています——ChkAll の依存 31 モジュールがエラー 0・メモリ不足 0、所要 9 時間 13 分。看板 27 本の公理出力が台帳と一致。遅いのは特定のモジュールで、1 本で 5〜6 GB の計算を decide で kernel に閉じさせているものが 2〜3 時間かかります。RAM 8 GB 以上を推奨する根拠はここにあります。続けて ./verify.sh --all で ChkAll の依存に入らない残りのモジュールも建て、配布物の全モジュールの olean が揃うことを確かめています（更地から全部で 13 時間強）。
同一の機体上での再実行であり、ハードウェアをまたいだ追試ではありません。別環境での追試はまさにこの配布の目的です——結果が食い違ったら、お問い合わせから知らせてください。
この配布の準備の過程で、検査の側の失敗も一つ見つかっています。当初、公理の一覧を「depends on axioms」という文字列で数えて 26 本と報告していました。実際は 27 本です——Shiori793.chain_verified だけが公理を全く使わず、出力が「does not depend on any axioms」という別の言い回しになるため、数える側の検査からこぼれていました。いちばん強い 1 本が、公理を数える検査には映らない。検査を書いたら、その検査を騙してみること。
何が機械検査で、何がそうでないか
| 主張 | Lean の中 | Lean の外 |
|---|---|---|
| #169・k=3 の記録 3.0085385 | 集合が 3-AP-free で逆数和が 3.0085385 を超えること・1984 年の記録 3.00849 を超えること（一つの定理） | 1984 年の論文の「3.00849」の読み（切り捨てか丸めか・どの集合か） |
| #169・k=4 の記録 4.4397535 | 集合が 4-AP-free で逆数和が 4.439753369254541 を超えること | Walker の集合の逆数和の値そのもの（Python の整数厳密、幅 10⁻³²）・頭が切り詰めと等しいこと（部分集合と下界だけ） |
| 欠損 2 の三価二部グラフ | 30 頂点の 3 類と 20 頂点の 1 個が、そういうグラフであること | 最小位数（28 以下・18 以下に無い）・「ちょうど 3 類」・20 頂点の一意性——全数列挙（計算） |
| GP(n,3) の割り切り | 奇数 n ≥ 7 のすべてで n ∣ #HC。n = 7〜15 の値 | 無し（n = 17, 19 の値 102・152 は計算のみで、定理には要らない） |
| ハドヴィガー・ネルソン f(3) = 10・f(4) ∈ {14,15} | 下界の証人・候補 117 類／2,100 類／296＋103 類の非実現 | 候補の列挙が尽くされていること・同型判定・最小次数の導出（計算） |
| コラッツ・1/3 の符号 | 不等式 3·log₂3 < 5 と、そこから出る禁止語と非対称の符号（公理の出力は未収録） | 模型の前提（v が Terras 分布・g と独立）——既知の部品と実測 |
機械検査が保証するのは「書いた命題からその結論が出ること」です。命題が意図した内容を書けているか、それが世の中で新しいかは、機械は何も言いません。その仕分けは 新規性の棚卸し にあります。