Merge branch 'main' into renameBusyBeaver

franzhusch · web-flow · commit 2190073cc880 · 2026-02-26T17:52:22.000+01:00
diff --git a/FormalConjectures/ErdosProblems/1067.lean b/FormalConjectures/ErdosProblems/1067.lean
@@ -65,7 +65,7 @@ Thomassen [Th17] constructed a counterexample to the version which asks for infi
 edge-connectivity (that is, to disconnect the graph requires deleting infinitely many edges).
 -/
 @[category research solved, AMS 5]
-theorem erdos_1067.variant.infinite_edge_connectivity :
+theorem erdos_1067.variants.infinite_edge_connectivity :
     answer(False) ↔ ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = ℵ_ 1 →
       ∃ (H : G.Subgraph), H.coe.chromaticCardinal = ℵ_ 1 ∧ InfinitelyEdgeConnected H.coe := by
   sorry
diff --git a/FormalConjectures/ErdosProblems/141.lean b/FormalConjectures/ErdosProblems/141.lean
@@ -80,15 +80,15 @@ theorem erdos_141 : answer(sorry) ↔
 The existence of such progressions has been verified for $k≤10$.
 -/
 @[category research solved, AMS 5 11]
-theorem erdos_141.variant.first_cases :
+theorem erdos_141.variants.first_cases :
     (∀ k ≥ 3, k ≤ 10 → ∃ (s : Set ℕ), s.IsAPAndPrimeProgressionOfLength k) := by
   sorry
 
 /--
 Are there $11$ consecutive primes in arithmetic progression?
 -/
 @[category research open, AMS 5 11]
-theorem erdos_141.variant.eleven : answer(sorry) ↔
+theorem erdos_141.variants.eleven : answer(sorry) ↔
     ∃ (s : Set ℕ), s.IsAPAndPrimeProgressionOfLength 11 := by
   sorry
 
@@ -102,15 +102,15 @@ def consecutivePrimeArithmeticProgressions (k : ℕ) : Set (Set ℕ) :=
 It is open, even for $k=3$, whether there are infinitely many such progressions.
 -/
 @[category research open, AMS 5 11]
-theorem erdos_141.variant.infinite_three : answer(sorry) ↔
+theorem erdos_141.variants.infinite_three : answer(sorry) ↔
     (consecutivePrimeArithmeticProgressions 3).Infinite := by
   sorry
 
 /--
 Fix a $k \geq 3$. Is it true that there are infinitely many arithmetic prime progressions of length $k$?
 -/
 @[category research open, AMS 5 11]
-theorem erdos_141.variant.infinite_general_case : answer(sorry) ↔
+theorem erdos_141.variants.infinite_general_case : answer(sorry) ↔
     ∀ k ≥ 3, (consecutivePrimeArithmeticProgressions k).Infinite := by
   sorry
 
diff --git a/FormalConjectures/ErdosProblems/195.lean b/FormalConjectures/ErdosProblems/195.lean
@@ -42,15 +42,15 @@ theorem erdos_195 :
 Geneson [Ge19] proved that k ≤ 5.
 -/
 @[category research solved, AMS 5]
-theorem erdos_195.variant.leq_5_bound :
+theorem erdos_195.variants.leq_5_bound :
     5 ≥ sSup {k : ℕ | ∀ f : ℤ ≃ ℤ, HasMonotoneAP f k} := by
   sorry
 
 /--
 Adenwalla [Ad22] proved that k ≤ 4.
 -/
 @[category research solved, AMS 5]
-theorem erdos_195.variant.leq_4_bound :
+theorem erdos_195.variants.leq_4_bound :
     4 ≥ sSup {k : ℕ | ∀ f : ℤ ≃ ℤ, HasMonotoneAP f k} := by
   sorry
 
diff --git a/FormalConjectures/ErdosProblems/218.lean b/FormalConjectures/ErdosProblems/218.lean
@@ -43,7 +43,7 @@ theorem erdos_218.variants.ge : {n | primeGap (n + 1) ≤ primeGap n}.HasDensity
 /--
 There are infintely many indices $n$ such that the prime gap at $n$ is equal to the prime gap
 at $n+1$. This is equivalent to the existence of infinitely many arithmetic progressions of
