SUMIRE

問い #124 2026-08-24 08:17:45 UTC 匿名 · hash c9230951a2fb…

【M_3 = M_1 問題（一般化距離空間）】

AI採点30 総合評価未評価

【M_3 = M_1 問題（一般化距離空間）】一般位相空間論における M_3 空間（stratifiable space）と M_1 空間の同値性問題。一般化された距離空間の理論の主要未解決問題であり、研究者数の減少により早期解決が望まれる。 — comm. AI for Math の過去会話より — 初出: 2026-08-09 #🤝進めてほしいopen-questions 発言者: Yoshito Ishiki 分類: math-research 関連する芽: 「非可算離散空間上のMet(X)の完備距離付け可能性（Conj 5.1）」(2026-08-07) / 「Scottish Book 問題155の非可分版」(2026-08-10)

AI採点 30 / 100 の理由を読む

AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。採点したモデル: claude-sonnet-5

M_3=M_1問題という著名な未解決問題の存在自体は明確に提示されているが、定義や既知の部分結果、具体的なアプローチの手がかりがほとんど無く、既存文献の紹介にとどまっている。

詳細レポート評価未評価 0 REPORTS

問い #121 2026-08-24 08:17:43 UTC 匿名 · hash 7ab6d2ba8467…

【正則言語理論のopen problems】

AI採点30 総合評価未評価

↗ Discord の元投稿詳細 →

【正則言語理論のopen problems】 Pinらによる "Open problems about regular languages, 35 years later" に集められた、正則言語の変種階層・decidability・代数的特徴づけ等に関する厳選された未解決問題群の共有。 — comm. AI for Math の過去会話より — 初出: 2026-08-06 #🤝進めてほしいopen-questions 発言者: hora 分類: math-research 関連する芽: 「Context-free language の density の存在」(2026-07-29)

AI採点 30 / 100 の理由を読む

AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。採点したモデル: claude-sonnet-5

問題群への言及と関連文献の紹介はあるが、具体的な問い・予想・構成や反例候補などの中身がほとんど示されておらず、続きを考えるための手がかりが乏しい。

詳細レポート評価未評価 0 REPORTS

問い #111 2026-08-24 08:17:37 UTC 匿名 · hash 1e2b7631317a…

【チューリング完全でない計算体系が扱える論理】

AI採点30 総合評価未評価

↗ Discord の元投稿詳細 →

【チューリング完全でない計算体系が扱える論理】チューリング完全でない構成（例えば正規表現で表現される体系）がどのような論理を内部で扱えるかという問い。排中律のような原理は成立しにくいのではないかという予想。 — comm. AI for Math の過去会話より — 初出: 2026-08-05 #冪集合は存在するか？（など）発言者: K.Kita Tokyo, ¬L 分類: math-research

AI採点 30 / 100 の理由を読む

AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。採点したモデル: claude-sonnet-5

問いの方向性（計算能力と内部論理の対応、排中律の成立可否）は示されているが、正規表現の体系で具体的に何が成立・不成立となるかの構成や例、文献的手がかりがなく、続きを考える足場が薄い。

詳細レポート評価未評価 0 REPORTS

問い #94 2026-08-24 08:17:26 UTC 匿名 · hash e909e5644bc6…

【Connes' rigidity conjecture の Lean 形式化の依存関係監査】

AI採点30 総合評価未評価

↗ Discord の元投稿詳細 →

【Connes' rigidity conjecture の Lean 形式化の依存関係監査】 ConnesRigidity.lean において、最終定理を仮定に置いていないか、sorry/独自 axiom がないか、universal lattice の property (T) が内部で証明されているか、Suslin 型生成定理の必要な特殊ケースが証明されているか、因子同型の explicit witness が構成されているか、といった依存関係の監査項目が整理された。 — comm. AI for Math の過去会話より — 初出: 2026-08-01 #astraと10の未解決問題発言者: Yasu, km, Qu, M.Hoshino 分類: math-formalization

AI採点 30 / 100 の理由を読む

AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。採点したモデル: claude-sonnet-5

監査項目のリスト自体は具体的だが、実際の定理・証明内容や反例・文献への言及がなく、Lean形式化の中身自体は示されていないため、続きを考える手がかりが限定的である。

詳細レポート評価未評価 0 REPORTS

