1. FormalConjectures
  2. ErdosProblems
  3. «786»
/- Copyright 2025 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 FormalConjecturesUtil

Erdős Problem 786

Reference: erdosproblems.com/786

open Filter Realopen scoped Topologynamespace Erdos786open Erdos786

Nat.IsMulCardSet A means that A is a set of natural numbers that satisfies the property that $a_1\cdots a_r = b_1\cdots b_s$ with $a_i, b_j\in A$ can only hold when $r = s$.

def Set.IsMulCardSet {α : Type*} [CommMonoid α] (A : Set α) := ∀ (a b : Finset α) (_ :↑a ⊆ A) (_ : ↑b ⊆ A) (_ : a.prod id = b.prod id), a.card = b.card

Let $\epsilon > 0$. Is there some set $A\subset\mathbb{N}$ of density $> 1 - \epsilon$ such that $a_1\cdots a_r = b_1\cdots b_s$ with $a_i, b_j\in A$ can only hold when $r = s$?

@[category research open, AMS 11] theorem erdos_786.parts.i : answer(sorry) ↔ ∀ ε > 0, ε ≤ 1 → ∃ (A : Set ℕ) (δ : ℝ), 0 ∉ A ∧ 1 - ε < δ ∧ A.HasDensity δ ∧ A.IsMulCardSet := ⊢ True ↔ ∀ ε > 0, ε ≤ 1 → ∃ A δ, 0 ∉ A ∧ 1 - ε < δ ∧ A.HasDensity δ ∧ Set.IsMulCardSet A All goals completed! 🐙

Is there some set $A\subset{1, ..., N}$ of size $\geq (1 - o(1))N$ such that $a_1\cdots a_r = b_1\cdots b_s$ with $a_i, b_j\in A$ can only hold when $r = s$?

@[category research open, AMS 11] theorem erdos_786.parts.ii : answer(sorry) ↔ ∃ (A : ℕ → Set ℕ) (f : ℕ → ℝ) (_ : f =o[atTop] (1 : ℕ → ℝ)), ∀ N, A N ⊆ Set.Icc 1 (N + 1) ∧ (1 - f N) * N ≤ (A N).ncard ∧ (A N).IsMulCardSet := ⊢ True ↔ ∃ A f, ∃ (_ : f =o[atTop] 1), ∀ (N : ℕ), A N ⊆ Set.Icc 1 (N + 1) ∧ (1 - f N) * ↑N ≤ ↑(A N).ncard ∧ Set.IsMulCardSet (A N) All goals completed! 🐙

An example of such a set with density $\frac 1 4$ is given by the integers $\equiv 2\pmod{4}$

All goals completed! 🐙

consecutivePrimesFrom p k gives the set of k + 1 consecutive primes that are at least p in size. If p is prime then this is the set of k + 1 consecutive primes p, p_1, ..., p_k

