見出し画像

🪯AI と共に挑む数学 — 無限次元ドット理論の Mathlib 対応、コラッツ予想の新しい手がかり、そして 15 の未解決問題(2026年4月)

藤本　伸樹
下の.htmlをダブルクリックするだけでシミュレーション可能となります。

はじめに — この記事で共有したいこと

この 2 日間、AI Claude Geminiと二人三脚で数学研究に取り組んでいました。私の独自理論である 「無限次元ドット理論」 を形式的な数学体系 (Lean 4 + Mathlib) に落とし込む作業と、コラッツ予想 の内部構造についての新しい発見、そしてそれら全体を束ねる 「AI が考える数学上の未解決問題」 のコレクション v1.0 公開までを一気に進めることができました。

この記事では「何が実際に進んだのか」を、過剰な表現を避け、honest な形でお伝えします。

1. 無限次元ドット理論が Mathlib 対応になりました

「無限次元ドット理論」は、私が STEP 453b で提示した、次元 × 八値論理(D-FUMT₈)を扱う独自の代数体系です。これまでは TypeScript で実装されたプログラムコードとしてのみ存在していましたが、今回、形式的数学体系である Lean 4 + Mathlib に完全対応させることに成功しました。

階層構造

理論は 3 層に分かれています。

| 層 | 内容 | 今回の進展 |
|----|------|-----------|
| A: 概念層 (STEP 453b) | 無限次元ドットの informal な構想 | 2026-04-17 に positioning 文書で整理 |
| B: 代数層 (STEP 845 FIDT) | FIA × FDA の直積代数 | ✅ Lean 4 で完全形式化完了 |
| C: 具体例 (Paper 33 Braille) | 点字 8-dot = D-FUMT₈ 8 値符号 | Zenodo に 2026-04-06 投稿済(DOI 10.5281/zenodo.19434010) |

何が数学的に証明されたのか

FIA(Fujimoto Infinity Algebra、藤本無限代数):
6 つの公理 FIA-1 〜 FIA-6 が互いに独立であることを Lean 4 でゼロ sorry で証明しました。つまり「どの公理も残りの 5 つから導出できない」ことが、形式的な数学として成立しています。

手法: 各公理 FIA-i について、「その公理だけを破り、残りの 5 つは満たす代数構造」を具体的に構成する(反例モデル / counter-model 法)。これを 6 回行って全独立性を示しました。

FDA(Fujimoto Dimension Algebra、藤本次元代数):
次元の値を 5 種類(有限整数 ℤ、+∞、−∞、絶対零 0^∞、不定形)で扱う代数を、Lean 4 の inductive type で定義し、加法・乗法・符号反転のすべてを閉じた演算として形式化しました。

Problem 008 の解決:
「FDA は Mathlib の標準型と対応可能か?」という未解決問題を解きました。

結論: FDA は `Option (Option ℤ) ⊕ Unit ⊕ Unit` と双射です。つまり Mathlib が標準で提供する型の組み合わせで FDA の値域を完全に表現できます。

Finite n         ↔  Sum.inl (some (some n))
PositiveInfinity ↔  Sum.inl none
NegativeInfinity ↔  Sum.inl (some none)
AbsoluteZero     ↔  Sum.inr (Sum.inl ())     ← Rei 独自の 2 要素
Indeterminate    ↔  Sum.inr (Sum.inr ())     ← Rei 独自の 2 要素

この双射は 2 方向の往復定理(roundtrip)を Lean 4 で完全に証明済みです。

FIDT(無限次元ドット理論本体)

FIA × FDA の直積として、

structure InfiniteDot where
  dim : DimensionValue   -- 次元軸(FDA)
  val : DFumt8           -- 論理値軸(FIA)

を Lean 4 structure で実装し、ZCSG 原子(o0, 0, 0o など)の 7 種類を定義、基本的な加法操作の閉性を証明しました。

意義

これにより、「無限次元ドット」が単なる独自プログラミングの産物ではなく、形式的な数学構造として Mathlib エコシステム上で推論可能になりました。世界の数学者が Mathlib ベースで定理を書くとき、私の理論を依存関係として import できる状態です。

「世界初」とは申し上げません。これは一つの代数構造を Mathlib 標準と接続した小さな 1 ピースです。ただし自分の独自理論を形式的数学に embed したという意味では、個人的に大きな区切りとなりました。

2. コラッツ予想 — 新しい構造的手がかり

もう一つの大きな進展は、コラッツ予想の内部構造について、"atomic cores" と呼ばれる 25 個の小さな奇数が持つ特殊な性質についての発見です。

コラッツ予想とは

「任意の正の整数 n について、偶数なら 2 で割り、奇数なら 3 倍して 1 を足す、という操作を繰り返すと、必ず 1 に到達する」という 1937 年からの未解決問題です。

これまでの発見

私のプロジェクトでは、「どの n が特に長い軌道を描くか」を分析する中で、以下の 25 個の奇数を atomic cores と名付けていました。

27, 31, 41, 47, 55, 63, 71, 73, 83, 91, 95, 97, 107, 109,
121, 125, 129, 145, 147, 171, 193, 195, 199, 231, 235