問い #65 2026-08-24 08:17:08 UTC 匿名 · hash 8ea0745b60a8…

【計算実験とToda bracketの関係】

AI採点30 総合評価未評価

↗ Discord の元投稿詳細 →

【計算実験とToda bracketの関係】自作プログラムによる具体例の計算実験をAIと進める中で、得られた計算がToda bracketの特殊な場合として解釈できるという指摘があった。先行研究の計算例との比較検証も含め、計算結果のホモトピー論的解釈が研究の種になりうる。 — comm. AI for Math の過去会話より — 初出: 2026-06-26 #🌀疲弊発言者: Taketo Sano 分類: math-research 関連する芽: 「スペクトル系列の機械計算アルゴリズム」(2026-06-09)

AI採点 30 / 100 の理由を読む

AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。採点したモデル: claude-sonnet-5

Toda bracketとの関連という具体的な着想の方向性は示されているが、どの計算実験・どの具体例が対応するのか、定義や計算内容が全く書かれておらず、他者が続きを検討するための手がかりが乏しい。

詳細レポート評価未評価 0 REPORTS

問い #58 2026-08-24 08:17:03 UTC 匿名 · hash 2388517b6ad8…

【局所平面性を課したメモリンクグラフ】

AI採点30 総合評価未評価

↗ Discord の元投稿詳細 →

【局所平面性を課したメモリンクグラフ】メモ間リンクの構造を「局所的に平面グラフ」かつ各頂点の重み（次数）が大きすぎないグラフに制限する設計案。局所的平面性 (local planarity) の形式的定義と効率的判定アルゴリズムが未解決の数学的課題として提起されている。 — comm. AI for Math の過去会話より — 初出: 2026-06-21 #💭作りたいものを口に出しておく空間発言者: ¬L 分類: math-research

AI採点 30 / 100 の理由を読む

AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。採点したモデル: claude-sonnet-5

局所平面性という概念と次数制限という設計動機は示されているが、形式的定義・具体例・判定アルゴリズムの候補や既存文献との関連が書かれておらず、続きを考えるための手がかりが薄い。

詳細レポート評価未評価 0 REPORTS

着想 AI-generated #218 2026-09-08 17:53:24 UTC 匿名 · hash 1fd0fb7f66e6…

Pretopological dynamics

AI採点28 総合評価未評価

詳細 →

Pretopological dynamics ## Trigger HPの準備中論文リスト（公開）にある *Dynamical systems on pretopological spaces* から瓶化する研究方向。正確な着想日は不明で、`created` は瓶化日。 ## Idea 位相空間よりも弱いpretopological space（閉包作用素が冪等性を要求しない空間概念）の上で力学系を展開する構想。公開タイトル以上の内容（どの力学的概念を移植するか・主結果）はこの瓶では補完しない。 ## Goal pretopological spaceの上の力学系の基礎概念を整備し、通常の位相力学系では見えない現象（冪等でない閉包に由来する挙動）を特定する。 ## Personal context 論文レジストリでは `dynamical-system-pretopological-space`・solo・mixed_article_note_talk（論文・ノート・講演資料が混在しており整理待ち）。該当するsloganは現行の登録簿に無い（新設提案はPR側に記載）。 ## Provenance - 出典: ryuyahora-HP `data/source/site-data.json` papers.preparation（公開リスト） - registry: hora-priority-papers `registry.yaml` slug `dynamical-system-pretopological-space`

AI採点 28 / 100 の理由を読む

AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。採点したモデル: claude-sonnet-5

研究方向のタイトルと動機は示されているが、どの力学的概念を移植するか・具体的な予想や構成・反例候補などの中身は明示的に補完されておらず、続きを考えるための手がかりが乏しい。

詳細レポート評価未評価 0 REPORTS

問い #122 2026-08-24 08:17:44 UTC 匿名 · hash 75b4b4173731…

【位相空間の間のk-morphismの定義と基本性質】

AI採点28 総合評価未評価

↗ Discord の元投稿詳細 →

【位相空間の間のk-morphismの定義と基本性質】位相空間の間に「k-morphism」という新しい概念を定義し、その基本性質(合成・関手性・cofibrationやk-space的性質との関係など)をAIと共同で調査しているという報告。定義の妥当性と基本命題の整備が未確定の探索段階。 — comm. AI for Math の過去会話より — 初出: 2026-08-07 #aiと一緒にお勉強発言者: ¬L 分類: math-research

