1. FormalConjectures
  2. ErdosProblems
  3. «26»
/- 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 26

References:

    erdosproblems.com/26

    Te19 G. Tenenbaum, Some of Erdős' unconventional problems in number theory, thirty-four years later, arXiv:1908.00488 [math.NT] (2019)

namespace Erdos26

A sequence of naturals $(a_i)$ is thick if their sum of reciprocals diverges: $$ \sum_i \frac{1}{a_i} = \infty $$

def IsThick {ι : Type*} (A : ι → ℕ) : Prop := ¬Summable (fun i ↦ (1 : ℝ) / A i) @[category test, AMS 11] theorem not_isThick_of_finite {ι : Type*} [Finite ι] (A : ι → ℕ) : ¬IsThick A := ι:Type u_1inst✝:Finite ιA:ι → ℕ⊢ ¬IsThick A All goals completed! 🐙 @[category test, AMS 11] theorem not_isThick_of_geom_one_lt (r : ℕ) (hr : r > 1) : ¬IsThick fun n : ℕ ↦ r ^ n := r:ℕhr:r > 1⊢ ¬IsThick fun n => r ^ n simpa [IsThick] using summable_geometric_of_lt_one (r := 1 / r) (r:ℕhr:r > 1⊢ 0 ≤ 1 / ↑r All goals completed! 🐙) (div_lt_self zero_lt_one (mod_cast hr)) @[category test, AMS 11] theorem isThick_const {ι : Type*} [Infinite ι] (r : ℕ) (h : r > 0) : IsThick fun _ : ι ↦ r := ι:Type u_1inst✝:Infinite ιr:ℕh:r > 0⊢ IsThick fun x => r ι:Type u_1inst✝:Infinite ιr:ℕh:r > 0⊢ ¬r = 0 All goals completed! 🐙

The set of multiples of a sequence $(a_i)$ is ${na_i | n \in \mathbb{N}, i}$.

def MultiplesOf {ι : Type*} (A : ι → ℕ) : Set ℕ := Set.range fun (n, i) ↦ n * A i @[category test, AMS 11] theorem multiplesOf_eq_univ {ι : Type*} (A : ι → ℕ) (h : 1 ∈ Set.range A) : MultiplesOf A = Set.univ := ι:Type u_1A:ι → ℕh:1 ∈ Set.range A⊢ MultiplesOf A = Set.univ ι:Type u_1A:ι → ℕi:ιhi:A i = 1⊢ MultiplesOf A = Set.univ exact top_unique fun n hn ↦ ⟨(n, i), ι:Type u_1A:ι → ℕi:ιhi:A i = 1n:ℕhn:n ∈ ⊤⊢ (fun x => match x with | (n, i) => n * A i) (n, i) = n All goals completed! 🐙⟩

A sequence of naturals $(a_i)$ is Behrend if almost all integers are a multiple of some $a_i$. In other words, if the set of multiples has natural density $1$.

def IsBehrend {ι : Type*} (A : ι → ℕ) : Prop := (MultiplesOf A).HasDensity 1

A sequence of naturals $(a_i)$ is weakly Behrend with respect to $\varepsilon \in \mathbb{R}$ if at least $1 - \varepsilon$ density of all numbers are a multiple of $A$.

def IsWeaklyBehrend {ι : Type*} (A : ι → ℕ) (ε : ℝ) : Prop := 1 - ε ≤ (MultiplesOf A).lowerDensity @[category test, AMS 11] theorem isBehrend_of_contains_one {ι : Type*} (A : ι → ℕ) (h : 1 ∈ Set.range A) : IsBehrend A := ι:Type u_1A:ι → ℕh:1 ∈ Set.range A⊢ IsBehrend A ι:Type u_1A:ι → ℕh:1 ∈ Set.range A⊢ Filter.Tendsto (fun b => (MultiplesOf A).partialDensity Set.univ b) Filter.atTop (nhds 1) exact tendsto_atTop_of_eventually_const (i₀ := 1) fun n hn ↦ ι:Type u_1A:ι → ℕh:1 ∈ Set.range An:ℕhn:n ≥ 1⊢ (MultiplesOf A).partialDensity Set.univ n = 1 ι:Type u_1A:ι → ℕh:1 ∈ Set.range An:ℕhn:n ≥ 1⊢ ¬n = 0 All goals completed! 🐙 @[category test, AMS 11] theorem isWeaklyBehrend_of_ge_one {ι : Type*} (A : ι → ℕ) {ε : ℝ} (hε : 1 ≤ ε) : IsWeaklyBehrend A ε := ι:Type u_1A:ι → ℕε:ℝhε:1 ≤ ε⊢ IsWeaklyBehrend A ε All goals completed! 🐙 @[category test, AMS 11] theorem not_isWeaklyBehrend_of_neg {ι : Type*} (A : ι → ℕ) {ε : ℝ} (hε : ε < 0) : ¬IsWeaklyBehrend A ε := ι:Type u_1A:ι → ℕε:ℝhε:ε < 0⊢ ¬IsWeaklyBehrend A ε ι:Type u_1A:ι → ℕε:ℝhε:ε < 0⊢ (MultiplesOf A).lowerDensity + ε < 1 All goals completed! 🐙

Let $A\subset\mathbb{N}$ be infinite such that $\sum_{a \in A} \frac{1}{a} = \infty$. Must there exist some $k\geq 1$ such that almost all integers have a divisor of the form $a+k$ for some $a\in A$?

This was formalized in Lean by Alexeev using Aristotle.

@[category research solved, AMS 11, formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos26.lean"] theorem declaration uses 'sorry'erdos_26 : answer(False) ↔ ∀ A : ℕ → ℕ, StrictMono A → IsThick A → ∃ k, IsBehrend (A · + k) := ⊢ False ↔ ∀ (A : ℕ → ℕ), StrictMono A → IsThick A → ∃ k, IsBehrend fun x => A x + k All goals completed! 🐙

If we allow for $\sum_{a\in A} \frac{1}{a} < \infty$ then Rusza has found a counter-example.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_26.variants.rusza : ∃ A : ℕ → ℕ, StrictMono A ∧ ¬IsThick A ∧ ∀ k, ¬IsBehrend (A · + k) := ⊢ ∃ A, StrictMono A ∧ ¬IsThick A ∧ ∀ (k : ℕ), ¬IsBehrend fun x => A x + k All goals completed! 🐙

Tenenbaum asked the weaker variant where for every $\epsilon>0$ there is some $k=k(\epsilon)$ such that at least $1-\epsilon$ density of all integers have a divisor of the form $a+k$ for some $a\in A$.

The DeepMind prover agent has found a formal disproof of this statement.

@[category research solved, AMS 11, formal_proof using formal_conjectures at "https://github.com/mo271/formal-conjectures/blob/09c54540aa51cb40dff73660c94a82e2631386f8/FormalConjectures/ErdosProblems/26.lean#L625"] theorem declaration uses 'sorry'erdos_26.variants.tenenbaum : answer(False) ↔ ∀ᵉ (A : ℕ → ℕ), StrictMono A → IsThick A → (∀ ε > (0 : ℝ), ∃ k, IsWeaklyBehrend (A · + k) ε) := ⊢ False ↔ ∀ (A : ℕ → ℕ), StrictMono A → IsThick A → ∀ ε > 0, ∃ k, IsWeaklyBehrend (fun x => A x + k) ε All goals completed! 🐙 end Erdos26