-length $3$, see `erdos_141.variant.infinite_three`.
+length $3$, see `erdos_141.variants.infinite_three`.
 -/
 @[category research open, AMS 11]
 theorem erdos_218.variants.infinite_equal_prime_gap : {n | primeGap n = primeGap (n + 1)}.Infinite := by
diff --git a/FormalConjectures/ErdosProblems/269.lean b/FormalConjectures/ErdosProblems/269.lean
@@ -80,7 +80,7 @@ This theorem addresses the case where the set of primes $P$ is infinite. In this
 irrational.
 -/
 @[category research solved, AMS 11]
-theorem erdos_269.variant.infinite (P : Set ℕ) (h : ∀ p ∈ P, p.Prime) (h_inf : P.Infinite) :
+theorem erdos_269.variants.infinite (P : Set ℕ) (h : ∀ p ∈ P, p.Prime) (h_inf : P.Infinite) :
   Irrational (series P) := by
   sorry
 
diff --git a/FormalConjectures/ErdosProblems/306.lean b/FormalConjectures/ErdosProblems/306.lean
@@ -44,7 +44,7 @@ Every positive integer can be expressed as an Egyptian fraction where each denom
 product of three distinct primes.
 -/
 @[category research solved, AMS 11]
-theorem erdos_306.variant.integer_three_primes (m : ℕ) (h : 0 < m) :
+theorem erdos_306.variants.integer_three_primes (m : ℕ) (h : 0 < m) :
     ∃ k > (0 : ℕ), ∃ (n : Fin (k + 1) → ℕ), n 0 = 1 ∧
     ∀ i, (hik : i < k) → n ⟨i, by omega⟩ < n ⟨(i + 1), by omega⟩ ∧
     (∀ i ∈ Finset.Icc 1 (Fin.last k), ω (n i) = 3 ∧ Ω (n i) = 3) ∧
diff --git a/FormalConjectures/ErdosProblems/313.lean b/FormalConjectures/ErdosProblems/313.lean
@@ -61,7 +61,7 @@ def IsPrimaryPseudoperfect (n : ℕ) : Prop := ∃ P, (n, P) ∈ erdos_313_solut
 It is conjectured that the set of primary pseudoperfect numbers is infinite.
 -/
 @[category research open, AMS 11]
-theorem erdos_313.variant.primary_pseudoperfect_are_infinite :
+theorem erdos_313.variants.primary_pseudoperfect_are_infinite :
     Set.Infinite {n | IsPrimaryPseudoperfect n} := by
   sorry
 
diff --git a/FormalConjectures/ErdosProblems/324.lean b/FormalConjectures/ErdosProblems/324.lean
@@ -40,7 +40,7 @@ Probably $f(x) = x^5$ has the property that the sums $f(a)+f(b)$ with
 $a < b$ nonnegative integers are distinct.
 -/
 @[category research open, AMS 11]
-theorem erdos_324.variant.quintic : {(a, b) : ℕ × ℕ | a < b}.InjOn fun (a, b) => a ^ 5 + b ^ 5 := by
+theorem erdos_324.variants.quintic : {(a, b) : ℕ × ℕ | a < b}.InjOn fun (a, b) => a ^ 5 + b ^ 5 := by
   sorry
 
 end Erdos324
diff --git a/FormalConjectures/ErdosProblems/331.lean b/FormalConjectures/ErdosProblems/331.lean
@@ -58,7 +58,7 @@ condition that $|A \cap \{1,\dots,N\}| \sim c_A N^{1/2}$ for some constant $c_A>
 for $B$.
 -/
 @[category research open, AMS 11]
-theorem erdos_331.variant.ruzsa :
+theorem erdos_331.variants.ruzsa :
     answer(sorry) ↔
       ∀ A B : Set ℕ,
       (∃ c_A > 0, (fun (n : ℕ) ↦ (count A n : ℝ)) ~[atTop] (fun (n : ℕ) ↦ c_A * (n : ℝ) ^ (1 / 2 : ℝ))) →