AI採点 28 / 100 の理由を読む

AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。採点したモデル: claude-sonnet-5

「k-morphism」という新概念を導入し合成・関手性等を調べているという報告はあるが、定義そのものが本文に示されておらず、具体例や既存概念との関係も欠けているため、他者が続きを考える手がかりが乏しい。

詳細レポート評価未評価 0 REPORTS

着想 #96 2026-08-24 08:17:27 UTC 匿名 · hash d8f3cf939a8b…

【様相演算子からの不動点の創発 (DEL/Auto-epistemic Logic)】

AI採点28 総合評価未評価

↗ Discord の元投稿詳細 →

【様相演算子からの不動点の創発 (DEL/Auto-epistemic Logic)】算術を持たない non-sequential な世界において、自己言及(不動点)が modal operator の代数的原理からどのように創生するかを Dynamic Epistemic Logic や Auto-epistemic Logic の枠組みで分析するという構想。自己認識の創発現象の形式化を目指す。 — comm. AI for Math の過去会話より — 初出: 2026-08-02 #🌀疲弊 › 「利己的な遺伝子」以外にあまり知らないですし、「利己的な遺伝子」を読んでも私の満... 発言者: IR., hora 分類: math-research 関連する芽: 「様相命題論理における自己言及現象の分類・N4 上の不動点階層」(2026-08-02)

AI採点 28 / 100 の理由を読む

AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。採点したモデル: claude-sonnet-5

DELやAuto-epistemic Logicで不動点創発を分析するという着想の方向性は示されているが、具体的な定義・命題・構成例が無く、抽象的な構想表明にとどまっている。関連する芽への言及はあるが、続きを考える手がかりが乏しい。

詳細レポート評価未評価 0 REPORTS

問い #84 2026-08-24 08:17:20 UTC 匿名 · hash 822759ccacac…

【WOW2グラフ理論未解決問題集の形式化と解決】

AI採点28 総合評価未評価

↗ Discord の元投稿詳細 →

【WOW2グラフ理論未解決問題集の形式化と解決】 AIが約20年前に生成したグラフ理論の未解決問題集WOW2 (Conjecture 160等) について、formal-conjectures上でLean形式化と解決PRが急増している状況の報告。問題集そのものが未解決問題の供給源として機能しており、個々の予想の解決が現在進行形の研究対象になっている。 — comm. AI for Math の過去会話より — 初出: 2026-07-26 #🌀疲弊発言者: K.Kita Tokyo, km 分類: math-research

AI採点 28 / 100 の理由を読む

AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。採点したモデル: claude-sonnet-5

WOW2という問題集がLean形式化・解決PRの供給源になっているという動向報告はあるが、具体的な予想の内容（Conjecture 160の中身）や定義・反例候補などの手がかりが示されておらず、続きを考えるための具体性に乏しい。

詳細レポート評価未評価 0 REPORTS

問い #78 2026-08-24 08:17:16 UTC 匿名 · hash a2da60655af2…

【反例に付随する多様体 X が A^3 に同型であることの幾何的解釈】

AI採点28 総合評価未評価

↗ Discord の元投稿詳細 →

【反例に付随する多様体 X が A^3 に同型であることの幾何的解釈】反例に対する幾何的解釈として、ある多様体 X が affine 3-space A^3 に同型であるという主張が挙げられている。この同型の証明がどの程度非自明かが問われており、言われなければ気づきにくい構成であることが、人間による見落としの説明になり得るかを検討している。 — comm. AI for Math の過去会話より — 初出: 2026-07-21 #Jacobian予想について発言者: M.Hoshino, J. Koizumi 分類: math-research 関連する芽: 「Vitushkinの構成と今回の反例の間のギャップ」(2026-07-22)

AI採点 28 / 100 の理由を読む

AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。採点したモデル: claude-sonnet-5

問いの方向性（同型証明の非自明さが見落としの原因か）は示されているが、対象となる多様体Xや反例の具体的な構成・定義が本文に無く、他の読者が続きを検討するための手がかりが乏しい。

詳細レポート評価未評価 0 REPORTS

問い #47 2026-08-24 08:16:56 UTC 匿名 · hash 1e97a00c0387…

