新規性の棚卸し — 到達点を四つの札で仕分ける
自然哲学の記事で言えたことを、どこまで確かめてあるかで仕分けた一覧です。札は四つ。上から下に弱くなります。「世の中に対する新しさ」は、どの行も「探した範囲で見当たらない」までしか書きません。
Lean で閉じた言明14 群Lean 4 + mathlib。標準三公理以下・
sorryAx なし・native_decide なし紙の証明8 件証明はあるが機械検査は未了
計算で閉じた事実10 件この端末で確かめた範囲。外に出す主張にはしない
既知・言い換え多数既知の定理の再発見・外の文献の確認・記事の訂正
この記事の順序
物差し
判定の物差し — 四つの札
| Lean | Lean 4 + mathlib で機械検査済み。#print axioms が標準三公理（propext／Classical.choice／Quot.sound）以下を返し、sorryAx（未証明の穴）も Lean.ofReduceBool（native_decide）も出ないもの。公理の出力が 台帳にあるものだけにこの札を付けます。写しはあるが出力が未収録のものは「公理ログ整備中」と書きます |
| 紙 | 証明はあるが、機械検査は未了。「定理」の語を使うときは必ずこの札を添えます |
| 計算 | 全数列挙・SAT・区間演算などで閉じた事実。「この端末で確かめた範囲」として書き、外に出す主張にはしません |
| 既知 | 既知の定理の言い換え・再発見・外の文献の進展の確認・記事の訂正。新しい数学ではありません |
機械検査が保証しないもの
機械検査が保証するのは、書いた命題からその結論が出ることだけです。保証しないものが三つあります。(1) 命題が意図した内容を書けているか——たとえば「3-AP を含まない」の定義が本当にそれを言っているかは、人が読んで判断するしかありません。(2) その命題が世の中で新しいか——数学ではなく文献調査の問題で、機械は何も言いません。(3) 比較対象の解釈が正しいか——1984 年の論文の「3.00849」が切り捨てなのか丸めなのか、どの集合についてなのか。
01
Lean で閉じた言明
定理名は Lean のソースの名前そのままです。「公理の出力」の欄は 台帳の状態です。
| 問題 | 言明 | 定理名 | 公理の出力 |
|---|---|---|---|
| コラッツ | 3n+1 の乗数 3 は、この形の写像で唯一の「ちょうど臨界」（臨界乗数が整数になるのは 3 だけ） | Shiori.qcrit_eq_three・qcrit_not_int_of_three_le | 台帳にあり（配布物） |
| コラッツ | 符号の共役・六つの剰余類の最小値・必要な率・c=3 の型の不成立 | Shiori702.syracuse_sign_conjugation・Shiori737.min_over_six_classes・Shiori716.necessary_rate・Shiori751.c_three_pattern_fails | 台帳にあり（配布物） |
| コラッツ | 模型 ek+1 − ek = vk+1 − gk（v ≥ 1 だけを仮定）で、三歩続けて下がることはなく（ek+3 − ek ≥ −2）、非対称 (3·log₂3 − 5)/4 は負。どちらも 3³ < 2⁵ から | Collatz1139.no_three_consecutive_descents・eK_three_step_lower・asymmetry_negative・three_cA_lt_five | 公理ログ整備中 |
| #169（k=3） | 3-AP を含まない有限集合で、逆数和が 3.0085385 を超える（84 段・窓分離ベルマン）。1984 年の記録 3.00849 を超える | Shiori959.erdos169_lower_record_939・setA939_apfree_and_lower・Shiori939.setA939_lower | 台帳にあり（配布物） |
| #169（k=3） | 100 段の集合が 3-AP-free で記録を超えること・窓分離の合併補題・Wróblewski の補題 1 | Shiori844.setA_apfree_and_beats_record・Shiori712.apfree_iUnion_of_separated・Shiori730.lemma1_nonaveraging ほか看板 20 本 | 台帳にあり（配布物） |
| #169（k=4） | 4-AP を含まない有限集合で、逆数和が 4.439753369254541 を超える（Walker 2025 の記録集合の逆数和を 15 桁で切り上げた数）。下界 4.439753474215620 | Shiori1112.setA4_apfree_and_beats_walker・setA4_apfree_and_lower | あり（15 件）・証明書の置き場にも |
| #169（k=4） | k-AP を含まない集合の入れ子補題（Wróblewski の補題 2 の k 一般の形）・Walker の Theorem 1.2（桁集合が mod b で k-AP を含まなければ K(S,b)+1 は k-AP-free） | Shiori1109.core_strong・lemma2_four・Shiori1112.KSet55_apfree | あり（15 件）・証明書の置き場にも |
| ロヴァース（周辺） | 30 頂点の三価二部グラフで、連結・長さ 28 の閉路あり・全閉路 ≤ 28・非ハミルトン（欠損 def = 2）。同型を除いて 3 類 | Shiori1161.G30_def2／Shiori1193.G30b_def2・G30c_def2 | あり（14 件・20 件） |
| ロヴァース（周辺） | 20 頂点の連結三価二部グラフで、周長 14・非ハミルトン | Shiori1193.G20_def6 | あり（20 件） |
| ロヴァース（周辺） | 一般化ペテルセングラフ GP(n,3) のハミルトン閉路の個数は n = 7, 9, 11, 13, 15 で 7, 9, 11, 26, 75 であり、n で割り切れる | Shiori1168.GP{7,9,11,13,15}_hc_card・card_dvd_of_perm_free・Shiori1173.GP{n}_dvd_rot・gp{7,13,15}_dvd_by_rotation | あり（21 件・24 件） |
| ロヴァース（周辺） | 奇数 n ≥ 7 のすべてで、GP(n,3) のハミルトン閉路の個数は n で割り切れる。仮定なし。部品は回転の自己同型・巻き数・ブロック構造・置換の符号・閉路のダーツの局所構造・第一帰還写像 | Shiori1202.gp3_dvd_hc_odd・Shiori1195.*・Shiori1197.*・Shiori1199.*・Shiori1202.* | あり（41・42・30・30 件） |
| ハドヴィガー・ネルソン | 独立数 ≤ 3 の単位距離グラフが 10 点に、独立数 ≤ 4 のものが 14 点にある（Moser ⊔ K₃・Moser ⊔ Moser）。一般に f(2k) ≥ 7k・f(2k+1) ≥ 7k+3 | Shiori1183.fGe_10_3・fGe_14_4・Shiori1192.hn_lower_family・indepNum_sum・fGe_add | あり（23 件・31 件） |
| ハドヴィガー・ネルソン | 11 点の候補 117 類・16 点の候補 2,100 類は平面に単位距離で実現しない（非実現の証明書） | Shiori1178.hn11_no_realiz・Shiori1185.hn16_no_realiz | あり（26 件・27 件） |
| ハドヴィガー・ネルソン | 16 点の列挙で落とした 10 点の部分グラフ 296 類＋103 類は実現しない。三辺測量の核（平方根が消える一次式）と箱の評価 | Shiori1189.hn10_no_realiz・hn10_no_realiz2・Shiori1178.trilat_core・lam_box | あり（22 件） |
「Lean の外」に残るものは各行に対応して決まっています——k=4 では Walker の集合の逆数和の値そのものと「頭が切り詰めと等しい」こと、def = 2 では最小位数と「ちょうど 3 類」、HN では候補の列挙が尽くされていること。これらは下の計算か紙の側にあります。
02
紙の証明のある定理
| 問題 | 言明 | 状態 |
|---|---|---|
| コラッツ | 停止時間の裾の定理。E(k) = #{r mod 2k : 停止時間 > k}（OEIS A076227）、uk = E(k)/2k について uk ρ−k k3/2 = A(θk) + o(1)。A は周期 1・平均 10.892710・振幅 7.59%、ρ = 0.9659065532。フーリエ係数は閉じた形 | 紙 Vatutin–Wachtel 2009 の定理 6 と Cramér の傾け、Sparre Andersen の恒等式（有理数で k ≤ 60 一致）。非中心格子で前因子が振動すること自体は一般論にあり、新しいのは閉じた形とこの数列への適用 |
| ロヴァース | 切頭は一世代で凍結する。T(G) がハミルトン ⟺ G がハミルトン。T²(G) は決して頂点推移でない。切頭型の 5 個目は 3,840 頂点まで無い | 紙 |
| ロヴァース（周辺） | 辺推移な d-正則グラフの辺連結度は d。Aut の頂点軌道が二つなら、def = 2 の欠損グラフは張る・正則・大きさ ≥ n/2。系：semisymmetric で def = 2 なら三価は n ≥ 50、四価は n ≥ 26 | 紙 三価 semisymmetric は 3,000 頂点未満でハミルトン（arXiv:2602.14388）なので、三価の側は目録に支配される |
| ロヴァース（周辺） | def = 2 の 2-辺切断による分解は次数 d ≥ 3 の全部に移る。二部の局所補題：n ≥ 4d、内周 ≥ 6 なら n ≥ 6d − 4（Heawood で等号） | 紙 |
| #169 | 接頭辞カット。Kempner 型の集合 A = {1..J} ∪ (K(S,b)+J+1) の逆数和が記録 13.5332472 以上なら、各 v₀ で |S ∩ [0,v₀]| ≥ mreq(v₀)。記録は下限としてしか使わないので、記録が上がっても結論は保たれる | 紙 |
| #169 | 円分性の命題の帰納の一歩。S が 3-AP-free、(1+xc) ∣ PS、3c > D なら S = {0,c} ⊕ S′ で S′ も 3-AP-free・PS′ は円分。昇格補題 EL ⟹ 命題全体 | 紙 局所の論法は c > D/3 で止まる（本物の直和で c ≤ D/3 の例がある） |
| #563 | β(n,m) ≥ k ⟺ n < R(𝒢m,k)。Pα(m) := R(𝒢m,⌊αC(m,2)⌋+1) として F(n,α) ~ cα log n ⟺ Pα(m)1/m → e1/cα。α = 0 は #77 そのもの。超乗法性は偽、辞書式積は α ≥ 1/3 で無効、XOR 型積も無効 | 紙 Erdős–Pach 1983 の擬ラムゼー数の言い換え |
| ハドヴィガー・ネルソン | α ≤ 2 なら 7 点以下・α ≤ 3 なら 12 点以下（Moser spindle の最小辺数と u(m) の比較） | 紙 のちに Lean で 11 点・10 点に更新 |
03
計算で閉じた事実
この端末で確かめた範囲です。外に出す主張にはしません。
| 問題 | 事実 |
|---|---|
| ハドヴィガー・ネルソン | f(3) ≤ 10 と f(4) ≤ 15 の候補の列挙が尽くされていること（ω ≤ 3・K2,3-free・u(m) 検問・最小次数・同型判定）／f(5) ≤ 24 |
| ロヴァース（周辺） | def = 2 の連結三価二部グラフの最小位数は 30、30 頂点にちょうど 3 類／非ハミルトンな連結三価二部グラフの最小位数は 20、同型を除き一意／四価二部で def = 2 は n ≤ 24 に無い（n ≤ 40 の四価二部頂点推移 4,623 個は全部ハミルトン）／既知の非ハミルトン三価二部 EH54・EH78・Horton96 はいずれも def = 2 |
| #169 | k = 8 の Kempner 型は b ≤ 200 で b = 121 を除き記録 13.5332472 以下／k = 5, 7, 8, 9 の記録値 7.8723049・13.5905274・13.5332472・13.5637722／k = 4 の頭は b ≤ 1000 の積構成で閉じている／円分性の命題は deg ≤ 52（67,236 集合）で反例なし |
| ラムゼー | ω(P₇₉₇) = 9（R(10,10) ≥ 798 の出所）／R(9,9) ≥ 565 は Paley では更新できない |
04
既知・言い換え・外の文献で決着したもの
| 問題 | 内容 |
|---|---|
| コラッツ | 1/3 の符号の模型は Terras の分布と Sturmian 語の標準部品の言い換え。新しいのは「符号と禁止語が同じ不等式から出る」ことと反転点 25/3 だけ／停止時間の前因子が振動すること自体は Vatutin–Wachtel・Mogulski–Rogozin の一般論にある／定数 C の閉じた式は既出、固有構造の記述が加わった |
| リーマン | Hurwitz 族の零点の一次摂動 dρ/da = ρζ(ρ+1)/ζ′(ρ) は初等／Re ζ′(ρ) > 0 ⟺ |S(γ)| < 1/2 は既知の恒等式（arXiv:2305.14253）／零点上の統計で見えた 1/12 は ζ と無関係な恒等式——零点上の統計は「ζ を使わない点過程でも成り立つか」を先に検問しないと、恒等式を発見と誤る |
| ロヴァース | 欠損 def には perimeter gap（Alspach 1981）の名がある／予想「def = 2 の頂点推移グラフは無い」は Grünbaum 1974 の予想を含む／切頭の三定理は既知 |
| #169 | k = 5 の文献値 7.866（GR79 から引かれている値）は 3 桁目が違い、H(G₅) = 7.8723049／「f(3) の頭を替える」道は記録の改良の言い換え／Elkin の因子は Θ(√log n) |
| #563 | Erdős–Pach 1983 の擬ラムゼー数 R̄c(k)（c = 1 − α）と同一の量。α = 0 は #77 |
| ハドヴィガー・ネルソン | 「n/α > 4 の有限単位距離グラフ」は Dúcz–Varga（arXiv:2606.28157）で既知。残る意味は f(α) の確定値だけ／Moser spindle の体 ℚ(√3,√11) の単位ベクトルは 9 方向で 4-彩色可（de Grey の構成は階数 4 の群の外） |
| 外の文献で決着 | #138：Campos–Fox–Schildkraut（arXiv:2608.20824）が w(k) ≥ (1−o(1))k2k−1／#634：Beeson（arXiv:2607.23453）で素数個の合同分割は例外を除き不可能／#165：DJPR（arXiv:1606.01043）の予想 2 ⟹ R(3,k) ≤ (1/2+o(1))k²/log k、下界は HHKP（arXiv:2510.19718）／#52：BSSZ（arXiv:2605.28781）が実数で max(|A+A|,|AA|) ≤ |A|2−c を構成／#143：KLL25（arXiv:2502.09539）が Σ1/x = o(log n)／#30：素数間隔への還元は Lean 4 で形式化済（arXiv:2605.03274） |
05
「新しさ」について言えること
どの行も「探した範囲で見当たらない」までです。探した範囲を書きます。
| 言明 | 探した範囲と、見当たらなかったこと |
|---|---|
| k=3・k=4 の記録（3.0085385・4.4397535） | 一次資料 9 系統と Walker 2025 の表。3.00849 超え・4.43975 超えの記載は見当たらない。第三者の検分を経ていない |
| n 奇・n ≥ 7 ⟹ n ∣ #HC(GP(n,3)) | OEIS に #HC(GP(n,3)) の列も #HC/n の列も無い。arXiv:2503.08326 は線形漸化式で値を与えるが分類ではない。活字は未確認。Burnside の使い方は標準で、専門家には自明でありうる |
| def = 2 の三価二部の最小位数 30 | 検索 20 本と Web で、def = 2 の最小位数を問う文献は見当たらない。House of Graphs との照合は未了。既知の値は 3-連結の最小 50、2-連結平面の最小 26 |
| f(3) = 10・f(4) ∈ {14, 15} | 探した範囲で活字に無い。専門家には自明でありうる |
| 停止時間の裾の閉じた形 | 一般論（前因子の振動）は既知。閉じた形と A076227 への適用は見当たらない |
| 円分性の命題（3-AP-free と直和分解） | 近いのは de Bruijn 1950/53・Billey–Swanson（arXiv:2305.07620）・Filaseta–Kalogirou（arXiv:2508.12242）。同じ言明は見当たらない。証明は未完 |
06
この記事が言えている範囲
| 内容 | |
|---|---|
| 言えている | §01 の各行は、書いた命題からその結論が Lean の kernel で出ること。公理の出力は台帳にあります |
| 言えていない | 未解決問題そのものは一つも動いていません。k=3・k=4 の記録も、予想の本体には触れていません |
| 言えていない | 「世の中に対して新しい」とは、どの行についても書いていません。§05 の範囲の外は当たっていません（MathSciNet・zbMATH・会議録・非英語の文献） |