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 Real open scoped Topology namespace Erdos786 open 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 declaration uses 'sorry'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 declaration uses 'sorry'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}$

@[category textbook, AMS 11] theorem declaration uses 'sorry'erdos_786.parts.i.example (A : Set ℕ) (hA : A = { n | n % 4 = 2 }) : A.HasDensity (1 / 4) ∧ A.IsMulCardSet := A:Set ℕhA:A = {n | n % 4 = 2}⊢ A.HasDensity (1 / 4) ∧ Set.IsMulCardSet A 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! 🐙 @[category test, AMS 11] lemma consecutivePrimesFrom_two_one : consecutivePrimesFrom 2 1 = {2, 3} := ⊢ consecutivePrimesFrom 2 1 = {2, 3} have h : Nat.nth (fun q ↦ q.Prime ∧ 2 ≤ q) 1 = 3 := ⊢ consecutivePrimesFrom 2 1 = {2, 3} exact Nat.nth_count (p := (fun q ↦ q.Prime ∧ 2 ≤ q)) (⊢ Nat.Prime 3 ∧ 2 ≤ 3 All goals completed! 🐙 : (3).Prime ∧ 2 ≤ 3) h:Nat.nth (fun q => Nat.Prime q ∧ 2 ≤ q) 1 = 3 := Nat.nth_count (of_decide_eq_true (id (Eq.refl true)))q:ℕ⊢ q ∈ consecutivePrimesFrom 2 1 ↔ q ∈ {2, 3} h:Nat.nth (fun q => Nat.Prime q ∧ 2 ≤ q) 1 = 3 := Nat.nth_count (of_decide_eq_true (id (Eq.refl true)))q:ℕ⊢ (∃ 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 = 3 := Nat.nth_count (of_decide_eq_true (id (Eq.refl true)))q:ℕ⊢ (∃ 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 = 3 := Nat.nth_count (of_decide_eq_true (id (Eq.refl true)))q:ℕ⊢ 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 := Nat.nth_count (of_decide_eq_true (id (Eq.refl true)))q:ℕ⊢ (∃ 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 = 3 := Nat.nth_count (of_decide_eq_true (id (Eq.refl true)))q:ℕ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 = 3 := Nat.nth_count (of_decide_eq_true (id (Eq.refl true)))q:ℕ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 = 3 := Nat.nth_count (of_decide_eq_true (id (Eq.refl true)))q:ℕ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 = 3 := Nat.nth_count (of_decide_eq_true (id (Eq.refl true)))q:ℕ⊢ 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 := Nat.nth_count (of_decide_eq_true (id (Eq.refl true)))⊢ ∃ 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 := Nat.nth_count (of_decide_eq_true (id (Eq.refl true)))⊢ ∃ 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 := Nat.nth_count (of_decide_eq_true (id (Eq.refl true)))⊢ 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 := Nat.nth_count (of_decide_eq_true (id (Eq.refl true)))⊢ 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 declaration uses 'sorry'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