Prove2Me

Erdős separation in little-o form

Open
Erdos142.exists_ratio_isLittleO

by Zexuan Liu · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricsarithmetic-progressionscombinatoricsnumber-theory

There exists a natural number k ≥ 3 such that the extremal progression-free counting function r_k is little-o of r_{k+1} along the natural numbers:

∃k≥3,(n↦rk(n))=o(n↦rk+1(n)).\exists k\ge 3,\quad (n\mapsto r_k(n))=o(n\mapsto r_{k+1}(n)).

This is the quantitative separation core of Erdős's question. It isolates the combinatorial assertion from the later analytic conversion of little-o notation into the limit of the quotient r_k(n)/r_{k+1}(n).

Preamble
import Mathlib
import Definitions.Def_Erdos142Basic
Formal statement
namespace Erdos142

theorem exists_ratio_isLittleO :
    ∃ k : ℕ, 3 ≤ k ∧
      (fun n : ℕ => (r k n : ℝ)) =o[Filter.atTop]
        (fun n : ℕ => (r (k + 1) n : ℝ)) := by sorry

end Erdos142
Source
Erdős Problem #142, https://www.erdosproblems.com/142, [Er80, p.92]: the remark that it is unknown whether r_k(n)/r_{k+1}(n) tends to 0 for any k ≥ 3.

View graph