Erdős Problem 287

Reference: erdosproblems.com/287

def Erdos287.max_gap (k : ℕ) (s : Fin k → ℕ) : ℕ

The maximum gap between consecutive terms of a finite sequence s : Fin k → ℕ, i.e., $\max_{0 \le i < k-1} (s(i+1) - s(i))$.

Equations

• Erdos287.max_gap k s = Finset.univ.sup fun (i : Fin (k - 1)) => s ⟨↑i + 1, ⋯⟩ - s ⟨↑i, ⋯⟩

theorem Erdos287.erdos_287 : sorry ↔ ∀ (k : ℕ) (hk : 2 ≤ k) (s : Fin k → ℕ), StrictMono s → 1 < s ⟨0, ⋯⟩ → ∑ i : Fin k, 1 / ↑(s i) = 1 → 3 ≤ max_gap k s

Let $k\geq2$. Is it true that, for any distinct integers $1 < n_1 < \cdots < n_k$ such that $\sum_{i=1}^k \frac{1}{n_i} = 1$, we must have $\max(n_{i+1} - n_i) \geq 3$?

theorem Erdos287.erdos_287.variants.gap_at_least_two (k : ℕ) (x✝ : 2 ≤ k) (s : Fin k → ℕ) : StrictMono s → 1 < s ⟨0, ⋯⟩ → ∑ i : Fin k, 1 / ↑(s i) = 1 → 2 ≤ max_gap k s

The lower bound of $\geq 2$ is equivalent to saying that $1$ is not the sum of reciprocals of consecutive integers, proved by Erdős [Er32].

theorem Erdos287.erdos_287.test.best_possible : have s := ![2, 3, 6]; StrictMono s ∧ 1 < s 0 ∧ ∑ i : Fin 3, 1 / ↑(s i) = 1 ∧ max_gap 3 s = 3

The example $1 = \frac{1}{2}+\frac{1}{3}+\frac{1}{6}$ shows that $3$ would be best possible here: the sequence $(2, 3, 6)$ is a valid Egyptian fraction representation of $1$ with max_gap = 3.

theorem Erdos287.erdos_287.variants.prime_conjecture : sorry ↔ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → ∃ (p : ℕ), Nat.Prime p ∧ N ≤ p ∧ p ≤ 2 * N ∧ Nat.Prime ((p + 1) / 2)

For all large $N$, there exists a prime $p \in [N, 2N]$ such that $\frac{p+1}{2}$ is also prime.

This is an open conjecture. If true, it would imply erdos_287 for all but at most finitely many exceptions (see erdos_287.variants.prime_conjecture_implies).

theorem Erdos287.erdos_287.variants.prime_conjecture_implies : (sorry ↔ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → ∃ (p : ℕ), Nat.Prime p ∧ N ≤ p ∧ p ≤ 2 * N ∧ Nat.Prime ((p + 1) / 2)) → ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (hk : 2 ≤ k) (s : Fin k → ℕ), StrictMono s → 1 < s ⟨0, ⋯⟩ → ∑ i : Fin k, 1 / ↑(s i) = 1 → 3 ≤ max_gap k s

The conjecture erdos_287 would follow for all but at most finitely many exceptions if it were known that, for all large $N$, there exists a prime $p \in [N, 2N]$ such that $\frac{p+1}{2}$ is also prime.

More precisely: if the prime conjecture holds, then there exists $k_0$ such that for all $k \geq k_0$, any Egyptian fraction representation of $1$ with $k$ terms and all terms $> 1$ must have $\max(n_{i+1} - n_i) \geq 3$.