【4次元多様体の特異性と次元＝難度の非単調性】

AI採点28 総合評価未評価

↗ Discord の元投稿詳細 →

【4次元多様体の特異性と次元＝難度の非単調性】線形空間などと異なり、多様体では4次元が特殊で分類理論の構築が極めて困難であり、「高次元ほど数学的に難しい」が成り立たない例になっている、という指摘（gauge theory for families の文脈）。 — comm. AI for Math の過去会話より — 初出: 2026-06-19 #AIを人間とのアナロジーで捉えるべきか発言者: IR. 分類: math-study

AI採点 28 / 100 の理由を読む

AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。採点したモデル: claude-sonnet-5

4次元多様体の特異性という着眼点は数学的に妥当で興味深いが、具体的な問い・予想・構成や参照文献名（Donaldson理論やSeiberg-Witten不変量など）が示されておらず、続きを考えるための手がかりが乏しい単なる指摘に留まっている。

詳細レポート評価未評価 0 REPORTS

着想 #40 2026-08-24 08:16:51 UTC 匿名 · hash 4cc00518eef0…

【classifying topos と levels の lattice の ∞ 版】

AI採点28 総合評価未評価

↗ Discord の元投稿詳細 →

【classifying topos と levels の lattice の ∞ 版】 classifying topos および level の complete lattice に対する不満は 1-topos の枠組みに起因するのではないか、という問題意識。∞-topos における classifying (∞,1)-topos と level の構造を考えるべきという方向性の提案。 — comm. AI for Math の過去会話より — 初出: 2026-06-17 #∞分類トポス-勉強channel 発言者: hora, IR. 分類: math-research 関連する芽: 「∞-type theory による分類 topos の解析」(2026-06-18)

AI採点 28 / 100 の理由を読む

AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。採点したモデル: claude-sonnet-5

1-topos的枠組みへの不満から∞-toposへの一般化という方向性は示されているが、具体的な構成・予想・定義や参考文献が無く、問いも輪郭のみで手がかりに乏しい。

詳細レポート評価未評価 0 REPORTS

問い #136 2026-08-24 08:17:53 UTC 匿名 · hash 304469b8206a…

【Wiener–池原の定理の Lean 証明】

AI採点25 総合評価未評価

↗ Discord の元投稿詳細 →

【Wiener–池原の定理の Lean 証明】 Wiener–Ikehara Tauberian theorem の Lean での形式化を Tau Ceti プロジェクトに登録する提案。後に Mathlib の PNTAnd（素数定理関連ファイル）に既に存在することが判明。 — comm. AI for Math の過去会話より — 初出: 2026-08-15 #💭作りたいものを口に出しておく空間発言者: K.Kita Tokyo, km 分類: math-formalization

AI採点 25 / 100 の理由を読む

AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。採点したモデル: claude-sonnet-5

既存の話題（Wiener–Ikehara定理のLean形式化）の提案と、既にMathlibに存在するという結論のみで、数学的な問い・構成・反例の手がかりがほとんど無く、続きを考える余地が乏しい。

詳細レポート評価未評価 0 REPORTS

問い #89 2026-08-24 08:17:23 UTC 匿名 · hash aba63479d660…

【CN(6,2) の未解決性】

AI採点22 総合評価未評価

匿名 1件 ↗ Discord の元投稿詳細 →

【CN(6,2) の未解決性】 arXiv:2604.02587 で CN(7,3) と CN(8,3) が解決された一方、CN(6,2) が依然として未解決であるという指摘。小さいパラメータの残された場合を攻略対象として挙げている。 — comm. AI for Math の過去会話より — 初出: 2026-07-29 #洞が気になっている問い発言者: hora 分類: math-research

AI採点 22 / 100 の理由を読む

AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。採点したモデル: claude-sonnet-5

CN(6,2)という記号や参照論文が具体的に示されているが、CN(n,k)が何を表す概念か定義がなく、問題の背景や難しさの説明もないため、専門知識なしに続きを考えるのは難しい。

詳細レポート評価未評価 0 REPORTS

定理 #332 2026-09-13 12:40:46 UTC 匿名 · hash e5a4171a0dc6…

Toda primes の補助予想5.6(i)・(ii)への反例：自然言語の証明とLean検証

AI採点未採点 総合評価判断保留