noncomputable def consecutivePrimesFrom (p : ℕ) (k : ℕ) : Finset ℕ := (Finset.range (k + 1)).image (Nat.nth (fun q ↦ q.Prime ∧ p ≤ q))@[category API, AMS 11] theorem nth_zero {p : ℕ} (hp : p.Prime) : Nat.nth (fun q ↦ q.Prime ∧ p ≤ q) 0 = p := p:ℕhp:Nat.Prime p⊢ Nat.nth (fun q ↦ Nat.Prime q ∧ p ≤ q) 0 = p simpa [Nat.nth_zero] using IsLeast.csInf_eq <| p:ℕhp:Nat.Prime p⊢ IsLeast {q | Nat.Prime q ∧ p ≤ q} p All goals completed! 🐙@[category test, AMS 11] lemma consecutivePrimesFrom_zero {p : ℕ} (hp : p.Prime) : consecutivePrimesFrom p 0 = {p} := p:ℕhp:Nat.Prime p⊢ consecutivePrimesFrom p 0 = {p} All goals completed! 🐙h:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 1 = 3⊢ consecutivePrimesFrom 2 1 = {2, 3} h:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 1 = 3q:ℕ⊢ q ∈ consecutivePrimesFrom 2 1 ↔ q ∈ {2, 3} h:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 1 = 3q:ℕ⊢ (∃ a < 1 + 1, Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) a = q) ↔ q = 2 ∨ q = 3 h:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 1 = 3q:ℕ⊢ (∃ a < 1 + 1, Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) a = q) → q = 2 ∨ q = 3h:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 1 = 3q:ℕ⊢ q = 2 ∨ q = 3 → ∃ a < 1 + 1, Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) a = q h:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 1 = 3q:ℕ⊢ (∃ a < 1 + 1, Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) a = q) → q = 2 ∨ q = 3 h:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 1 = 3q:ℕi:ℕhi:i < 1 + 1hq:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) i = q⊢ q = 2 ∨ q = 3 cases i with h:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 1 = 3q:ℕhi:0 < 1 + 1hq:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 0 = q⊢ q = 2 ∨ q = 3 All goals completed! 🐙 h:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 1 = 3q:ℕi:ℕhi:i + 1 < 1 + 1hq:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) (i + 1) = q⊢ q = 2 ∨ q = 3 All goals completed! 🐙 h:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 1 = 3q:ℕ⊢ q = 2 ∨ q = 3 → ∃ a < 1 + 1, Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) a = q h:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 1 = 3⊢ ∃ a < 1 + 1, Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) a = 2h:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 1 = 3⊢ ∃ a < 1 + 1, Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) a = 3; exact ⟨0, h:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 1 = 3⊢ 0 < 1 + 1 All goals completed! 🐙, nth_zero Nat.prime_two⟩; exact ⟨1, h:Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 1 = 3⊢ 1 < 1 + 1 ∧ Nat.nth (fun q ↦ Nat.Prime q ∧ 2 ≤ q) 1 = 3 All goals completed! 🐙⟩

Let $\epsilon > 0$ be given. Then, for a sufficiently large prime p, take the sequence of consecutive primes $p_1 < \cdots < p_k$ such that $$ \sum_{i=1}^k \frac{1}{p_i} < 1 < \sum_{i=1}^{k + 1} \frac{1}{p_i}, $$ and let $A$ be the set of all naturals divisible by exactly one of $p_1, ..., p_k$ (with multiplicity $1$). Then $A$ has density $\frac{1}{e} - \epsilon$ and has the property that $a_1\cdots a_r = b_1\cdots b_s$ with $a_i, b_j\in A$ can only hold when $r = s$.

@[category research solved, AMS 11] theorem erdos_786.parts.i.selfridge (ε : ℝ) (hε : 0 < ε ∧ ε < 1 / rexp 1) : ∀ᶠ (p : ℕ) in atTop, p.Prime → ∃ k, ∑ q ∈ consecutivePrimesFrom p k, (1 : ℝ) / q < 1 ∧ 1 < ∑ q ∈ consecutivePrimesFrom p (k + 1), (1 : ℝ) / q ∧ letI A := { n | ∑ q ∈ consecutivePrimesFrom p k, (n : ℕ).factorization q = 1 } A.HasDensity (1 / rexp 1 - ε) ∧ A.IsMulCardSet := ε:ℝhε:0 < ε ∧ ε < 1 / rexp 1⊢ ∀ᶠ (p : ℕ) in atTop, Nat.Prime p → ∃ k, ∑ q ∈ consecutivePrimesFrom p k, 1 / ↑q < 1 ∧ 1 < ∑ q ∈ consecutivePrimesFrom p (k + 1), 1 / ↑q ∧ {n | ∑ q ∈ consecutivePrimesFrom p k, n.factorization q = 1}.HasDensity (1 / rexp 1 - ε) ∧ Set.IsMulCardSet {n | ∑ q ∈ consecutivePrimesFrom p k, n.factorization q = 1} All goals completed! 🐙end Erdos786