新規性調査・形式検証レポート（2026年9月13日、Codexによる）
評価：同値そのものは証明済み。新規性・初出は未確定。既知の生成閉包法とvon Staudt–Clausenから得られる正確な再定式化、およびそのLean形式化として記録する。Toda primeの一般存在やD(2m)＝mの不存在を証明したという評価ではない。
先行研究との対応
-
Greg Martinの2018年4月15日のMathOverflow回答は、3,5から始め、既出素数の積の4倍の約数に1を足して新しい素数を取り込む反復を述べ、この反復の無限性がToda存在問題を解決することを指摘する。今回の生成閉包の基本手法は既出である。同回答にBernoulli固定点との同値の明記は見つからなかった。
https://mathoverflow.net/questions/297915/number-theory-question-from-homotopy-groups-of-spheres
-
Mees de Vriesの2021年6月27日の回答（7月4日改訂）のDownward/upward saturated節には、素数を追加するsaturation操作と、結果がsaturatedな倍数を割る性質がある。末尾には4の倍数のsaturated numberが存在しそうにないとの観察もある。4からこの操作を始め、各奇素数を一度だけ掛ければ、Toda反例がある場合には4Nで停止する。von Staudt–ClausenによりD(4N)＝2Nとなるため、今回の同値はこの既知の方法と古典定理から短く導ける。
https://math.stackexchange.com/a/4184376
-
OEIS A345765は、全素数pについてp∣s ⇔ p−1∣sを満たす整数を扱う。McKeanのToda primes §5.1はToda primeとBernoulli分母の関係を扱う。確認したこれらの本文には、D(2m)＝mの不存在との同値の明記は見つからなかった。
https://oeis.org/A345765
https://arxiv.org/html/2511.19744v1#S5.SS1
-
Kellner（2005）, The equation denom(B_n)=n has only one solution, Theorem 2.1はD(m)＝mの唯一の解が1806であることを証明する。D(2m)＝mとは異なる方程式であり、Toda存在問題の解決にそのまま使うことはできない。
https://www.bernoulli.org/~bk/denombneqn.pdf
調査範囲と限界
公開ウェブでToda、Bernoulli denominator fixed point、saturated numbers、D_(2n)=n等を組み合わせて検索し、上記一次資料と著者サイトの現行Toda PDFを確認した。SUMIRE内もToda、Tominaga、Bernoulli、4nで検索し、同内容の登録は見つからなかった。OEIS A106741から辿った2012年NMBRTHRY投稿はログイン案内しか取得できず、本文未確認である。検索に見つからないことは不存在の証明ではなく、未索引資料・私信・未取得資料に同じ式がある可能性は残る。
https://oeis.org/A106741
https://shmckean.github.io/research/toda.pdf
再現条件と検証対象
Lean: leanprover/lean4:v4.30.0
mathlib commit: c5ea00351c28e24afc9f0f84379aa41082b1188f
https://github.com/leanprover-community/mathlib4/tree/c5ea00351c28e24afc9f0f84379aa41082b1188f
以下のソースをTodaFixedPointEquivalence.leanとして保存し、このmathlibを導入したプロジェクトで lake env lean TodaFixedPointEquivalence.lean を実行する。2026年9月13日の再実行は終了コード0だった。
最終定理: TodaFixedPointEquivalence.existence_iff_no_fixed_point
依存公理: propext, Classical.choice, Quot.sound のみ。sorry、admit、独自公理、native_decideは使っていない。mathlibの実際のbernoulliとBernoulli.vonStaudt_clausenを使い、分母を別の定義に置き換えてはいない。
コード中の補助定理を含めて単独実行できる。固定点の不存在そのもの、および固定点の一意性はこの最終定理の結論に含まれない。
ソース: TodaFixedPointEquivalence.lean
SHA-256: b92ba0ffa9aa53f6b3738b90a738e761f05beec32cd88f86266cf177b5bc0e3a
----- BEGIN TodaFixedPointEquivalence.lean -----
import Mathlib
/-! An exact inductive-closure reduction of the one-Toda-prime conjecture.
The infinitude appearing on the right-hand side is not proved here. -/
namespace TodaClosure
def Toda (n p : ℕ) : Prop :=
Nat.Prime p ∧ p ≠ 2 ∧ (p - 1) ∣ 4 * n ∧ ¬ p ∣ n
inductive Generated : ℕ → Prop
| step (p : ℕ) (s : Finset ℕ) (hp : Nat.Prime p) (hodd : p ≠ 2)
(hs : ∀ q ∈ s, Generated q) (hpred : (p - 1) ∣ 4 * s.prod id) : Generated p
theorem generated_prime {p : ℕ} (hp : Generated p) : Nat.Prime p := by
cases hp with
| step p s hprime hodd hs hpred => exact hprime
theorem prime_product_dvd {s : Finset ℕ} {n : ℕ}
(hp : ∀ p ∈ s, Nat.Prime p) (hd : ∀ p ∈ s, p ∣ n) : s.prod id ∣ n := by
have hcop : (s : Set ℕ).Pairwise (Function.onFun Nat.Coprime id) := by
intro p hps q hqs hpq
exact (Nat.coprime_primes (hp p hps) (hp q hqs)).mpr hpq
rw [← Finset.lcm_eq_prod hcop]
exact Finset.lcm_dvd hd
/-- Every generated prime must divide any number lacking Toda primes. -/
theorem generated_dvd_of_no_toda {n p : ℕ} (hbad : ∀ q, ¬ Toda n q)
(hp : Generated p) : p ∣ n := by
induction hp with
| step p s hp hodd hs hpred ih =>
have hprod : s.prod id ∣ n :=
prime_product_dvd (fun q hq => generated_prime (hs q hq)) ih
have hpn : (p - 1) ∣ 4 * n :=
dvd_trans hpred (mul_dvd_mul_left 4 hprod)
by_contra hnot
exact hbad p ⟨hp, hodd, hpn, hnot⟩
/-- A positive counterexample forces the entire generated set to be finite. -/
theorem finite_generated_of_counterexample {n : ℕ} (hn : 0 < n)
(hbad : ∀ q, ¬ Toda n q) : Set.Finite {p | Generated p} := by
apply (n.divisors.finite_toSet).subset
intro p hp
exact Nat.mem_divisors.mpr ⟨generated_dvd_of_no_toda hbad hp, Nat.ne_of_gt hn⟩
/-- If the generated set is finite, its product is a positive counterexample. -/
theorem counterexample_of_finite_generated (hf : Set.Finite {p | Generated p}) :
∃ n, 0 < n ∧ ∀ p, ¬ Toda n p := by
classical
let s := hf.toFinset
have hs : ∀ p, p ∈ s ↔ Generated p := by
intro p
exact hf.mem_toFinset
refine ⟨s.prod id, ?, ?⟩
· exact Finset.prod_pos (fun p hp => (generated_prime ((hs p).mp hp)).pos)
· intro p ht
obtain ⟨hp, hodd, hpred, hnot⟩ := ht
have hgen : Generated p :=
Generated.step p s hp hodd (fun q hq => (hs q).mp hq) hpred
exact hnot (Finset.dvd_prod_of_mem id ((hs p).mpr hgen))
/-- Exact equivalence; the infinitude is the still-unproved assertion. -/
theorem existence_iff_generated_infinite :
(∀ n, 0 < n → ∃ p, Toda n p) ↔ Set.Infinite {p | Generated p} := by
constructor
· intro hex hfinite
obtain ⟨n, hn, hbad⟩ := counterexample_of_finite_generated hfinite
obtain ⟨p, hp⟩ := hex n hn
exact hbad p hp
· intro hinf n hn
by_contra hnone
have hbad : ∀ p, ¬ Toda n p := by simpa only [not_exists] using hnone
exact hinf (finite_generated_of_counterexample hn hbad)
/-- If counterexamples exist, one counterexample divides every counterexample.
The number is the product of the entire generated set. -/
theorem common_core_of_counterexample {n : ℕ} (hn : 0 < n)
(hbad : ∀ p, ¬ Toda n p) :
∃ N, 0 < N ∧ (∀ p, ¬ Toda N p) ∧
∀ m, (∀ p, ¬ Toda m p) → N ∣ m := by
classical
have hf := finite_generated_of_counterexample hn hbad
let s := hf.toFinset
have hs : ∀ p, p ∈ s ↔ Generated p := by
intro p
exact hf.mem_toFinset
refine ⟨s.prod id, ?, ?, ?_⟩
· exact Finset.prod_pos (fun p hp => (generated_prime ((hs p).mp hp)).pos)
· intro p ht
have hg : Generated p := Generated.step p s ht.1 ht.2.1
(fun q hq => (hs q).mp hq) ht.2.2.1
exact ht.2.2.2 (Finset.dvd_prod_of_mem id ((hs p).mpr hg))
· intro m hm
apply prime_product_dvd
· intro p hp
exact generated_prime ((hs p).mp hp)
· intro p hp
exact generated_dvd_of_no_toda hm ((hs p).mp hp)
end TodaClosure
namespace TodaBernoulliBridge
theorem prime_dvd_den_predecessor (k p : ℕ) (hp : Nat.Prime p)
(hd : p ∣ (bernoulli (2k)).den) : p-1 ∣ 2k := by
let S := (Finset.range (2k+2)).filter (fun q => Nat.Prime q ∧ q-1 ∣ 2k)
let Q : ℚ := ∑ q ∈ S, (1 : ℚ)/q
have hv : bernoulli (2k) + Q ∈ Set.range Int.cast := Bernoulli.vonStaudt_clausen k
obtain ⟨z, hz⟩ := hv
have heq : bernoulli (2k) = (z : ℚ) - Q := by linarith
have hdQ : p ∣ Q.den := by simpa only [heq, Rat.intCast_sub_den] using hd
have hprod : p ∣ ∏ q ∈ S, ((1 : ℚ)/q).den :=
dvd_trans hdQ (Finset.Rat.den_sum_dvd_prod_den S (fun q => (1 : ℚ)/q))
obtain ⟨q, hq, hdiv⟩ := (hp.prime.dvd_finsetProd_iff (fun q : ℕ => ((1 : ℚ)/q).den)).mp hprod
have hqprime : Nat.Prime q := (Finset.mem_filter.mp hq).2.1
have hqden : ((1 : ℚ)/q).den = q := by
simpa only [one_div] using Rat.inv_natCast_den_of_pos hqprime.pos
rw [hqden] at hdiv
have heqpq : p = q := (Nat.prime_dvd_prime_iff_eq hp hqprime).mp hdiv
simpa only [heqpq] using (Finset.mem_filter.mp hq).2.2
theorem predecessor_dvd_den {k p : ℕ} (hk : 0 < k) (hp : Nat.Prime p)
(hd : p-1 ∣ 2k) : p ∣ (bernoulli (2k)).den := by
classical
let S := (Finset.range (2k+2)).filter (fun q => Nat.Prime q ∧ q-1 ∣ 2k)
let Q : ℚ := ∑ q ∈ S, (1 : ℚ)/q
let R : ℚ := ∑ q ∈ S.erase p, (1 : ℚ)/q
have hmem : p ∈ S := by
apply Finset.mem_filter.mpr
refine ⟨Finset.mem_range.mpr ?_, hp, hd⟩
have := Nat.le_of_dvd (by omega : 0 < 2k) hd
omega
have hsum : (1 : ℚ)/p + R = Q := Finset.add_sum_erase S (fun q : ℕ => (1 : ℚ)/q) hmem
have hrest : ¬ p ∣ R.den := by
intro h
have hprod := dvd_trans h (Finset.Rat.den_sum_dvd_prod_den (S.erase p) (fun q => (1 : ℚ)/q))
obtain ⟨q,hq,hdiv⟩ := (hp.prime.dvd_finsetProd_iff (fun q : ℕ => ((1 : ℚ)/q).den)).mp hprod
have hprime := (Finset.mem_filter.mp (Finset.mem_erase.mp hq).2).2.1
have hqden : ((1 : ℚ)/q).den = q := by simp [hprime.ne_zero]
rw [hqden] at hdiv
have heq := (Nat.prime_dvd_prime_iff_eq hp hprime).mp hdiv
exact (Finset.mem_erase.mp hq).1 heq.symm
have hQ : p ∣ Q.den := by
have heq : (1 : ℚ)/p = Q-R := by linarith
have hdiv : p ∣ (Q-R).den := by rw [← heq]; simp [hp.ne_zero]
have hh := hp.dvd_mul.mp (dvd_trans hdiv (Rat.sub_den_dvd Q R))
exact hh.resolve_right hrest
obtain ⟨z,hz⟩ := (show bernoulli (2k) + Q ∈ Set.range Int.cast from Bernoulli.vonStaudt_clausen k)
have heq : bernoulli (2*k) = (z : ℚ)-Q := by linarith
simpa only [heq, Rat.intCast_sub_den] using hQ
theorem prime_dvd_den_iff {k p : ℕ} (hk : 0 < k) (hp : Nat.Prime p) :
p ∣ (bernoulli (2k)).den ↔ p-1 ∣ 2k :=
⟨prime_dvd_den_predecessor k p hp, predecessor_dvd_den hk hp⟩
def Toda (n p : ℕ) : Prop :=
Nat.Prime p ∧ p ≠ 2 ∧ p-1 ∣ 4*n ∧ ¬p ∣ n
theorem toda_iff_den {n p : ℕ} (hn : 0 < n) :
Toda n p ↔ Nat.Prime p ∧ p ≠ 2 ∧ p ∣ (bernoulli (4n)).den ∧ ¬p ∣ n := by
unfold Toda
by_cases hp : Nat.Prime p
· have hh := prime_dvd_den_iff (by omega : 0 < 2n) hp
rw [show 2*(2n)=4n by ring] at hh
rw [hh]
· simp [hp]
theorem no_toda_of_den_eq {n : ℕ} (hn : 0 < n)
(hden : (bernoulli (4n)).den = 2n) : ∀ p, ¬ Toda n p := by
intro p ht
obtain ⟨hp,hodd,hd,hnot⟩ := (toda_iff_den hn).mp ht
rw [hden] at hd
rcases hp.dvd_mul.mp hd with htwo | hn'
· exact hodd ((Nat.dvd_prime Nat.prime_two).mp htwo |>.resolve_left hp.ne_one)
· exact hnot hn'
theorem fixed_point_gives_counterexample {m : ℕ} (hm : 0 < m)
(hfix : (bernoulli (2m)).den = m) :
∃ n, 0 < n ∧ ∀ p, ¬ Toda n p := by
have htwo : 2 ∣ m := by
rw [← hfix]
exact predecessor_dvd_den hm Nat.prime_two (by norm_num)
obtain ⟨n,hn⟩ := htwo
have hnpos : 0 < n := by omega
refine ⟨n, hnpos, no_toda_of_den_eq hnpos ?_⟩
rw [hn] at hfix
simpa only [show 2(2n)=4n by ring] using hfix
theorem existence_implies_no_fixed_point
(hex : ∀ n, 0 < n → ∃ p, Toda n p) :
∀ m, 0 < m → (bernoulli (2*m)).den ≠ m := by
intro m hm hf
obtain ⟨n,hn,hbad⟩ := fixed_point_gives_counterexample hm hf
obtain ⟨p,hp⟩ := hex n hn
exact hbad p hp
theorem no_toda_iff_den_dvd {n : ℕ} (hn : 0 < n) :
(∀ p, ¬ Toda n p) ↔ (bernoulli (4n)).den ∣ 2n := by
classical
constructor
· intro hbad
let S := (Finset.range (4n+2)).filter (fun p => Nat.Prime p ∧ p-1 ∣ 4n)
let Q : ℚ := ∑ p ∈ S, (1 : ℚ)/p
have hv : bernoulli (4n) + Q ∈ Set.range Int.cast := by
simpa only [show 2(2n)=4n by ring] using Bernoulli.vonStaudt_clausen (2n)
obtain ⟨z,hz⟩ := hv
have heq : bernoulli (4n) = (z : ℚ)-Q := by linarith
have hden : (bernoulli (4*n)).den ∣ S.prod id := by
rw [heq, Rat.intCast_sub_den]
have hh := Finset.Rat.den_sum_dvd_prod_den S (fun p => (1 : ℚ)/p)
have hprod : (∏ p ∈ S, ((1 : ℚ)/p).den) = S.prod id := by
apply Finset.prod_congr rfl
intro p hp
have hprime := (Finset.mem_filter.mp hp).2.1
simp [hprime.ne_zero]
rwa [hprod] at hh
apply dvd_trans hden
have hcop : (S : Set ℕ).Pairwise (Function.onFun Nat.Coprime id) := by
intro p hp q hq hne
exact (Nat.coprime_primes (Finset.mem_filter.mp hp).2.1
(Finset.mem_filter.mp hq).2.1).mpr hne
rw [← Finset.lcm_eq_prod hcop]
apply Finset.lcm_dvd
intro p hp
obtain ⟨hprime,hpred⟩ := (Finset.mem_filter.mp hp).2
by_cases ht : p=2
· simp [ht]
· have hd : p ∣ n := by
by_contra hh
exact hbad p ⟨hprime,ht,hpred,hh⟩
exact dvd_mul_of_dvd_right hd 2
· intro hden p ht
obtain ⟨hp,hodd,hd,hnot⟩ := (toda_iff_den hn).mp ht
rcases hp.dvd_mul.mp (dvd_trans hd hden) with htwo | hn'
· exact hodd ((Nat.dvd_prime Nat.prime_two).mp htwo |>.resolve_left hp.ne_one)
· exact hnot hn'
theorem existence_iff_den_not_dvd {n : ℕ} (hn : 0 < n) :
(∃ p, Toda n p) ↔ ¬ (bernoulli (4n)).den ∣ 2n := by
have hh := no_toda_iff_den_dvd hn
simpa only [not_forall, not_not] using not_congr hh
end TodaBernoulliBridge
namespace TodaFixedPointEquivalence
open TodaClosure
theorem finite_closure_gives_fixed_point (hf : Set.Finite {p | Generated p}) :
∃ m, 0 < m ∧ (bernoulli (2m)).den = m := by
classical
let s := hf.toFinset
let N := s.prod id
have hs : ∀ p, p ∈ s ↔ Generated p := fun p => hf.mem_toFinset
have hN : 0 < N := Finset.prod_pos (fun p hp => (generated_prime ((hs p).mp hp)).pos)
have hnot2 : 2 ∉ s := by
intro h
cases (hs 2).mp h with
| step p t hp hodd ht hd => exact hodd rfl
have hbad : ∀ p, ¬ TodaBernoulliBridge.Toda N p := by
intro p hp
have hg := Generated.step p s hp.1 hp.2.1 (fun q hq => (hs q).mp hq) hp.2.2.1
exact hp.2.2.2 (Finset.dvd_prod_of_mem id ((hs p).mpr hg))
have hu : (bernoulli (4N)).den ∣ 2N :=
(TodaBernoulliBridge.no_toda_iff_den_dvd hN).mp hbad
have hl : 2N ∣ (bernoulli (4N)).den := by
have hprod : (insert 2 s).prod id = 2N := by simp [Finset.prod_insert hnot2, N]
rw [← hprod]
apply prime_product_dvd
· intro p hp
rcases Finset.mem_insert.mp hp with rfl | hp
· exact Nat.prime_two
· exact generated_prime ((hs p).mp hp)
· intro p hp
have hprime : Nat.Prime p := by
rcases Finset.mem_insert.mp hp with rfl | hp
· exact Nat.prime_two
· exact generated_prime ((hs p).mp hp)
have hcriterion := TodaBernoulliBridge.prime_dvd_den_iff (by omega : 0 < 2N) hprime
rw [show 2(2N)=4N by ring] at hcriterion
apply hcriterion.mpr
rcases Finset.mem_insert.mp hp with rfl | hp
· norm_num
· cases (hs p).mp hp with
| step p t hp hodd ht hd =>
have hsub : t ⊆ s := fun q hq => (hs q).mpr (ht q hq)
have htdiv : t.prod id ∣ N := Finset.prod_dvd_prod_of_subset t s id hsub
exact dvd_trans hd (mul_dvd_mul_left 4 htdiv)
refine ⟨2N, by omega, ?_⟩
rw [show 2(2N)=4N by ring]
exact Nat.dvd_antisymm hu hl
theorem existence_iff_no_fixed_point :
(∀ n, 0 < n → ∃ p, TodaClosure.Toda n p) ↔
(∀ m, 0 < m → (bernoulli (2*m)).den ≠ m) := by
constructor
· exact TodaBernoulliBridge.existence_implies_no_fixed_point
· intro hnone
apply TodaClosure.existence_iff_generated_infinite.mpr
intro hf
obtain ⟨m,hm,hfix⟩ := finite_closure_gives_fixed_point hf
exact hnone m hm hfix
end TodaFixedPointEquivalence
#print axioms TodaFixedPointEquivalence.existence_iff_no_fixed_point
----- END TodaFixedPointEquivalence.lean -----
コメント (0)