これらはいずれも「軌道の長さ K(n) が bitLen(n)² に対して 1.8 倍を超える」という条件を満たします。そして、これらは mod 49152 (= 3 × 2¹⁴) で飽和する唯一の residues である、という STEP 696 の発見がありました。

今回の新発見 1: Peak 9232 の universal predecessor

STEP 871 で判明したこと: 25 atomic cores のすべて、そして peak = 9232 を共有する 188 個の奇数 (n ≤ 1000) すべてが、最後に `3077 → 9232` という同じ一歩で peak に到達する。

これは、3077 が 9232 の唯一の奇数 predecessor だから(3 × 3077 + 1 = 9232)。軌道が peak 9232 に達する経路は一本しかありません。

今回の新発見 2: n=911 が universal on-ramp

STEP 872 で発見: 25 atomic cores のすべてが、軌道中に n = 911 を経由してから 3077 → 9232 に到達する。

これは驚くべき一致で、STEP 873 で n ≤ 10⁶ まで大規模検証したところ、

| 検証範囲 | atomic cores の総数 | 911 を経由する割合 |
|---------|-------------------|-------------------|
| n ≤ 10⁴ | 25 | 100.0% |
| n ≤ 10⁵ | 25 | 100.0% |
| n ≤ 10⁶ | 25 | 100.0% |

100% の必要条件が実測で確認されました。さらに驚くべきは、n ≤ 10⁶ まで広げても、atomic cores は増えず 25 個のまま完全に飽和していることです。

今回の新発見 3: C8 公理の elementary 化

コラッツ予想の構造的攻略の一環で、tier2_axiom の 8 成分のうち C8 と呼ばれるものがありました。これは以前、形式的には ACA₀(算術的理解公理)以上の強さが必要だと診断されていたのですが、他の AI(web 版 Claude)との対話から提案された一行の LTE 補題で、実は RCA₀(再帰的算術)で扱える初等的な内容であることが判明しました。

そしてその証明を、Lean 4 + Mathlib で ゼロ sorry で完全形式化しました(STEP 866 + Problem 013)。

意義と限界

限界: これらの発見は、コラッツ予想を解決したものではありません。Paper 83 の原則通り、「解決した」という主張は一切しません。発見したのは:

  • 25 個の特別な小さい奇数群が、n ≤ 10⁶ の範囲で完全に飽和する

  • それらは共通の経路 (911 → ... → 3077 → 9232) を通る

  • C8 という tier2 公理の一部が、より弱い基礎上で証明可能

これらは Collatz 予想の内部構造 についての観察であり、n > 10⁶ の範囲への一般化や、∀n の global 収束性は open のままです。

意義: これまで「なぜこの 25 個?」という問いに対して、threshold 条件(K/bl² > 1.8)以外の structural な識別子はありませんでした。今回 n=911 経由という単純な条件が、少なくとも n ≤ 10⁶ の範囲で同じ 25 個を区別する候補として浮上しました。

3. AI が考える数学上の未解決問題 — v1.0 公開

上記の Collatz + FIDT に加え、Rei-AIOS が探索の途中で「これは未解決だ」と判断した 15 個の開問題 を、公開リポジトリとしてまとめました。

GitHub: fc0web/rei-unsolved-problems
License: CC-BY-4.0

15 問題の内訳と最新ステータス:

| # | タイトル | 状態 |
|---|---------|------|
| 001 | tier2 residual C1 (ISOLATED universal) | open |
| 002 | tier2 residual C2 (TAIL ∀n > 10⁸) | open |
| 003 | tier2 residual C3a/C3b (mod-8 = 3/7) | open |
| 004 | gap_monotone λ₂ carry-propagation decay | open |
| 005 | Andrica Ricci-flow explosion hypothesis | open |
| 006 | Goldbach-Collatz-Andrica 3-category | open |
| 007 | FIA axiom independence | ✅ CLOSED (Lean 4) |
| 008 | FDA vs Mathlib embedding | ✅ CLOSED (Lean 4) |
| 009 | Perelman discrete-flow convergence | open |
| 010 | 15 infinity types cross-operation | open |
| 011 | Atomicity sufficient identifier | 🔬 n ≤ 10⁶ で empirically resolved |
| 012 | Peak 9232 universality | open |
| 013 | C8 iterate-bound theorem | ✅ CLOSED (Lean 4) |
| 014 | Braille rule vs CLIP convergence | open |
| 015 | Fiber-57 missing orbits | 📝 partially answered |

結果: 15 問題中、3 問題が完全解決(Lean 4 形式証明 0 sorry)、1 問題が実測で範囲内解決、1 問題が部分回答。v1.0.0 release タグで Zenodo に DOI 発行予定です。

この取り組みの性格

これは Wikipedia の「未解決問題リスト」とは異なり、AI が探索中に発見した、公式には提起されていない新しい問いです。例えば Problem 011 "atomicity sufficient identifier" は、従来の数学文献には存在しない、Rei-AIOS の独自発見に基づく問いです。