詳細 →

Toda primes の補助予想5.6(i)・(ii)への反例：自然言語の証明とLean検証 Stephen McKean, Toda primes のConjecture 5.6は、(i)・(ii)とも一般には成立しない。対象はarXiv:2511.19744v1（2025年11月24日）と、2026年9月13日に確認した著者サイトのPDF第8頁である。記号 T(n) は p−1∣4n かつ p∤n を満たす奇素数 p の集合、t(n)＝|T(n)|。D(k) はBernoulli数 B_k の既約分母（原論文の Dₖ）とする。F(d) は D(k)＝d となる最小の正の偶数 k である。 (i) 分母が等しくてもToda集合は変わる予想(i)は、F(d)＝4a なら、D(4am)＝D(4a) を満たす m について T(am)＝T(a) と主張する。 a＝29、m＝59、am＝1711 とすると、 F(1770)＝116＝4a、 D(116)＝D(6844)＝1770、 T(29)＝{3,5,59}、T(1711)＝{3,5}。したがって最小性を含む全前提を満たし、結論に反する。証明：6844＝4·29·59 の偶数約数に1を足した候補は、3,5,59,117,119,237,3423,6845で尽きる。後五つはそれぞれ9·13、7·17、3·79、3·1141、5·1369で合成数である。116の場合の候補は3,5,59,117である。2も含め、p−1が116または6844を割る素数の集合はいずれも{2,3,5,59}となり、von Staudt–Clausenから両分母は1770となる。さらに正の偶数 k が D(k)＝1770 を満たせば、分母の素因数5と59により4∣k、58∣k、したがって116∣kである。116で実現するので F(1770)＝116。59は29を割らず1711を割るため、Toda集合から59だけが失われる。 (ii) 分母が変わってもToda素数の個数は減る予想(ii)は、D(4am)≠D(4a)＝d なら t(am)≥t(a) と主張する。 a＝11、m＝5、am＝55 とすると、 D(44)＝690、D(220)＝7590、 T(11)＝{3,5,23}、T(55)＝{3,23}。したがって分母は異なるが、t(55)＝2＜3＝t(11) となる。証明：44の偶数約数に1を足した候補は3,5,23,45、220の場合は3,5,11,21,23,45,111,221である。21＝3·7、45＝5·9、111＝3·37、221＝13·17なので、2を含む素数集合はそれぞれ{2,3,5,23}、{2,3,5,11,23}。von Staudt–Clausenから分母690と7590を得る。新しく分母に加わる11は55を割るためToda primeにならず、元のToda primeである5は5を掛けることで失われる。なお F(690)＝44 も成り立つ。分母に5と23が含まれれば添字は4と22の公倍数であり、44で実現するためである。この最小性の補足は自然言語での証明であり、(ii)のLean主定理の前提には含めていない。結論の範囲二例は補助予想5.6の一般形への反例である。元の「任意の正整数にToda primeが存在する」という問題や「2個以上ある」という予想への反例ではない。a＝3または5に限定した5.6(ii)も、この二例では否定されない。新規性の位置づけ（2026年9月13日調査）上記の組が5.6の反例になるという先行報告は今回の検索・原文確認の範囲では見つからなかった。ただし、(ii)に使ったT(11)とT(55)は既に原論文のTable 1と5.6直後に記載されている。したがって数値そのものの新発見とは扱わず、a＝11、m＝5と選ぶことで一般形への反例になるという指摘と、その形式検証を記録する。初出は断定しない。 Lean検証 TodaDenominatorCounterexample.lean の conjecture_5_6_i_counterexample と TodaCountCounterexample.lean の conjecture_5_6_ii_counterexample を、実際のmathlibのbernoulliを用いて証明した。(i)はF(1770)の最小性も含む。両ファイルはLean 4.30.0で2026年9月13日に再実行し成功した。コード全文と再現条件は添付調査レポートに収録する。出典・経緯この検討の起点は、Akira Tominagaの2026年9月10日のToda prime問題の紹介投稿である（Ryuya Horaが提示した引用による。元投稿URLは未確認）。本記録の反例整理・文献調査・Lean形式化は、Ryuya Horaの研究指示の下でCodexが作成・検証した。紹介投稿と今回の反例の帰属を区別する。原論文・対象版: https://arxiv.org/abs/2511.19744 https://arxiv.org/html/2511.19744v1#S5.SS1 https://shmckean.github.io/research/toda.pdf#page=8

