From f6a75f3a9e7c19543dc06208477f19196f7a6de0 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 7 Jan 2026 21:36:07 +0100 Subject: [PATCH 1/3] =?UTF-8?q?Fix=20typo=20in=20Erd=C5=91s=20Problem=2048?= =?UTF-8?q?0?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit fixes #1282 --- FormalConjectures/ErdosProblems/480.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FormalConjectures/ErdosProblems/480.lean b/FormalConjectures/ErdosProblems/480.lean index 2ea2c7962..b1cf7f218 100644 --- a/FormalConjectures/ErdosProblems/480.lean +++ b/FormalConjectures/ErdosProblems/480.lean @@ -45,7 +45,7 @@ and $F_m$ is the $m$th Fibonacci number. This constant is best possible. theorem erdos_480.variants.chung_graham : let c : ℝ := 1 + ∑' (k : ℕ+), (1 : ℝ) / (2*k : ℕ).fib IsGreatest {C : ℝ | C > 0 ∧ ∀ (x : ℕ → ℝ) (hx : ∀ n, x n ∈ Set.Icc 0 1), - ∀ ε ∈ Set.Ioo 0 C, ∃ n, {m | m ≠ 0 ∧ |x (n + m) - x m| < 1 / ((C - ε) * n)}.Infinite} + ∀ ε ∈ Set.Ioo 0 C, ∃ n, {m | n ≠ 0 ∧ |x (n + m) - x m| < 1 / ((C - ε) * n)}.Infinite} c := by sorry From 21bf4c56d9cbc0c6133fb9c432cd874752d31e27 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Tue, 13 Jan 2026 23:51:04 +0000 Subject: [PATCH 2/3] rewrite --- FormalConjectures/ErdosProblems/480.lean | 36 ++++++++++++++++-------- 1 file changed, 24 insertions(+), 12 deletions(-) diff --git a/FormalConjectures/ErdosProblems/480.lean b/FormalConjectures/ErdosProblems/480.lean index b1cf7f218..d558fd4b0 100644 --- a/FormalConjectures/ErdosProblems/480.lean +++ b/FormalConjectures/ErdosProblems/480.lean @@ -24,29 +24,41 @@ import FormalConjectures.Util.ProblemImports namespace Erdos480 -/-- -Let $x_1,x_2,\dots \in [0, 1]$ be an infinite sequence. Is it true that there are infinitely many $m, n$ -such that $|x_{m+n} - x_m| \le \frac 1 {\sqrt 5 n}$? +open Filter -This was proved Chung and Graham. +/-- +Let $x_1,x_2,\ldots\in [0,1]$ be an infinite sequence. +Is it true that +$$\inf_n \liminf_{m\to \infty} n \lvert x_{m+n}-x_m\rvert\leq 5^{-1/2}\approx 0.447?$$ +A conjecture of Newman. -/ @[category research solved, AMS 11] theorem erdos_480 : answer(True) ↔ ∀ (x : ℕ → ℝ), (∀ n, x n ∈ Set.Icc 0 1) → - {(m, n) | (m) (n) (_ : m ≠ 0) (_ : |x (m + n) - x m| ≤ 1 / (√5 * n))}.Infinite := by + ⨅ n, atTop.liminf (fun m => n *|x (m + n) - x m|) ≤ 1 / √5 := by sorry /-- -For any $ϵ>0$ there must exist some $n$ such that there are infinitely many $m$ -for which $|x_{m+n} - x_m| < \frac 1 {(c-ϵ)n}$, where -$c= 1 + \sum_{k \ge 1} \frac 1 {F_{2k}} =2.535370508\dots$ -and $F_m$ is the $m$th Fibonacci number. This constant is best possible. +This was proved by Chung and Graham \cite{ChGr84}, who in fact prove that +$$\inf_n \liminf_{m\to \infty} n \lvert x_{m+n}-x_m\rvert\leq \frac{1}{c}\approx 0.3944$$ +where +$$c=1+\sum_{k\geq 1}\frac{1}{F_{2k}}=2.5353705\cdots$$ +and $F_m$ is the $m$th Fibonacci number. -/ @[category research solved, AMS 11] theorem erdos_480.variants.chung_graham : let c : ℝ := 1 + ∑' (k : ℕ+), (1 : ℝ) / (2*k : ℕ).fib - IsGreatest {C : ℝ | C > 0 ∧ ∀ (x : ℕ → ℝ) (hx : ∀ n, x n ∈ Set.Icc 0 1), - ∀ ε ∈ Set.Ioo 0 C, ∃ n, {m | n ≠ 0 ∧ |x (n + m) - x m| < 1 / ((C - ε) * n)}.Infinite} - c := by + ∀ (x : ℕ → ℝ), (∀ n, x n ∈ Set.Icc 0 1) → + ⨅ n, atTop.liminf (fun m => n *|x (m + n) - x m|) ≤ 1 / c := by + sorry + +/-- +They also prove that this constant is best possible. +-/ +@[category research solved, AMS 11] +theorem erdos_480.variants.chung_graham_best_possible : + let c : ℝ := 1 + ∑' (k : ℕ+), (1 : ℝ) / (2*k : ℕ).fib + ∀ ε > (0 : ℝ), ¬ (∀ (x : ℕ → ℝ), (∀ n, x n ∈ Set.Icc 0 1) → + ⨅ n, atTop.liminf (fun m => n *|x (m + n) - x m|) ≤ 1 / c - ε) := by sorry end Erdos480 From 3b413469dc15fa1c563b510e69723c79dbc6add8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 14 Jan 2026 19:41:47 +0100 Subject: [PATCH 3/3] typos --- FormalConjectures/ErdosProblems/480.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/FormalConjectures/ErdosProblems/480.lean b/FormalConjectures/ErdosProblems/480.lean index d558fd4b0..bdfbb756d 100644 --- a/FormalConjectures/ErdosProblems/480.lean +++ b/FormalConjectures/ErdosProblems/480.lean @@ -34,7 +34,7 @@ A conjecture of Newman. -/ @[category research solved, AMS 11] theorem erdos_480 : answer(True) ↔ ∀ (x : ℕ → ℝ), (∀ n, x n ∈ Set.Icc 0 1) → - ⨅ n, atTop.liminf (fun m => n *|x (m + n) - x m|) ≤ 1 / √5 := by + ⨅ n, atTop.liminf (fun m => n * |x (m + n) - x m|) ≤ 1 / √5 := by sorry /-- @@ -48,7 +48,7 @@ and $F_m$ is the $m$th Fibonacci number. theorem erdos_480.variants.chung_graham : let c : ℝ := 1 + ∑' (k : ℕ+), (1 : ℝ) / (2*k : ℕ).fib ∀ (x : ℕ → ℝ), (∀ n, x n ∈ Set.Icc 0 1) → - ⨅ n, atTop.liminf (fun m => n *|x (m + n) - x m|) ≤ 1 / c := by + ⨅ n, atTop.liminf (fun m => n * |x (m + n) - x m|) ≤ 1 / c := by sorry /-- @@ -58,7 +58,7 @@ They also prove that this constant is best possible. theorem erdos_480.variants.chung_graham_best_possible : let c : ℝ := 1 + ∑' (k : ℕ+), (1 : ℝ) / (2*k : ℕ).fib ∀ ε > (0 : ℝ), ¬ (∀ (x : ℕ → ℝ), (∀ n, x n ∈ Set.Icc 0 1) → - ⨅ n, atTop.liminf (fun m => n *|x (m + n) - x m|) ≤ 1 / c - ε) := by + ⨅ n, atTop.liminf (fun m => n * |x (m + n) - x m|) ≤ 1 / c - ε) := by sorry end Erdos480