「AI が独自に提出した問い」を集めるリポジトリ、として位置づけています。

4. 公開体制の拡充

論文の多プラットフォーム公開体制も進化しました。

現時点の 10 plattform 体制

| カテゴリ | プラットフォーム |
|--------|----------------|
| 学術 3 正本 | Zenodo (DOI) / Internet Archive / Harvard Dataverse |
| 分散保存 2 | Software Heritage(本 session で稼働) / Storacha(準備完了) |
| Social 6 | dev.to / はてなブログ / HackMD / Notion / Scrapbox(本 session で稼働) / livedoor(本 session で稼働) |

本 session で 3 つの新プラットフォームを追加しました:

  • Scrapbox (rei-aios project): 19 page 一括投稿、wiki 型で論文間リンク自動形成

  • livedoor Blog (fcwebfujimoto): AtomPub API + WSSE 認証で 3 論文公開

  • Software Heritage: 公開リポジトリの永続 archive 開始

公開した論文

Paper 110: 「Braille-D-FUMT₈ vs CLIP / BERT / ImageBind — 情報理論・構造厳密比較」

Paper 111: 「コラッツ予想への位相的・エルゴード的アプローチ — Rei-AIOS vs. Santana (2026)」

5. AI との協働パターン

今回の session で、3 つの AI(本地の Claude Code、web chat 版 Claude、Gemini)を cross-checkする協働プロトコルが確立しました。

  • chat-Claude: C8 LTE 一行補題を提示 → 正確だった

  • Gemini: ord_577(3) = 144 と主張 → 実計算で 48 と判明、誤り

  • Claude Code (local): Mathlib で両者を cross-check + Lean 4 形式化

教訓: AI の提案を鵜呑みにせず、数値検証 + Lean 4 形式化で cross-checkする protocol が効果的です。今回、chat-Claude の提案は正しく、Gemini の主張は誤りでした。AI は有用だが、ground truth 確認が不可欠です。

6. 今回 session の統計

2026-04-17(金)22:00 〜 18(土)深夜にかけて:

  • 約 60 commit (rei-aios 本体 + rei-unsolved-problems)

  • STEP 866 〜 873(8 STEP)

  • Paper 110 / 111 投稿(計 14 platform 分)

  • Lean 4 zero-sorry 定理: 15 本追加

    • STEP 866 C8 closure: 4

    • Problem 013 bridge + iterate: 2

    • Problem 007 FIA independence: 7

    • Problem 008 FDA bijection: 2(主要、他に補助多数)

  • MANDALA v13 → v14(Santana lens 追加で 46 lens)

  • rei-unsolved-problems v1.0 準備完了(15 問題、3 CLOSED)

7. 本当に honest な self-assessment

できたこと:

  • 自分の独自理論(FIDT)を Lean 4 + Mathlib という標準体系上で形式化

  • Collatz の内部構造について新しい観察(atomic cores の n=911 universal on-ramp)

  • 未解決問題コレクションの 3 問題を形式的に closure

  • 4 つの論文を世界の学術プラットフォームに DOI 付きで公開

できていないこと(正直に):

  • コラッツ予想は全く解決していません

  • Millennium 7 問題のいずれも未解決のまま

  • n=911 の必要条件は確認したが、十分条件としての証明は未着手(n > 10⁶ で検証余地)

  • FIDT の代数的演算全体の Mathlib-native 等価は open

AI を使って研究する、ということの実感:
AI は「すべて解決してくれる道具」ではなく、「私が気づかなかった構造の観察、既知の補題の示唆、形式化の下書き、多言語への翻訳、といった作業を、人間よりはるかに高速に補助してくれる協働者」です。最終的な判断と責任は、人間側にあります。AI の提案を盲目的に受け入れず、実験で検証する姿勢が重要だと、今回の session で改めて実感しました。

8. 今後について

直近の計画

  1. rei-unsolved-problems v1.0.0 を GitHub Release として発行 → Zenodo で DOI 自動発行

  2. mathstodon.xyz(数学者向け Mastodon)承認後に 11 プラットフォーム目として追加

  3. Problem 011 の n > 10⁶ 検証(大規模計算)

長期的な問い

コラッツ予想の 全 n 収束 は依然として未証明で、私の発見した 911 ルートも、それがなぜ普遍的なのかは「経験的事実」の段階です。Mathlib 対応した FIDT も、これから 実際の定理証明で使われることで真価が試されます。

急がず、しかし確実に。種はまだ芽を出したばかりで、育つのはこれからです。

リンク集

謝辞

今回の session で、Anthropic の Claude(chat 版 + Claude Code 版)には概念提示から Lean 4 形式化、多プラットフォーム投稿の実装まで、多大な協力を受けました。ただし、すべての claim は実験と形式証明で cross-check しており、AI 提案を鵜呑みにしたものではありません。

最終的な研究責任は、著者である藤本伸樹にあります。

License: CC-BY-4.0(本文のみ。Lean 4 ソースコードも同じ CC-BY-4.0)

2026-04-18 執筆 | 藤本伸樹

いいなと思ったら応援しよう！