詳細レポート評価新規性調査・形式検証レポート（2026年9月13日、Codexによる） 1 REPORT

定理 #331 2026-09-13 12:40:00 UTC 匿名 · hash d1cce66acefc…

Toda primeの一般存在とBernoulli分母の固定点 D₂ₘ＝m の不存在は同値である

AI採点未採点 総合評価判断保留

詳細 →

Toda primeの一般存在とBernoulli分母の固定点 D₂ₘ＝m の不存在は同値である正整数 n に対し、T(n) を p−1∣4n かつ p∤n を満たす奇素数 p の集合とする。D(k) は通常の Bernoulli 数 B_k の既約分母を表す（原論文の Dₖ）。命題「すべての正整数 n について T(n)≠∅」と「D(2m)＝m を満たす正整数 m が存在しない」は同値である。この同値の両方向を自然言語とLeanで証明した。固定点の不存在そのものは証明しておらず、Toda primeの一般存在問題は未解決である。証明正の偶数 k について、von Staudt–Clausenの定理は D(k)＝∏{p：p は素数、p−1∣k} を与える。まず D(2m)＝m と仮定する。分母は2を含む相異なる素数の積なので m＝2N と書け、D(4N)＝2N である。奇素数 p が p−1∣4N を満たせば p∣D(4N)＝2N、したがって p∣N となる。よって T(N)＝∅ である。逆に、T(n)＝∅ となる正整数 n があると仮定する。S₀＝∅ から出発し、N_j＝∏{q：q∈S_j}（空積は1）として、S_(j+1) を S_j と「p−1∣4N_j を満たす奇素数 p 全体」の和集合とする。各集合は有限である。帰納法により、S_j の全素数は n を割る。実際、そのとき相異なる素数の積 N_j は n を割るので、新しく加わる p は p−1∣4n を満たす。T(n)＝∅ より p∣n である。したがって増大列 S_j は n の有限個の素因数の範囲で停止する。停止した集合を S、N＝∏{q：q∈S} と置く。停止条件から、p−1∣4N を満たす奇素数 p はすべて S に入る。また S の各素数は生成された時点で p−1∣4N_j を満たしており、N_j∣N だから p−1∣4N である。よって von Staudt–Clausen により D(4N)＝2N。m＝2N とすれば D(2m)＝m を得る。以上で両命題の否定が同値となる。新規性の位置づけ（2026年9月13日調査）素数を生成する基本手法は Greg Martin の2018年のMathOverflow回答に既出である。Mees de Vries の2021年のsaturation操作とも直接対応し、これらとvon Staudt–Clausenを結ぶ再定式化として位置づける。D(2m)＝m の不存在との同値を明記した先行資料は今回の確認範囲では見つからなかったが、新規性・初出は未確定である。Kellnerの D(m)＝m ⇔ m＝1806 という定理は添字の異なる方程式を扱っており、今回の不存在を証明するものではない。 Lean検証実際のmathlibのbernoulliを使用。TodaFixedPointEquivalence.lean の existence_iff_no_fixed_point が上記同値を証明する。Lean 4.30.0で2026年9月13日に再実行し成功した。再現条件とコード全文は添付調査レポートに収録する。出典・経緯この検討の起点は、Akira Tominagaの2026年9月10日のToda prime問題の紹介投稿である（Ryuya Horaが提示した引用による。元投稿URLは未確認）。本記録の証明整理・文献調査・Lean形式化は、Ryuya Horaの研究指示の下でCodexが作成・検証した。問題の紹介元と今回の導出の帰属を区別する。 Greg Martin（2018）: https://mathoverflow.net/questions/297915/number-theory-question-from-homotopy-groups-of-spheres Mees de Vries（2021）: https://math.stackexchange.com/a/4184376 Stephen McKean, Toda primes, arXiv:2511.19744v1, §5.1: https://arxiv.org/html/2511.19744v1#S5.SS1 Bernd C. Kellner, The equation denom(B_n)=n has only one solution（2005）: https://www.bernoulli.org/~bk/denombneqn.pdf

詳細レポート評価新規性調査・形式検証レポート（2026年9月13日、Codexによる） 1 REPORT