ErdosProblems: add 24, 93, 164, 314, 315, 333, 369, 401, 429, 435 (#3998 sync)

FormalConjectures/ErdosProblems/164.lean

@@ -0,0 +1,59 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 164
+
+*References:*
+- [erdosproblems.com/164](https://www.erdosproblems.com/164)
+- [ABLLPSTT26] B. Alexeev, K. Barreto, Y. Li, J. D. Lichtman, L. Price, J. I. Shah, Q. Tang, and
+  T. Tao, *Primitive sets and Von Mangoldt Chains: Erdős problem #1196 and beyond*.
+  arXiv:2605.00301 (2026).
+- [Er35] Erdős, Paul, *Note on Sequences of Integers No One of Which is Divisible By Any Other*.
+  J. London Math. Soc. (1935), 126-128.
+- [Li23] Lichtman, J. D., *A proof of the Erdős primitive set conjecture*. arXiv:2202.02384 (2023).
+-/
+
+namespace Erdos164
+
+/-- A set `A ⊆ ℕ` is *primitive* if no member of `A` divides another. -/
+def IsPrimitive (A : Set ℕ) : Prop :=
+  ∀ a ∈ A, ∀ b ∈ A, a ∣ b → a = b
+
+/--
+A set $A\subset \mathbb{N}$ is primitive if no member of $A$ divides another. Is the sum
+\[\sum_{n\in A}\frac{1}{n\log n}\]
+maximised over all primitive sets when $A$ is the set of primes?
+
+Erdős [Er35] proved that this sum always converges for a primitive set. Lichtman [Li23] proved
+that the answer is yes. An alternative, simpler, proof is given by Alexeev, Barreto, Li, Lichtman,
+Price, Shah, Tang, and Tao [ABLLPSTT26].
+
+Following the convention of [Li23] we require the members of a primitive set to be greater than
+one; this excludes $A = \{1\}$, for which the summand $\frac{1}{1\cdot\log 1}$ is not defined.
+-/
+@[category research solved, AMS 11,
+  formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos164.lean"]
+theorem erdos_164 : answer(True) ↔
+    IsPrimitive {p : ℕ | p.Prime} ∧
+      ∀ A : Set ℕ, (∀ a ∈ A, 2 ≤ a) → IsPrimitive A →
+        (∑' a : A, 1 / ((a : ℕ) * Real.log (a : ℕ))) ≤
+          ∑' p : {p : ℕ | p.Prime}, 1 / ((p : ℕ) * Real.log (p : ℕ)) := by
+  sorry
+
+end Erdos164

FormalConjectures/ErdosProblems/24.lean

@@ -0,0 +1,55 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 24
+
+*References:*
+- [erdosproblems.com/24](https://www.erdosproblems.com/24)
+- [Er92b] Erdős, Paul, *Some of my favourite problems in various branches of combinatorics*.
+  Matematiche (Catania) (1992), 231-240.
+- [Er97f] Erdős, Paul, *Some unsolved problems*. Combinatorics, geometry and probability
+  (Cambridge, 1993) (1997), 1-10.
+- [Gr12] Grzesik, Andrzej, *On the maximum number of five-cycles in a triangle-free graph*.
+  J. Combin. Theory Ser. B (2012), 1061-1066.
+- [HHKNR13] Hatami, Hamed and Hladký, Jan and Kráľ, Daniel and Norine, Serguei and Razborov,
+  Alexander, *On the number of pentagons in triangle-free graphs*. J. Combin. Theory Ser. A
+  (2013), 722-732.
+-/
+
+open SimpleGraph
+
+namespace Erdos24
+
+/--
+Does every triangle-free graph on $5n$ vertices contain at most $n^5$ copies of $C_5$?
+
+Győri proved this with $1.03n^5$, which has been improved by Füredi. The answer is yes, as proved
+independently by Grzesik [Gr12] and Hatami, Hladky, Král, Norine, and Razborov [HHKNR13].
+
+Copies of $C_5$ are counted as subgraphs isomorphic to the cycle graph on five vertices,
+i.e. by `SimpleGraph.copyCount`.
+-/
+@[category research solved, AMS 5,
+  formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos24.lean"]
+theorem erdos_24 : answer(True) ↔
+    ∀ (n : ℕ) (G : SimpleGraph (Fin (5 * n))), G.CliqueFree 3 →
+      G.copyCount (cycleGraph 5) ≤ n ^ 5 := by
+  sorry
+
+end Erdos24

FormalConjectures/ErdosProblems/314.lean

@@ -0,0 +1,61 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 314
+
+*References:*
+- [erdosproblems.com/314](https://www.erdosproblems.com/314)
+- [LiSt24] J. Lim and Steinerberger, S., *On differences of two harmonic numbers*.
+  arXiv:2405.11354 (2024).
+-/
+
+open Filter
+
+namespace Erdos314
+
+/-- The block harmonic sum $\sum_{n\leq k\leq m}\frac{1}{k}$. -/
+noncomputable def harmonicSum (n m : ℕ) : ℝ := ∑ k ∈ Finset.Icc n m, (1 : ℝ) / k
+
+/-- `mMin n` is the minimal `m` such that $\sum_{n\leq k\leq m}\frac{1}{k}\geq 1$; such an `m`
+exists for `n ≥ 1` since the harmonic series diverges. -/
+noncomputable def mMin (n : ℕ) : ℕ := sInf {m | 1 ≤ harmonicSum n m}
+
+/-- $\epsilon(n) = \sum_{n\leq k\leq m}\frac{1}{k}-1$, the overshoot of the minimal block sum
+reaching $1$. -/
+noncomputable def epsilon (n : ℕ) : ℝ := harmonicSum n (mMin n) - 1
+
+/--
+Let $n\geq 1$ and let $m$ be minimal such that $\sum_{n\leq k\leq m}\frac{1}{k}\geq 1$. We define
+\[\epsilon(n) = \sum_{n\leq k\leq m}\frac{1}{k}-1.\]
+How small can $\epsilon(n)$ be? Is it true that
+\[\liminf n^2\epsilon(n)=0?\]
+
+This is true, and shown by Lim and Steinerberger [LiSt24], who further proved that, for any
+$\delta>0$, there exist infinitely many $n$ and $m$ such that
+\[n^2\left\lvert \sum_{n\leq k\leq m}\frac{1}{k}-1\right\rvert\ll \frac{1}{(\log n)^{5/4-\delta}}.\]
+Erdős and Graham (and also Lim and Steinerberger) believe that the exponent of $2$ is best
+possible here, in that $\liminf \epsilon(n) n^{2+\delta}=\infty$ for all $\delta>0$.
+-/
+@[category research solved, AMS 11 40,
+  formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos314.lean"]
+theorem erdos_314 : answer(True) ↔
+    atTop.liminf (fun n : ℕ => (n : ℝ) ^ 2 * epsilon n) = 0 := by
+  sorry
+
+end Erdos314

FormalConjectures/ErdosProblems/315.lean

@@ -0,0 +1,73 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 315
+
+*References:*
+- [erdosproblems.com/315](https://www.erdosproblems.com/315)
+- [ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial number
+  theory*. Monographies de L'Enseignement Mathematique (1980).
+- [Ka25] Y. Kamio, *Asymptotic analysis of infinite decompositions of a unit fraction into unit
+  fractions*. arXiv:2503.02317 (2025).
+- [LiTa25] Z. Li and Q. Tang, *On a conjecture of Erdős and Graham about the Sylvester's
+  sequence*. arXiv:2503.12277 (2025).
+-/
+
+open Filter
+
+namespace Erdos315
+
+/-- The sequence $u_1=1$, $u_{n+1}=u_n(u_n+1)$, indexed here so that `u i` is $u_{i+1}$:
+`u 0 = 1`, `u 1 = 2`, `u 2 = 6`, `u 3 = 42`, … (so `u i + 1` is Sylvester's sequence
+$2, 3, 7, 43, \ldots$). -/
+def u : ℕ → ℕ
+  | 0 => 1
+  | n + 1 => u n * (u n + 1)
+
+/-- The Vardi constant $c_0=\lim u_n^{1/2^n}=1.264085\cdots$. With the `0`-indexing of `u`, the
+$n$-th term $u_n^{1/2^n}$ of the defining sequence is `(u i : ℝ) ^ ((1 / 2 : ℝ) ^ (i + 1))` at
+`i = n - 1`. -/
+noncomputable def c₀ : ℝ := limUnder atTop fun i => (u i : ℝ) ^ ((1 / 2 : ℝ) ^ (i + 1))
+
+/--
+Let $u_1=1$ and $u_{n+1}=u_n(u_n+1)$, so that $\sum_{k\geq 1}\frac{1}{u_k+1}$ and
+$u_k=\lfloor c_0^{2^k}+1\rfloor$ for $k\geq 1$, where
+\[c_0=\lim u_n^{1/2^n}=1.264085\cdots.\]
+Let $a_1<a_2<\cdots $ be any other sequence with $\sum \frac{1}{a_k}=1$. Is it true that
+\[\liminf a_n^{1/2^n}<c_0=1.264085\cdots?\]
+
+This is true, and was proved independently by Kamio [Ka25] and Li and Tang [LiTa25].
+
+An earlier interpretation of this question on this site defined $u_1=2$ and
+$u_{n+1}=u_n^2-u_n+1$ (Sylvester's sequence), which is the same sequence shifted by $1$; we use
+the phrasing above as more faithful to [ErGr80]. The constant $c_0$ is called the Vardi constant.
+
+Formalisation note: `a i` and `u i` denote $a_{i+1}$ and $u_{i+1}$, so the exponent $1/2^n$
+becomes `(1 / 2) ^ (i + 1)`, and "any other sequence" is expressed as `∃ i, a i ≠ u i + 1`, the
+sequence $(u_k+1)_{k\geq 1}$ being the given decomposition with $\sum_{k\geq 1}\frac{1}{u_k+1}=1$.
+-/
+@[category research solved, AMS 11,
+  formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos315.lean"]
+theorem erdos_315 : answer(True) ↔
+    ∀ a : ℕ → ℕ, (∀ i, 0 < a i) → StrictMono a → (∃ i, a i ≠ u i + 1) →
+      ∑' i, (1 : ℝ) / a i = 1 →
+      atTop.liminf (fun i => (a i : ℝ) ^ ((1 / 2 : ℝ) ^ (i + 1))) < c₀ := by
+  sorry
+
+end Erdos315

FormalConjectures/ErdosProblems/333.lean

@@ -0,0 +1,55 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 333
+
+*References:*
+- [erdosproblems.com/333](https://www.erdosproblems.com/333)
+- [ErNe77] Erdős, P. and Newman, D. J., *Bases for sets of integers*. J. Number Theory (1977),
+  420-425.
+-/
+
+open Classical Filter Asymptotics
+
+open scoped Pointwise
+
+namespace Erdos333
+
+/--
+Let $A\subseteq \mathbb{N}$ be a set of density zero. Does there exist a $B$ such that
+$A\subseteq B+B$ and
+\[\lvert B\cap \{1,\ldots,N\}\rvert =o(N^{1/2})\]
+for all large $N$?
+
+The answer is no. Erdős and Newman [ErNe77] have proved this is true when $A$ is the set of
+squares. In fact, Theorem 2 of [ErNe77] already implies a negative answer to this problem, but
+this seems to have been overlooked by Erdős and Graham.
+
+See also [806].
+-/
+@[category research solved, AMS 11,
+  formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos333.lean"]
+theorem erdos_333 : answer(False) ↔
+    ∀ A : Set ℕ, A.HasDensity 0 →
+      ∃ B : Set ℕ, A ⊆ B + B ∧
+        (fun N => (((Finset.Icc 1 N).filter (· ∈ B)).card : ℝ)) =o[atTop]
+          fun N => Real.sqrt N := by
+  sorry
+
+end Erdos333

FormalConjectures/ErdosProblems/369.lean

@@ -0,0 +1,56 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 369
+
+*References:*
+- [erdosproblems.com/369](https://www.erdosproblems.com/369)
+- [BaWo98] Balog, Antal and Wooley, Trevor D., *On strings of consecutive integers with no large
+  prime factors*. J. Austral. Math. Soc. Ser. A (1998), 266-276.
+-/
+
+open Filter
+
+namespace Erdos369
+
+/--
+Let $\epsilon>0$ and $k\geq 2$. Is it true that, for all sufficiently large $n$, there is a
+sequence of $k$ consecutive integers in $\{1,\ldots,n\}$ all of which are $n^\epsilon$-smooth?
+
+The problem is trivially true as written (simply taking $\{1,\ldots,k\}$ and $n>k^{1/\epsilon}$).
+There are (at least) two possible variants which are non-trivial, and it is not clear which
+Erdős and Graham meant. We formalize the second: each $m\in P$ (where $P$ is the sequence of $k$
+consecutive integers sought for) must be in $[n/2,n]$. In this case a positive answer also
+follows directly from the result of Balog and Wooley [BaWo98] for infinitely many $n$. Proving
+this is true for all large $n$ does not follow immediately from [BaWo98], but can be deduced
+using a similar construction, as shown by SkyYang.
+
+The statement below takes the $k$ consecutive integers as $a+1,\ldots,a+k$ with
+$\lfloor n/2\rfloor\leq a+1$ and $a+k\leq n$, and renders "$n^\epsilon$-smooth" as: every prime
+factor is at most $n^\epsilon$.
+-/
+@[category research solved, AMS 11,
+  formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos369.lean"]
+theorem erdos_369 : answer(True) ↔
+    ∀ (ε : ℝ) (hε : 0 < ε) (k : ℕ) (hk : 2 ≤ k),
+      ∀ᶠ (n : ℕ) in atTop, ∃ a : ℕ, n / 2 ≤ a + 1 ∧ a + k ≤ n ∧
+        ∀ j < k, ∀ p ∈ (a + 1 + j).primeFactors, (p : ℝ) ≤ (n : ℝ) ^ ε := by
+  sorry
+
+end Erdos369