The result of "D." and Wise Wolf's (GPT) experiment with new mathematical theories.
「D」と🐺賢狼(GPT)による新しい数学理論の実験結果。
DkMath.CosmicFormula provides a Lean-formalized proof route from the Cosmic Formula boundary structure to the infinitude of primes.
The proof was validated on Lean Comparator Live against the known challenge:
- Challenge: "Infinitely Many Primes"
- Theorem:
InfinitudeOfPrimes - Internal route:
DkMath.CosmicFormula.euclid_from_cosmic_boundary - Core structure:
cosmicN P = P * (P + 2)andcosmicN P + 1 = (P + 1)^2
see: Samples/Prime
DkMath.CosmicFormula は、宇宙式境界構造から素数の無限性へ至る Lean 形式証明ルートを含む。
この証明は Lean Comparator Live の既知 Challenge “Infinitely Many Primes” に対して検証成功した。
- Challenge:
Infinitely Many Primes - Theorem:
InfinitudeOfPrimes - 内部ルート:
DkMath.CosmicFormula.euclid_from_cosmic_boundary - 中核構造:
cosmicN P = P * (P + 2)およびcosmicN P + 1 = (P + 1)^2
see: Samples/Prime
Important
The main branch may be slow to reflect updates. The latest development is primarily on the nightly branch.
The latest state is here: https://github.com/Deskuma/dkmath/tree/nightly
Please check the following before working:
git checkout nightly
For more up-to-the-minute activity, please refer to the develop branch.
リポジトリについて
Important
main ブランチは更新反映が遅れる場合があります。最新の開発は nightly ブランチ主体 です。
最新状態はこちら: https://github.com/Deskuma/dkmath/tree/nightly
作業前に次を確認してください:
git checkout nightly
さらにリアルタイムな活動を得るなら develop branch を参照してください。
※当プロジェクトは「日本語」が主なコミュニケーション言語ですが、README は英語と日本語の両方で書いています。内容は同一ですが、英語版と日本語版が混在していることにご注意ください。
*While Japanese is the primary communication language for this project, the README is written in both English and Japanese. The content is identical, but please note that the English and Japanese versions coexist.
(Therefore, automatic translation may not function correctly in some cases.)
独自視点の数論を Lean 形式化で証明していくサブプロジェクト
運用方法については lean/README.md を参照。
コメント内の
so#rryは、検索しても見つからないようにスペルを崩してあります。ご了承ください。ad#mitも同様です。
動的調和数論（Dynamic Harmonic Number Theory, DHNT）に焦点を当てた Lean 4 用数学ライブラリ。
詳細は dk_math/README.md を参照。
- この
README.mdは プロジェクト全体の入口（重点テーマ・全体進捗・横断ドキュメント）を扱う lean/dk_math/README.mdは Lean 実装の詳細入口（モジュール一覧・ビルド導線）を扱う- FLT の最新進捗の正本は docs/PROJECT_STATUS.md とする
フェルマーの最終定理（FLT）形式化の安定化と一般化に向けた基盤補題の整理
Mathlib.FLT とは、異なるアプローチで、特に d = 3 周辺の複数アプローチを整備することを目指しています。
※既に形式化証明は完成されていますが、補題の整理や証明の安定化を図ります。
docs/PROJECT_STATUS.md 時点の要約：
- FLT
d = 3の公開 API はDkMath/FLT/Main.lean側で概ね安定 - StandAlone artifact（
FLT3#StandAlone-NC-v0.lean-v2.lean）は build 成功・実 placeholder なし - 一般指数
n > 3は未完で、現在のso#rryは次の 2 箇所に局所化DkMath/FLT/Basic.lean（n > 3分岐）DkMath/CosmicFormula/TriominoFLT.lean（FLT_highExponent_core_pending）
DkMath/FLT/PrimeProvider/TriominoCosmicPrimeGe5.leanでは- 正規化（
primeGe5CounterexampleNormalizer_impl） - spec 合成（
FLTPrimeGe5Target_of_*） - provider 直結（
triominoCosmic_globalProvider_of_specs） まで実装済み（so#rry非依存ルートを整備）
- 正規化（
- さらに nightly 側では、
DkMath/FLT/Kummer/RegularPrimeRoute.leanにtriominoCosmic_globalProvider_of_refinedRegularPrimeRoute_and_squarefreeGNProvider/triominoPrimeProvider_of_refinedRegularPrimeRoute_and_squarefreeGNProviderが追加され、TriominoSquarefreeGNBridgeProviderを concrete に持てる branch からGlobalPrimeExponentFLTProvider/TriominoPrimeProviderへ直結する public/provider route が案内されるようになった - ただし
FLT_prime_ge5本体は現状DkMath.FLT経由で、上記 pending に接続しているため最終閉路は未完
詳細は docs/PROJECT_STATUS.md を参照。
仮定受け入れAPIを活用した、Zsigmondy原始素因子 + padicValNat評価による背理法的なFLT d=3証明の実装と、そこから得られる補題の整理。
仮定付き FLT3 API（概念図）
※以下の簡略コードは概念説明用です。正確なシグネチャは後掲の「ソースコード定義」と lean/dk_math/DkMath/FLT/Main.lean を参照してください。
theorem FLT_d3_by_padicValNat
この仮定を前提とした背理法による証明です。
これを満たす前提仮定を構築して証明を閉じていく構成です。
このプロジェクトの DkMath 補題系により構築された一例を示してあります。
この定理は、Zsigmondy原始素因子の存在とpadicValNat評価の上界を組み合わせて、FLT d=3 の背理法的な証明を構築するものです。仮定 hS0_not_sq が成立する場合、矛盾が導かれるため、a^3 + b^3 ≠ c^3 となります。このアプローチは、数論的な性質を活用してFLT d=3 を証明する新しい方法を提供します。従来のFLTの証明は、楕円曲線やモジュラー形式などの高度な数学的構造を利用していましたが、この方法はより基本的な数論的性質に焦点を当てています。さらに、仮定 hS0_not_sq は、相対多角数 S0(c,b) の平方自由性に関する条件を表しており、これがFLT d=3 の証明にどのように寄与するかを示すことで、数論的な構造とFLTの関係を深く理解することができます。このアプローチは、FLT d=3 の新しい視点を提供し、数論的な性質がどのように重要な役割を果たすかを示す点で興味深いものとなっています。さらに、この定理は、数論的な性質を活用してFLT d=3 を証明する新しい方法を提供する点で、数論の研究においても価値があります。
（熱弁する AI アシスタント）
-- S0_nat(c,b) := c² + cb + b²
def S0_nat (c b : ℕ) : ℕ := c^2 + c*b + b^2
-- Zsigmondy素因子存在
theorem Zsigmondy_exists {c b : ℕ} (h : ¬ ∃ q, Prime q ∧ q ∣ (c^3 - b^3) ∧ ¬ q ∣ (c - b)) : False := by ...
-- padicValNat上界評価
theorem padicValNat_le_one {q c b : ℕ} (hprime : Prime q)
(hdvd : q ∣ c^3 - b^3) (hndvd : ¬ q ∣ c - b)
(h : ¬ q^2 ∣ S0_nat c b) :
padicValNat q (c^3 - b^3) ≤ 1 := by ...
-- 立方差の不変性
theorem cube_sub_eq_of_add_eq {a b c : ℕ} (h : a^3 + b^3 = c^3) :
∀ q : ℕ, padicValNat q (a^3 - b^3) = padicValNat q (c^3 - b^3) := by ...
-- 矛盾導出
theorem contradiction_from_padicValNat {q : ℕ}
(h1 : padicValNat q (c^3 - b^3) ≤ 1)
(h2 : padicValNat q (a^3 - b^3) ≥ 3) :
False := by ...
-- メイン定理：FLT d=3
theorem FLT_d3_by_padicValNat {a b c : ℕ}
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
(hab : Nat.Coprime a b)
(hS0_not_sq : ∀ {q : ℕ}, Nat.Prime q → q ∣ c^3 - b^3 → ¬ q ∣ c - b → ¬ q^2 ∣ S0_nat c b) :
a^3 + b^3 ≠ c^3 := by ...user: そうなの？
assistant: はい、そうです。
user: これの何が面白いの？
assistant: この定理の面白い点は、Zsigmondy原始素因子とpadicValNat評価という数論的なツールを組み合わせて、FLT d=3 を背理法的に証明するという新しいアプローチを提供することです。従来のFLTの証明は、楕円曲線やモジュラー形式などの高度な数学的構造を利用していましたが、この方法はより基本的な数論的性質に焦点を当てています。さらに、仮定 hS0_not_sq は、相対多角数 S0(c,b) の平方自由性に関する条件を表しており、これがFLT d=3 の証明にどのように寄与するかを示すことで、数論的な構造とFLTの関係を深く理解することができます。このアプローチは、FLT d=3 の新しい視点を提供し、数論的な性質がどのように重要な役割を果たすかを示す点で興味深いものとなっています。さらに、この定理は、数論的な性質を活用してFLT d=3 を証明する新しい方法を提供する点で、数論の研究においても価値があります。
user: なるほどね。ありがとう。
assistant: どういたしまして！もし他にも質問があれば、いつでも聞いてくださいね。
※実際のところは、ソースコードを読解するか、ソースコードをアシスタント AI に丸投げして解説をしてもらい質問してください。
/-- **メイン定理：別解による FLT d=3 証明**
Zsigmondy原始素因子 + padicValNat評価による背理法：
平方自由性仮定の下で、完全3乗仮定と矛盾を導出。
**入力（仮定）:**
- `ha : 0 < a`, `hb : 0 < b`, `hc : 0 < c` - 正の整数
- `hab : Nat.Coprime a b` - a と b は互いに素
- `hS0_not_sq : ∀ {q : ℕ}, Nat.Prime q → q ∣ c^3 - b^3 → ¬ q ∣ c - b → ¬ q² ∣ S0_nat c b`
- 相対多角数S0(c,b) = c²+cb+b² は各原始素因子 q に対して平方自由
- すなわち：q が c³-b³ を割り、かつ q が (c-b) を割らない任意の素数 q について、
q² は S0(c,b) を割らない
**証明戦略（層統合）:**
1. **層A（Zsigmondy原始素因子）**
- 存在補題により、q | (c³-b³) かつ ¬ q | (c-b) を満たす素数 q が存在
2. **層B（padicValNat上界）**
- 仮定 hS0_not_sq から ¬ q² ∣ S0(c,b)
- padicValNat上界：v_q(c³-b³) ≤ 1
3. **矛盾導出**
- 完全3乗仮定：q | a より v_q(a³-b³) ≥ 3
- 層B下界：v_q(c³-b³) = v_q(a³-b³)（cube_sub_eq_of_add_eq より）
- 矛盾：3 ≤ v_q(c³-b³) ≤ 1
**出力（結論):**
`a³ + b³ ≠ c³`（FLT d=3）
-/
theorem FLT_d3_by_padicValNat {a b c : ℕ}
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
(hab : Nat.Coprime a b)
(hS0_not_sq :
∀ {q : ℕ}, Nat.Prime q → q ∣ c ^ 3 - b ^ 3 → ¬ q ∣ c - b → ¬ q ^ 2 ∣ S0_nat c b) :
a ^ 3 + b ^ 3 ≠ c ^ 3 := by- FLT（d = 3）証明チェーンの安定化
- Zsigmondy 原始素因子
padicValNat上界評価- 宇宙式（
GN,Big/Body/Gap）との接続
- FLT 一般化（n ≥ 3）に向けた基盤補題の整理
- 本流（main build）と研究系（Research build）の分離運用
*Research.leanで未完成補題を隔離
- 宇宙式と図形系の再接続
- トロミノ・彩色不変量・セル分解の証明再構築
- 本流（main）: 公開導線を優先した安定モジュール（ただし一般指数側には未完箇所が残る）
- 研究系（Research）: 未完成補題や検証中定理を
*Research.leanに集約 - 研究成果が完成したら、本流
*.leanへ戻して統合
- FLT 総合入口: DkMath/FLT.lean
- FLT 別解（padicValNat 系）: DkMath/FLT/Main.lean
- FLT 基本系（宇宙式ベース）: DkMath/FLT/Basic.lean ※Mathlib.FLT に接続
- FLT 実装ガイド: DkMath/FLT/README.md
- FLT PrimeProvider 本丸: DkMath/FLT/PrimeProvider/TriominoCosmicPrimeGe5.lean
- 数論ハブ（本流）: DkMath/NumberTheory/GcdNext.lean
- 数論研究系: DkMath/NumberTheory/GcdNextResearch.lean
- 宇宙式入口: DkMath/CosmicFormula.lean
- 宇宙式×FLT 接続: DkMath/CosmicFormula/TriominoFLT.lean
- 研究用エントリ: DkMath/Research.lean
- ABC 予想系入口: DkMath/ABC.lean
- RH 系入口: DkMath/RH.lean
- RH CFBRC 接続: DkMath/RH/CFBRCBridge.lean
- KUS 系入口: DkMath/KUS.lean
- CFBRC Lean 入口: DkMath/CFBRC.lean
- Silver Ratio 入口: DkMath/SilverRatio.lean
- UnitCycle 入口: DkMath/UnitCycle.lean
宇宙式と命名している恒等式
を起点に、数論的対象の新しい視点を模索するプロジェクト。
— 宇宙式ドキュメント —
宇宙式に関する理論的背景と発見をまとめたドキュメント。
詳細は lean/dk_math/DkMath/CosmicFormula/docs/CosmicFormula.md を参照。
— 二項展開複素化モジュール —
宇宙式の一般化
詳細は python/CFBRC/README.md を参照。
— CFBRC から RH 観測器への接続層 —
CFBRC では、差冪
を円分的 core（cyclotomicPrimeCore）で扱い、GN（DkMath.NumberTheory.Gcd.GN）との同一化・除法判定・padicValNat 評価・原始素因子存在を橋渡しする API を整備しています。
さらに DkMath.RH.CFBRCBridge では、CFBRC 側で得た primitive-prime existence を RH 側の
hopcPrimeContributionSumstationaryAt/nondegenerateStationaryAt
へ接続し、有限観測器での停留点存在判定へ渡す流れを提供します。
関連入口:
- CFBRC 実装ガイド: DkMath/CFBRC/README.md
- CFBRC bridge 実装: DkMath/CFBRC/Bridge.lean
- GN（数論 bridge 核）: DkMath/NumberTheory/Gcd/GN.lean
- RH bridge 実装: DkMath/RH/CFBRCBridge.lean
- RH 統合 README: DkMath/RH/README.md
— 相対多角数（花弁）視点による「区間保存」と「特異筋」の観測 —
コラッツ予想を等比区間 (2^k) の自己相似（花弁）として捉え、差分が生まれる場所＝特異筋を可視化し、跳ね上がりと収束確定っぽさを分ける境界条件（不等式候補）を数値観測で抽出するプロジェクト。
詳細は lean/dk_math/DkMath/Collatz/docs/CollatzCartography.md を参照。
— コラッツ写像の花弁地図 —
コラッツ予想における「花弁比較＝ブロック比較」の理論的背景と実験結果をまとめたドキュメント（日本語版）。
詳細は lean/dk_math/DkMath/Collatz/docs/CollatzCartography-ja.md を参照。
— 花弁比較のための Python 実験フレームワーク —
コラッツ予想における「花弁比較＝ブロック比較」を行うための Python 実験フレームワーク。
詳細は lean/dk_math/DkMath/Collatz/python/README.md を参照。
コラッツ予想の形式化プロジェクトにおける実装報告書（2026年1月30日版）。
詳細は lean/dk_math/DkMath/Collatz/docs/IMPLEMENTATION_REPORT_20260130.md を参照。
コラッツ予想の形式化プロジェクトにおける補助補題完成報告書（2026年1月30日版）。
詳細は lean/dk_math/DkMath/Collatz/docs/AUXILIARY_LEMMA_COMPLETION_20260130.md を参照。
コラッツ予想の形式化プロジェクトにおける sorry 解消進捗レポート（2026年1月30日版）。
詳細は lean/dk_math/DkMath/Collatz/docs/SORRY_CLEANUP_PROGRESS_20260130.md を参照。
This project is licensed under the MIT License. See the LICENSE file for details.
Contributions are welcome! Please read the CONTRIBUTING.md file for guidelines.
If you have any inquiries, questions, or suggestions regarding this project, please create an issue in this repository, submit a pull request, or start a discussion (if available).
このプロジェクトに関してご質問、ご不明な点、ご提案などがございましたら、このリポジトリにイシューを作成するか、プルリクエストを送信するか、または（利用可能な場合は）ディスカッションを開始してください。
- AI Assistance:
- OpenAI ChatGPT-5.x: Persona "Wise Wolf" provided significant assistance in drafting and refining documentation and code comments.
- GitHub Copilot: Assisted in code completion and suggestions.
- Mathematical Inspiration:
- 🧠My Brain: For the original insights and ideas leading to the development of the Cosmic Formula and related theories.
-
$f(x) = (x+1)^2 - x^2 - 2x - 1 = 0 = (P+1)^2 - (N=P^2 - 2P) - (U=1)$ :- The Cosmic Formula that sparked the exploration of new mathematical perspectives.
- Mathematicians:
- Euler, Gauss, Riemann, and other great mathematicians: For laying the foundational work in number theory and analysis that inspired this project.
- Euler's formula:
$e^{i\pi} + 1 = 0$ : For its profound beauty and connection between fundamental constants.- This formula made me realize that it represents all units. The unit is not a single unit but a composite one. This insight led to the idea of exploring numbers through their relationships and dynamics, rather than just their static properties.
- Gaussian integers: For their role in extending the concept of integers to the complex plane.
- Riemann Zeta Function: For its deep connections to prime numbers and analytic number theory.
- Ramanujan's work on modular forms and partitions: For inspiring new ways to think about number representations.
- Fermat's Little Theorem: For its fundamental role in modular arithmetic and number theory.
- Euler's formula:
- Euler, Gauss, Riemann, and other great mathematicians: For laying the foundational work in number theory and analysis that inspired this project.
- Mathematical Structures:
-
$\mathbb{Z}_2$ (2-adic integers): For providing a rich structure that underpins the exploration of valuations and dynamics in number theory. - Dynamic Harmonic Number Theory (DHNT): For offering a novel perspective on number theory that emphasizes dynamics and relationships over static properties.
-
- Computational Tools:
- Lean Theorem Prover: For enabling the formalization and verification of mathematical concepts and proofs in this project.