diff --git a/FormalConjectures/ErdosProblems/366.lean b/FormalConjectures/ErdosProblems/366.lean
@@ -43,15 +43,15 @@ theorem exists_three_full_then_two_full : (∃ n > 0, (3).Full n ∧ (2).Full (n
 Are there infinitely many 3-full $n$ such that $n+1$ is 2-full?
 -/
 @[category research open, AMS 11]
-theorem erdos_366.variant.three_two :
+theorem erdos_366.variants.three_two :
     answer(sorry) ↔ {n | (3).Full n ∧ (2).Full (n + 1)}.Infinite := by
   sorry
 
 /--
 Are there any consecutive pairs of $3$-full integers?
 -/
 @[category undergraduate, AMS 11]
-theorem erdos_366.variant.weaker : answer(sorry) ↔ ∃ n > 0, (3).Full n ∧ (3).Full (n + 1) := by
+theorem erdos_366.variants.weaker : answer(sorry) ↔ ∃ n > 0, (3).Full n ∧ (3).Full (n + 1) := by
   sorry
 
 end Erdos366
diff --git a/FormalConjectures/ErdosProblems/494.lean b/FormalConjectures/ErdosProblems/494.lean
@@ -49,12 +49,12 @@ $|A| \ne 2^l$ for $l \ge 0$.
 They also gave counterexamples when $k = 2$ and $|A| = 2^l$.
 -/
 @[category research solved, AMS 5]
-theorem erdos_494.variant.k_eq_2_card_not_pow_two :
+theorem erdos_494.variants.k_eq_2_card_not_pow_two :
     ∀ card : ℕ, (∀ l : ℕ, card ≠ 2 ^ l) → Erdos494Unique 2 card := by
   sorry
 
 @[category research solved, AMS 5]
-theorem erdos_494.variant.k_eq_2_card_pow_two :
+theorem erdos_494.variants.k_eq_2_card_pow_two :
     ∀ card : ℕ, (∃ l : ℕ, card = 2 ^ l) → ¬Erdos494Unique 2 card := by
   sorry
 
@@ -66,25 +66,25 @@ More generally, they proved that $A$ is determined by $A_k$ (and $|A|$) if $|A|$
 a prime greater than $k$.
 -/
 @[category research solved, AMS 5]
-theorem erdos_494.variant.k_eq_3_card_gt_6 :
+theorem erdos_494.variants.k_eq_3_card_gt_6 :
     ∀ card > 6, Erdos494Unique 3 card := by
   sorry
 
 @[category research solved, AMS 5]
-theorem erdos_494.variant.k_eq_4_card_gt_12 :
+theorem erdos_494.variants.k_eq_4_card_gt_12 :
     ∀ card > 12, Erdos494Unique 4 card := by
   sorry
 
 @[category research solved, AMS 5]
-theorem erdos_494.variant.card_divisible_by_prime_gt_k :
+theorem erdos_494.variants.card_divisible_by_prime_gt_k :
     ∀ (k card p : ℕ), p.Prime → k ∈ Set.Ioo 0 p → p ∣ card → Erdos494Unique k card := by
   sorry
 
 /--
 Kruyt noted that the conjecture fails when $|A| = k$, by rotating $A$ around an appropriate point.
 -/
 @[category research solved, AMS 5]
-theorem erdos_494.variant.k_eq_card :
+theorem erdos_494.variants.k_eq_card :
     ∀ k > 2, ¬Erdos494Unique k k := by
   sorry
 
@@ -93,7 +93,7 @@ Similarly, Tao noted that the conjecture fails when $|A| = 2k$, by taking $A$ to
 the total sum 0 and considering $-A$.
 -/
 @[category research solved, AMS 5]
-theorem erdos_494.variant.card_eq_2k :
+theorem erdos_494.variants.card_eq_2k :
     ∀ k > 2, ¬Erdos494Unique k (2 * k) := by
   sorry
 
@@ -102,7 +102,7 @@ Gordon, Fraenkel, and Straus [GRS62] proved that the claim is true for all $k >
 $|A|$ is sufficiently large.
 -/
 @[category research solved, AMS 5]
-theorem erdos_494.variant.gordon_fraenkel_straus :
+theorem erdos_494.variants.gordon_fraenkel_straus :
     ∀ k > 2, ∀ᶠ card in atTop, Erdos494Unique k card := by
   sorry
 
@@ -115,7 +115,7 @@ noncomputable def prodMultiset (A : Finset ℂ) (k : ℕ) : Multiset ℂ :=
   ((A.powersetCard k).val.map (fun s => s.prod id))
 
 @[category research solved, AMS 5]
-theorem erdos_494.variant.product :
+theorem erdos_494.variants.product :
     ∃ (A B : Finset ℂ), A.card = B.card ∧ prodMultiset A 3 = prodMultiset B 3 ∧
       A ≠ B := by
   sorry
diff --git a/FormalConjectures/ErdosProblems/510.lean b/FormalConjectures/ErdosProblems/510.lean
@@ -47,7 +47,7 @@ theorem erdos_510 :
 Ruzsa [Ru04] proved an upper bound of $-\exp(O(\sqrt{\log N})$.
 -/
 @[category research solved, AMS 11]
-theorem erdos_510.variant.ruzsa :
+theorem erdos_510.variants.ruzsa :
     ∃ (c : ℝ) (hc : 0 < c),
       ∀ᶠ N in atTop, ∀ (A : Finset ℕ), 0 ∉ A → #A = N →
       ∃ θ, ∑ n ∈ A, cos (n * θ) < - exp (c * sqrt (log N)) := by
@@ -57,7 +57,7 @@ theorem erdos_510.variant.ruzsa :
 Bedert [Be25c] proved an upper bound of $-c N^{1/7}$.
 -/
 @[category research solved, AMS 11]
-theorem erdos_510.variant.bedert :
+theorem erdos_510.variants.bedert :
     ∃ (c : ℝ) (hc : 0 < c),
       ∀ᶠ N in atTop, ∀ (A : Finset ℕ), 0 ∉ A → #A = N →
       ∃ θ, ∑ n ∈ A, cos (n * θ) < - c * N ^ (1 / 7 : ℝ) := by
diff --git a/FormalConjectures/ErdosProblems/617.lean b/FormalConjectures/ErdosProblems/617.lean
@@ -47,7 +47,7 @@ theorem erdos_617 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V
 Erdős and Gyárfás [ErGy99] proved the conjecture for $r=3$.
 -/
 @[category research solved, AMS 5]
-theorem erdos_617.variant.r_eq_3 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V]
+theorem erdos_617.variants.r_eq_3 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V]
     (hV : Fintype.card V = 3^2 + 1) (coloring : Sym2 V → Fin 3) :
     ∃ (S : Finset V) (k : Fin 3),
       S.card = 3 + 1 ∧
@@ -58,7 +58,7 @@ theorem erdos_617.variant.r_eq_3 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V]
 Erdős and Gyárfás [ErGy99] proved the conjecture for $r=4$.
 -/
 @[category research solved, AMS 5]
-theorem erdos_617.variant.r_eq_4 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V]
+theorem erdos_617.variants.r_eq_4 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V]
     (hV : Fintype.card V = 4^2 + 1) (coloring : Sym2 V → Fin 4) :
     ∃ (S : Finset V) (k : Fin 4),
       S.card = 4 + 1 ∧
@@ -70,7 +70,7 @@ Erdős and Gyárfás [ErGy99] showed this property fails for infinitely many $r$
 by $r^2$.
 -/
 @[category research solved, AMS 5]
-theorem erdos_617.variant.r2 :
+theorem erdos_617.variants.r2 :
     {r : ℕ | ∃ (V : Type) (_ : Fintype V) (_ : DecidableEq V), Fintype.card V = r^2 ∧
       ∃ (coloring : Sym2 V → Fin r),
         ∀ (S : Finset V), S.card = r + 1 →
diff --git a/FormalConjectures/ErdosProblems/695.lean b/FormalConjectures/ErdosProblems/695.lean
@@ -48,7 +48,7 @@ q(k) \leq \exp(k (\log k)^{1 + o(1)})?
 $$
 -/
 @[category research open, AMS 11]
-theorem erdos_695.variant.upperBound : answer(sorry) ↔
+theorem erdos_695.variants.upperBound : answer(sorry) ↔
     ∃ q : ℕ → ℕ,
       StrictMono q ∧
       (∀ i, (q i).Prime) ∧
diff --git a/FormalConjectures/ErdosProblems/835.lean b/FormalConjectures/ErdosProblems/835.lean
@@ -61,7 +61,7 @@ This is equivalent to asking whether there exists $k > 2$ such that the chromati
 Johnson graph $J(2k, k)$ is $k+1$.
 -/
 @[category research open, AMS 5]
-theorem erdos_835.variant.johnson : (∃ l,
+theorem erdos_835.variants.johnson : (∃ l,
     -- making sure k > 2
     letI k := l + 3
     J(2 * k, k).chromaticNumber = k + 1) ↔ answer(sorry) := by
diff --git a/FormalConjectures/ErdosProblems/930.lean b/FormalConjectures/ErdosProblems/930.lean
@@ -67,7 +67,7 @@ Theorem 2 from [ErSe75].
 [ErSe75] Erdős, P. and Selfridge, J. L., The product of consecutive integers is never a power. Illinois J. Math. (1975), 292-301.
 -/
 @[category research solved, AMS 11]
-theorem erdos_930.variant.consecutive_strong :
+theorem erdos_930.variants.consecutive_strong :
     ∀ k l n, 3 ≤ k → 2 ≤ l → nextPrime k ≤ n + k →
       ∃ p, k ≤ p ∧ p.Prime ∧
         ¬ (l ∣ Nat.factorization (∏ m ∈ Icc (n + 1) (n + k), m) p) := by
@@ -79,12 +79,12 @@ consecutive integers is never a power (establishing the case $r=1$).
 
 Theorem 1 from [ErSe75].
 
-It is implied from `erdos_930.variant.consecutive_strong`.
+It is implied from `erdos_930.variants.consecutive_strong`.
 
 [ErSe75] Erdős, P. and Selfridge, J. L., The product of consecutive integers is never a power. Illinois J. Math. (1975), 292-301.
 -/
 @[category research solved, AMS 11]
-theorem erdos_930.variant.consecutive_integers :
+theorem erdos_930.variants.consecutive_integers :
     ∀ n k, 0 ≤ n → 2 ≤ k →
       ¬ IsPower (∏ m ∈ Icc (n + 1) (n + k), m) := by
   sorry
diff --git a/FormalConjectures/ErdosProblems/975.lean b/FormalConjectures/ErdosProblems/975.lean
@@ -61,12 +61,12 @@ theorem erdos_975 : answer(sorry) ↔
 The correctness of the growth rate is shown in [Va39] (lower bound) and [Er52b] (upper bound).
 -/
 @[category research solved, AMS 11]
-theorem erdos_975.variant.upper_bound (f : ℤ[X]) (hf : Irreducible f)
+theorem erdos_975.variants.upper_bound (f : ℤ[X]) (hf : Irreducible f)
     (hf_pos : ∀ᶠ n in atTop, 1 ≤ f.eval n) : Erdos975Sum f =O[atTop] (fun x ↦ x * log x) := by
   sorry
 
 @[category research solved, AMS 11]
-theorem erdos_975.variant.lower_bound (f : ℤ[X]) (hf : Irreducible f) (hfdeg : f.natDegree ≠ 0)
+theorem erdos_975.variants.lower_bound (f : ℤ[X]) (hf : Irreducible f) (hfdeg : f.natDegree ≠ 0)
     (hf_pos : ∀ᶠ n in atTop, 1 ≤ f.eval n) :
     (fun x ↦ x * log x) =O[atTop] Erdos975Sum f := by
   sorry
@@ -79,7 +79,7 @@ is given by McKey in [Mc95], [Mc97], [Mc99].
 TODO: formalize Hurwitz class numbers and the expression of the constant in terms of them.
 -/
 @[category research solved, AMS 11]
-theorem erdos_975.variant.quadratic (f : ℤ[X]) (hf : Irreducible f)
+theorem erdos_975.variants.quadratic (f : ℤ[X]) (hf : Irreducible f)
     (hf_pos : ∀ᶠ n : ℕ in atTop, 1 ≤ f.eval ↑n) (hf_degree : f.degree = 2) (c : ℝ) :
     c = answer(sorry) → 0 < c ∧ Tendsto (fun x ↦ Erdos975Sum f x / (x * log x)) atTop (𝓝 c) := by
   sorry
@@ -89,12 +89,12 @@ More concrete example for $f(n) = n^2 + 1$, where the asymptote is
 $\sum_{n \le x} \tau(n^2 + 1) \sim \frac{3}{\pi} x \log x + O(x)$. See Tao's blog [T].
 -/
 @[category research solved, AMS 11]
-theorem erdos_975.variant.n2_plus_1_strong :
+theorem erdos_975.variants.n2_plus_1_strong :
     (fun x ↦ Erdos975Sum (X ^ 2 + 1) x - (3 / π) * x * log x) =O[atTop] id := by
   sorry
 
 @[category research solved, AMS 11]
-theorem erdos_975.variant.n2_plus_1 :
+theorem erdos_975.variants.n2_plus_1 :
     ∃ c > (0 : ℝ), Tendsto (fun x ↦ Erdos975Sum (X ^ 2 + 1) x / (x * log x)) atTop (𝓝 c) := by
   sorry
 
diff --git a/FormalConjectures/GreensOpenProblems/7.lean b/FormalConjectures/GreensOpenProblems/7.lean
@@ -30,7 +30,7 @@ namespace Green7
 -- TODO: Add Green's Open Problem 7
 
 @[category research open, AMS 11]
-theorem green_7.variant.queneau : type_of% Erdos341.erdos_341 := by
+theorem green_7.variants.queneau : type_of% Erdos341.erdos_341 := by
   sorry
 
 end Green7
diff --git a/FormalConjectures/Paper/Kurepa.lean b/FormalConjectures/Paper/Kurepa.lean
@@ -51,7 +51,7 @@ theorem kurepa_conjecture (n : ℕ) (h_n : 2 < n) : (!n : ℕ) % n ≠ 0 := by
 This statement can be reduced to the prime case only.
 -/
 @[category research open, AMS 11]
-theorem kurepa_conjecture.variant.prime (p : ℕ) (h_p : 2 < p) :
+theorem kurepa_conjecture.variants.prime (p : ℕ) (h_p : 2 < p) :
     p.Prime → (!p : ℕ) % p ≠ 0 := by
   sorry
 
@@ -87,7 +87,7 @@ theorem kurepa_conjecture.prime_reduction : (∀ n, 2 < n → (!n : ℕ) % n ≠
 An equivalent formulation in terms of the gcd of $n!$ and $!n$.
 -/
 @[category research open, AMS 11]
-theorem kurepa_conjecture.variant.gcd (n : ℕ) : 2 < n → (n !).gcd (! n) = 2 := by
+theorem kurepa_conjecture.variants.gcd (n : ℕ) : 2 < n → (n !).gcd (! n) = 2 := by
   sorry
 
 @[category undergraduate, AMS 11]
@@ -121,15 +121,15 @@ theorem kurepa_conjecture.gcd_reduction : (∀ n, 2 < n → (!n : ℕ) % n ≠ 0
 Sanity check: for small values we can just compute that the conjecture is true
 -/
 @[category test, AMS 11]
-theorem kurepa_conjecture.variant.first_cases (n : ℕ) (h_n : 2 < n) (h_n_upper : n < 50) :
+theorem kurepa_conjecture.variants.first_cases (n : ℕ) (h_n : 2 < n) (h_n_upper : n < 50) :
     (!n : ℕ) % n ≠ 0 := by
   interval_cases n <;> decide
 
 /--
 Sanity check: for small values we can just compute that the conjecture is true.
 -/
 @[category test, AMS 11]
-theorem kurepa_conjecture.variant.gcd.first_cases (n : ℕ) (h_n : 2 < n) (h_n_upper : n < 50) :
+theorem kurepa_conjecture.variants.gcd.first_cases (n : ℕ) (h_n : 2 < n) (h_n_upper : n < 50) :
     (n !).gcd (! n) = 2 := by
   interval_cases n <;> decide
 
