Erdős Problem 948 to Erdős Problem 970

TheoremErdős Problem 948#

References: - erdosproblems.com/948 - [Er77c] Erdős, Paul, Problems and results on combinatorial number theory. III. Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976) (1977), 43-72. - [ErGa91] Erdős, P. and Galvin, F., Some Ramsey-type theorems. Discrete Math. 87 (1991), 261–269.

Quoted from FormalConjectures/ErdosProblems/948.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/948.

The file states 2 research or textbook statements: 2 solved.

Erdos948.erdos_948

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos948.lean#L451.

Is there a function \(f(n)\) and a \(k\) such that in any \(k\)-colouring of the integers there exists a sequence \(a_1 < a_2 < \cdots\) such that \(a_n < f(n)\) for infinitely many \(n\) and the set

\[\left\{ \sum_{i \in S} a_i : \textrm{finite nonempty } S \right\}\]

does not contain all colours?

A question of Erdős [Er77c] and Erdős and Galvin [ErGa91]. The answer is no: GPT-5.5 Pro (prompted by Price) showed that for every \(f\) there is a colouring of the integers such that the finite sums of every such sequence use all colours. The linked formal proof (Codex and GPT-5.6 Sol) gives, for every \(f\) and \(k \ge 1\), a colouring \(c : \mathbb{Z} \to \{0, \ldots, k - 1\}\) such that for every strictly increasing \(a\) with \(a_n < f(n)\) infinitely often and every colour, some nonempty finite sum of the \(a_i\) has that colour.

theorem erdos_948 :
    ¬ ∃ (f : ℕ → ℕ) (k : ℕ), 0 < k ∧ ∀ colouring : ℤ → Fin k,
      ∃ a : ℕ → ℤ, StrictMono a ∧ {n | a n < f n}.Infinite ∧
        ∃ c : Fin k, ∀ S : Finset ℕ, S.Nonempty → colouring (∑ i ∈ S, a i) ≠ c

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/948.lean, line 52.

Erdos948.erdos_948.variants.monochromatic

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos948.lean#L451.

The original question asks for the set of finite sums to be monochromatic. Galvin showed that this fails for \(k = 2\), and it fails for every \(k \ge 2\) by the negative answer to erdos_948.

theorem erdos_948.variants.monochromatic :
    ¬ ∃ (f : ℕ → ℕ) (k : ℕ), 2 ≤ k ∧ ∀ colouring : ℤ → Fin k,
      ∃ a : ℕ → ℤ, StrictMono a ∧ {n | a n < f n}.Infinite ∧
        ∃ c : Fin k, ∀ S : Finset ℕ, S.Nonempty → colouring (∑ i ∈ S, a i) = c

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/948.lean, line 65.

Sources

• FormalConjectures/ErdosProblems/948.lean at 2055e5ad
• erdosproblems.com/948

LeanErdos948.erdos_948 · Erdos948.erdos_948.variants.monochromatic

TheoremErdős Problem 949#

Reference: erdosproblems.com/949

Quoted from FormalConjectures/ErdosProblems/949.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/949.

The file states 2 research or textbook statements: 1 open and 1 solved.

Erdos949.erdos_949

Open: stated without proof.

Let \(S \subseteq \mathbb{R}\) be a set containing no solutions to \(a + b = c\). Must there be a set \(A \subseteq \mathbb{R} \setminus S\) of cardinality continuum such that \(A + A \subseteq \mathbb{R}\setminus S\)?

theorem erdos_949 :
    ∀ S : Set ℝ, (∀ a ∈ S, ∀ b ∈ S, a + b ∉ S) → ∃ A ⊆ Sᶜ, #A = 𝔠 ∧ A + A ⊆ Sᶜ

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/949.lean, line 40.

Erdos949.erdos_949.variants.sidon

Proved here.

Let \(S\sub \mathbb{R}\) be a Sidon set. Must there be a set \(A\sub \mathbb{R}∖S\) of cardinality continuum such that \(A + A \sub \mathbb{R}∖S\)?

theorem erdos_949.variants.sidon :
    ∀ S : Set ℝ, IsSidon S → ∃ A ⊆ Sᶜ, #A = 𝔠 ∧ A + A ⊆ Sᶜ

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/949.lean, line 47.

Sources

• FormalConjectures/ErdosProblems/949.lean at 2055e5ad
• erdosproblems.com/949

LeanErdos949.erdos_949 · Erdos949.erdos_949.variants.sidon

TheoremErdős Problem 950#

References: - erdosproblems.com/855 - erdosproblems.com/950 - [Er77c] Erdős, Paul, Problems and results on combinatorial number theory. III. Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976) (1977), 43-72. - mathoverflow/508491

Quoted from FormalConjectures/ErdosProblems/950.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/950.

The file states 7 research or textbook statements: 5 open and 2 solved.

Erdos950.erdos_950.parts.i

Open: stated without proof.

Is it true that \(\liminf f(n)=1\)?

theorem erdos_950.parts.i :
    atTop.liminf (fun n : ℕ ↦ (f n : EReal)) = 1

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/950.lean, line 48.

Erdos950.erdos_950.parts.ii

Open: stated without proof.

Is it true that \(\limsup f(n)=\infty\)?

theorem erdos_950.parts.ii :
    atTop.limsup (fun n : ℕ ↦ (f n : EReal)) = ⊤

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/950.lean, line 56.

Erdos950.erdos_950.parts.iii

Open: stated without proof.

Is it true that \(f(n)=o(\log\log n)\) for all \(n\)?

theorem erdos_950.parts.iii :
    f =o[atTop] (fun n : ℕ ↦ Real.log (Real.log n))

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/950.lean, line 64.

Erdos950.erdos_950.variants.debruijn_erdos_turan

Solved: stated here without proof.

This function was considered by de Bruijn, Erdős, and Turán, who showed that \(\sum_{n\lt x}f(n)\sim \sum_{n\lt x}f(n)^2\sim x\). They gave no proofs, but a proof of the (harder) second claim is given by Gorodetsky here [mathoverflow/508491].

theorem erdos_950.variants.debruijn_erdos_turan :
    (fun x : ℕ ↦ ∑ n ∈ Finset.range x, f n) ~[atTop] (fun x : ℕ ↦ (x : ℝ)) ∧
    (fun x : ℕ ↦ ∑ n ∈ Finset.range x, (f n) ^ 2) ~[atTop] (fun x : ℕ ↦ (x : ℝ))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/950.lean, line 74.

Erdos950.erdos_950.variants.weaker_pi

Open: stated without proof.

Erdős writes that a 'weaker conjecture which is perhaps not quite inaccessible' is that, for every \(\epsilon>0\), if \(x\) is sufficiently large there exists \(y\lt x\) such that \(\pi(x)< \pi(y)+\epsilon \pi(x-y)\). Compare this to [855].

theorem erdos_950.variants.weaker_pi :
    ∀ ε > 0, ∀ᶠ x in atTop, ∃ y < x,
      (π x : ℝ) < (π y : ℝ) + ε * (π (x - y) : ℝ)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/950.lean, line 85.

Erdos950.erdos_950.variants.weaker_pi_implies_f

Solved: stated here without proof.

He notes that if \(\pi(x)< \pi(y)+O\left(\frac{x-y}{\log x}\right)\) for all \(y\lt x-(\log x)^C\) for some constant \(C>0\) then \(f(n)\ll \log\log\log n\).

theorem erdos_950.variants.weaker_pi_implies_f
    (h : ∃ C > (0 : ℝ), ∃ K > (0 : ℝ), ∀ᶠ x : ℕ in atTop, ∀ y : ℕ,
      (y : ℝ) < x - (Real.log x) ^ C →
      (π x : ℝ) < (π y : ℝ) + K * ((x - y : ℝ) / Real.log x)) :
    f =O[atTop] fun n : ℕ ↦ Real.log (Real.log (Real.log n))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/950.lean, line 95.

Erdos950.erdos_950.variants.sum_primes

Open: stated without proof.

The study of \(f(p)\) is even harder, and Erdős could not prove that \(\sum_{p\lt x}f(p)^2\sim \pi(x)\).

theorem erdos_950.variants.sum_primes :
    (fun x : ℕ ↦ ∑ p ∈ (Finset.range x).filter Prime, (f p) ^ 2) ~[atTop]
      fun x ↦ (π x : ℝ)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/950.lean, line 107.

Sources

• FormalConjectures/ErdosProblems/950.lean at 2055e5ad
• erdosproblems.com/950

LeanErdos950.erdos_950.parts.i · Erdos950.erdos_950.parts.ii · Erdos950.erdos_950.parts.iii · Erdos950.erdos_950.variants.debruijn_erdos_turan · Erdos950.erdos_950.variants.weaker_pi · Erdos950.erdos_950.variants.weaker_pi_implies_f · Erdos950.erdos_950.variants.sum_primes

TheoremErdős Problem 951#

References: - erdosproblems.com/951 - [Er77c] Erdős, Paul, Problems and results on combinatorial number theory. III. Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976) (1977), 43-72.

Quoted from FormalConjectures/ErdosProblems/951.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/951.

The file states 2 research or textbook statements: 1 open and 1 solved. It also has 1 API statement, counted here but not shown.

Erdos951.erdos_951

Open: stated without proof.

If 1 < a 0 < ... has property Erdos951Prop, is it true that #{a i ≤ x} ≤ π x?

theorem erdos_951 :
    ∀ a : ℕ → ℝ, 1 < a 0 → StrictMono a → Erdos951Prop a →
      ∀ᶠ (x : ℝ) in Filter.atTop, {i : ℕ | a i ≤ x}.ncard ≤ π ⌊x⌋₊

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/951.lean, line 62.

Erdos951.erdos_951.variants.beurling

Solved: stated here without proof.

Beurling conjectured that if 1 < a 0 < a 1 < ⋯ has property Erdos951Prop and the number of reals in \([1, x]\) of the form \(\prod_i a_i^{k_i}\) is \(x + o(\log x)\), then a must be the sequence of primes. Property Erdos951Prop makes distinct exponent vectors give distinct Beurling integers, so counting the set BeurlingIntegers a counts the generalised integers.

theorem erdos_951.variants.beurling :
    ∀ a : ℕ → ℝ, IsBeurlingPrimes a → Erdos951Prop a →
    ((fun x => (BeurlingIntegers a ∩ .Iic x).ncard - x) =o[atTop] Real.log) →
    a = Nat.cast ∘ Nat.nth Nat.Prime

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/951.lean, line 72.

Sources

• FormalConjectures/ErdosProblems/951.lean at 2055e5ad
• erdosproblems.com/951

LeanErdos951.erdos_951 · Erdos951.erdos_951.variants.beurling

TheoremErdős Problem 952#

References: - erdosproblems.com/952 - Wikipedia - [OAI26a] OpenAI, Bounded-Step Walks on Gaussian Primes. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Bounded-Step-Walks-on-Gaussian-Primes-September-26-2026/paper.pdf

Quoted from FormalConjectures/ErdosProblems/952.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/952.

The file states 1 research or textbook statement: 1 solved.

Erdos952.erdos_952

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/GaussianMoat/Main.lean#L102.

Is there an infinite sequence of distinct Gaussian primes \(x_1,x_2,\ldots\) such that \(\lvert x_{n+1}-x_n\rvert \ll 1\)?

No. This was disproved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.

theorem erdos_952 :
  ¬ ∃ (x : ℕ → GaussianInt) (C : ℤ),
    Function.Injective x ∧
      ∀ n, Prime (x n) ∧ (x (n + 1) - x n).norm < C

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/952.lean, line 45.

Sources

• FormalConjectures/ErdosProblems/952.lean at 2055e5ad
• erdosproblems.com/952

LeanErdos952.erdos_952

TheoremErdős Problem 954#

References: - erdosproblems.com/954 - [Er77c] Erdős, P., Problems and results on combinatorial number theory. III. Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976), Lecture Notes in Math. 626, Springer (1977), 43-72. PDF

Quoted from FormalConjectures/ErdosProblems/954.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/954.

The file states 3 research or textbook statements: 2 open and 1 textbook result. It also has 3 test statements, counted here but not shown.

Erdos954.erdos_954

Open: stated without proof.

Let \(0=a_0\lt a_1\lt a_2\lt \cdots\) be the sequence of integers defined by \(a_0=0\) and \(a_1=1\), and \(a_{k+1}\) is the smallest integer \(n\) for which the number of solutions to \(a_i+a_j \leq n\) (with \(0\leq i\leq j\leq k\) and \(j\geq 1\)) is \(\lt n\).

Is the number of solutions to \(a_i+a_j \leq x\) equal to \(x+O(x^{1/4+o(1)})\)?

The sequence was constructed by Rosen [Er77c, p. 71]. We read \(O(x^{1/4+o(1)})\) as \(O(x^{1/4+\varepsilon})\) for every \(\varepsilon>0\), and use the version with \(a_0=0\).

theorem erdos_954 :
    ∀ ε > (0 : ℝ), (fun x : ℕ ↦ (solutionCount x : ℝ) - x) =O[atTop]
      (fun x : ℕ ↦ (x : ℝ) ^ ((1 : ℝ) / 4 + ε))

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/954.lean, line 87.

Erdos954.erdos_954.variants.upper

Open: stated without proof.

Erdős and Rosen could not even prove that the number of solutions to \(a_i+a_j\leq x\) is at most \((1+o(1))x\) [Er77c, p. 71].

theorem erdos_954.variants.upper :
    ∀ ε > (0 : ℝ), ∀ᶠ x : ℕ in atTop, (solutionCount x : ℝ) ≤ (1 + ε) * x

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/954.lean, line 97.

Erdos954.erdos_954.variants.lower

Textbook result, stated without proof.

The number of solutions to \(a_i+a_j\leq x\) is always at least \(x\) by construction [Er77c, p. 71].

theorem erdos_954.variants.lower : ∀ x : ℕ, x ≤ solutionCount x

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/954.lean, line 106.

Sources

• FormalConjectures/ErdosProblems/954.lean at 2055e5ad
• erdosproblems.com/954

LeanErdos954.erdos_954 · Erdos954.erdos_954.variants.upper · Erdos954.erdos_954.variants.lower

TheoremErdős Problem 955#

References: - erdosproblems.com/955 - [EGPS90] Erdős, P. and Granville, A. and Pomerance, C. and Spiro, C., On the normal behavior of the iterates of some arithmetic functions. Analytic number theory (Allerton Park, IL, 1989) (1990), 165-204. - [Er73b] Erdős, P., Über die Zahlen der Form \(\sigma(n) - n\) und \(n - \phi(n)\). Elem. Math. (1973), 83--86. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437. - [PPT18] Pollack, Paul and Pomerance, Carl and Thompson, Lola, Divisor-sum fibers. Mathematika (2018), 330--342. - [Po14b] Pollack, Paul, Some arithmetic properties of the sum of proper divisors and the sum of prime divisors. Illinois J. Math. (2014), 125--147. - [PoPo16] Pollack, Paul and Pomerance, Carl, Some problems of Erdős on the sum-of-divisors function. Trans. Amer. Math. Soc. Ser. B (2016), 1--26. - [Tr15] Troupe, Lee, On the number of prime factors of values of the sum-of-proper-divisors function. J. Number Theory (2015), 120--135. - [Tr20] Troupe, Lee, Divisor sums representable as the sum of two squares. Proc. Amer. Math. Soc. (2020), 4189--4202.

Quoted from FormalConjectures/ErdosProblems/955.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/955.

The file states 7 research or textbook statements: 1 open and 6 solved. It also has 5 test statements, counted here but not shown.

Erdos955.erdos_955

Open: stated without proof.

If \(A\subset \mathbb{N}\) has density \(0\) then \(s^{-1}(A)\) must also have density \(0\).

A conjecture of Erdős, Granville, Pomerance, and Spiro [EGPS90].

theorem erdos_955 :
    ∀ A : Set ℕ, A.HasDensity 0 → { x | s x ∈ A }.HasDensity 0

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/955.lean, line 76.

Erdos955.erdos_955.variants.positive_density

Solved: stated here without proof.

It is possible for \(s(A)\) to have positive density even if \(A\) has zero density (for example taking \(A\) to be the product of two distinct primes).

theorem erdos_955.variants.positive_density :
    ∃ A : Set ℕ, A.HasDensity 0 ∧ (∃ d > 0, (s '' A).HasDensity d)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/955.lean, line 85.

Erdos955.erdos_955.variants.empty_preimage

Solved: stated here without proof.

Erdős [Er73b] proved that there are sets \(A\) of positive density such that \(s^{-1}(A)\) is empty.

Here "positive density" means positive lower density: Erdős proved that the set of untouchable numbers (those not of the form \(s(n)\)) has positive lower density [Er73b, Satz I]. Pollack and Pomerance [PoPo16] conjecture that this set has a natural density and give a heuristic for its value. The same result is stated as erdos_418.variants.sigma in Erdős Problem 418.

theorem erdos_955.variants.empty_preimage :
    ∃ A : Set ℕ, 0 < A.lowerDensity ∧ { x | s x ∈ A } = ∅

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/955.lean, line 98.

Erdos955.erdos_955.variants.pollack_primes

Solved: stated here without proof.

Pollack [Po14b] has shown that this is true if \(A\) is the set of primes.

theorem erdos_955.variants.pollack_primes :
    { x | Nat.Prime (s x) }.HasDensity 0

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/955.lean, line 106.

Erdos955.erdos_955.variants.troupe_unusually_many_prime_factors

Solved: stated here without proof.

Troupe [Tr15] has shown that this is true if \(A\) is the set of integers with unusually many prime factors.

theorem erdos_955.variants.troupe_unusually_many_prime_factors :
    ∀ ε > 0, { x | (1 + ε) * Real.log (Real.log (s x)) <
      (ArithmeticFunction.cardDistinctFactors (s x) : ℝ) }.HasDensity 0

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/955.lean, line 115.

Erdos955.erdos_955.variants.troupe_sum_of_two_squares

Solved: stated here without proof.

Troupe [Tr20] has also shown this is true if \(A\) is the set of integers which are the sum of two squares.

theorem erdos_955.variants.troupe_sum_of_two_squares :
    { x | ∃ a b : ℕ, s x = a^2 + b^2 }.HasDensity 0

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/955.lean, line 125.

Erdos955.erdos_955.variants.pollack_pomerance_thompson_bound

Solved: stated here without proof.

Pollack, Pomerance, and Thompson [PPT18] prove that if \(\epsilon(x)=o(1)\) and \(A\subset \mathbb{N}\) has size at most \(x^{1/2+\epsilon(x)}\) then \(\#\{ n\leq x: s(n)\in A\} =o(x)\) as \(x\to \infty\). It follows that (using \(s(n)\ll n\log\log n\)) if \(A\) grows like \(\lvert A\cap [1,x]\rvert\leq x^{1/2+o(1)}\) then \(s^{-1}(A)\) has density \(0\).

theorem erdos_955.variants.pollack_pomerance_thompson_bound :
    ∀ (A : Set ℕ) (ε : ℕ → ℝ),
      Tendsto ε atTop (𝓝 0) →
      (∀ᶠ n : ℕ in atTop, (count (· ∈ A) n : ℝ) ≤ (n : ℝ) ^ ((1 / 2 : ℝ) + ε n)) →
      { x | s x ∈ A }.HasDensity 0

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/955.lean, line 137.

Sources

• FormalConjectures/ErdosProblems/955.lean at 2055e5ad
• erdosproblems.com/955

LeanErdos955.erdos_955 · Erdos955.erdos_955.variants.positive_density · Erdos955.erdos_955.variants.empty_preimage · Erdos955.erdos_955.variants.pollack_primes · Erdos955.erdos_955.variants.troupe_unusually_many_prime_factors · Erdos955.erdos_955.variants.troupe_sum_of_two_squares · Erdos955.erdos_955.variants.pollack_pomerance_thompson_bound

TheoremErdős Problem 957#

References: - erdosproblems.com/957 - [Du19] Dumitrescu, Adrian, A product inequality for extreme distances. Comput. Geom. 85 (2019), 101577. PDF - [ErPa90] Erdős, P. and Pach, J., Variations on the theme of repeated distances. Combinatorica 10 (1990), 261-269.

Quoted from FormalConjectures/ErdosProblems/957.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/957.

The file states 2 research or textbook statements: 2 solved.

Erdos957.erdos_957

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos957.lean#L57.

Let \(A\subset \mathbb{R}^2\) be a set of size \(n\) and let \(\{d_1\lt \ldots\lt d_k\}\) be the set of distinct distances determined by \(A\). Let \(f(d)\) be the number of times the distance \(d\) is determined. Is it true that

\[f(d_1)f(d_k) \leq (\tfrac{9}{8}+o(1))n^2?\]

A question of Erdős and Pach [ErPa90]. The answer is yes, proved by Dumitrescu [Du19]. Here \(f(d)\) counts unordered pairs of points of \(A\) at distance \(d\) (distanceMultiplicity), and \(o(1)\) is uniform over all \(A\) of size \(n\).

theorem erdos_957 :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ A : Finset ℝ², A.card = n →
      ∀ d₁ dₖ : ℝ, IsLeast (distanceSet A : Set ℝ) d₁ →
        IsGreatest (distanceSet A : Set ℝ) dₖ →
          (distanceMultiplicity A d₁ : ℝ) * distanceMultiplicity A dₖ ≤
            (9 / 8 + ε) * (n : ℝ) ^ 2

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/957.lean, line 52.

Erdos957.erdos_957.variants.dumitrescu

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos957.lean#L44.

The original problem was solved by Dumitrescu [Du19, Theorem 1], who proved that

\[f(d_1)f(d_k)\leq \frac{9}{8}n^2+O(n).\]

Here a single constant \(C\) in the error term \(Cn\) works for all finite \(A \subset \mathbb{R}^2\).

theorem erdos_957.variants.dumitrescu :
    ∃ C : ℝ, ∀ A : Finset ℝ², ∀ d₁ dₖ : ℝ, IsLeast (distanceSet A : Set ℝ) d₁ →
      IsGreatest (distanceSet A : Set ℝ) dₖ →
        (distanceMultiplicity A d₁ : ℝ) * distanceMultiplicity A dₖ ≤
          9 / 8 * (A.card : ℝ) ^ 2 + C * (A.card : ℝ)

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/957.lean, line 68.

Sources

• FormalConjectures/ErdosProblems/957.lean at 2055e5ad
• erdosproblems.com/957

LeanErdos957.erdos_957 · Erdos957.erdos_957.variants.dumitrescu

TheoremErdős Problem 958#

References: - erdosproblems.com/958 - [CDL25] Clemen, F., Dumitrescu, A. and Liu, D., On multiplicities of interpoint distances. arXiv:2505.04283 (2025). - PALOMAR-2026-10-05-000004

Quoted from FormalConjectures/ErdosProblems/958.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/958.

The file states 1 research or textbook statement: 1 solved.

Erdos958.erdos_958

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/08152671ab394392fd941b18654daba734c26518/erdos-958/Solution.lean#L60.

Let \(A\subset \mathbb{R}^2\) be a finite set of size \(n\), and let \(\{d_1,\ldots,d_k\}\) be the set of distances determined by \(A\). Let \(f(d)\) be the multiplicity of \(d\), that is, the number of unordered pairs from \(A\) of distance \(d\) apart.

Is it true that \(k=n-1\) and \(\{f(d_i)\}=\{n-1,\ldots,1\}\) if and only if \(A\) is a set of equidistant points on a line or a circle?

Erdős conjectured that the answer is no, and other such configurations exist.

This was proved by Clemen, Dumitrescu, and Liu [CDL25], who observed that equidistant points on a short circular arc on a circle of radius \(1\), together with the centre, are also an example.

The classification is asked for all sufficiently large \(n\). Small exceptions such as \(\{(0,0), (1,0), (0,1), (0,-1)\}\) exist, so the negative answer asserts counterexamples of arbitrarily large size, as in [CDL25].

theorem erdos_958 :
    ¬ ∃ N : ℕ, ∀ n ≥ N, ∀ A : Finset ℝ², #A = n →
      ((#(distanceSet A) = n - 1 ∧
            (distanceSet A).image (distanceMultiplicity A) = Finset.Icc 1 (n - 1)) →
        (IsEquidistantOnLine A ∨ IsEquidistantOnCircle A))

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/958.lean, line 68.

Sources

• FormalConjectures/ErdosProblems/958.lean at 2055e5ad
• erdosproblems.com/958

LeanErdos958.erdos_958

TheoremErdős Problem 959#

Reference: erdosproblems.com/959

Quoted from FormalConjectures/ErdosProblems/959.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/959.

The file states 2 research or textbook statements: 1 open and 1 solved.

Erdos959.erdos_959

Open: stated without proof.

Let \(A\subseteq \mathbb{R}^2\) be a set of size \(n\) and let \(\{d_1,\ldots,d_k\}\) be the set of distinct distances determined by \(A\). Let \(f(d)\) be the number of times the distance \(d\) is determined, ordered so that \(f(d_1)\geq f(d_2)\geq \cdots \geq f(d_k)\). Estimate

\[\max (f(d_1)-f(d_2)),\]

where the maximum is taken over all \(A\) of size \(n\) (this is extremalGap n).

theorem erdos_959 :
    (fun n ↦ (extremalGap n : ℝ)) =Θ[atTop] erdos_959.answer

Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/959.lean, line 85.

Erdos959.erdos_959.lower_bound

Solved: stated here; a Lean proof is at https://github.com/williamjblair/lean-proofs/blob/4f915a323443bfb1709a6805a013812016dca88a/starfleet/erdos-959/Research/FinalLowerBound.lean.

A superlinear lower bound: there is a \(c>0\) with

\[\text{extremalGap}(n)\geq n^{1 + c/\log\log n}\]

for all large \(n\), so \(\max (f(d_1)-f(d_2))\) grows faster than any linear function of \(n\). Determining the exact order remains open, which is erdos_959.

theorem erdos_959.lower_bound :
    ∃ c : ℝ, 0 < c ∧ ∃ N : ℕ, ∀ n ≥ N,
      (n : ℝ) ^ (1 + c / Real.log (Real.log n)) ≤ extremalGap n

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/959.lean, line 97.

Sources

• FormalConjectures/ErdosProblems/959.lean at 2055e5ad
• erdosproblems.com/959

LeanErdos959.erdos_959 · Erdos959.erdos_959.lower_bound

TheoremErdős Problem 961#

References: - erdosproblems.com/961 - [Ju74] Jutila, Matti, On numbers with a large prime factor. {II}. J. Indian Math. Soc. (N.S.) (1974), 125--130. - RaSh73 Ramachandra, K. and Shorey, T. N., On gaps between numbers with a large prime factor. Acta Arith. (1973), 99--111.

Quoted from FormalConjectures/ErdosProblems/961.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/961.

The file states 5 research or textbook statements: 1 open and 4 solved. It also has 1 test statement, counted here but not shown.

Erdos961.erdos_961.sylvester_schur

Solved: stated here without proof.

Sylvester and Schur [Er34] proved that every set of \(k\) consecutive integers greater than \(k\) contains an integer divisible by a prime greater than \(k\), i.e. not \((k+1)\)-smooth.

theorem erdos_961.sylvester_schur (k : ℕ) (hk : 0 < k) : Erdos961Prop k k

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/961.lean, line 43.

Erdos961.erdos_961.variants.well_defined

Proved here.

There exists \(n\) such that Erdos961Prop k n holds.

theorem erdos_961.variants.well_defined (k : ℕ) (hk : 0 < k): ∃ n, Erdos961Prop k n

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/961.lean, line 60.

Erdos961.erdos_961

Open: stated without proof.

It is conjectured that \(f(k) \ll (\log k)^O(1)\).

theorem erdos_961 : ∃ C : ℕ, ∀ᶠ k : ℕ in atTop, f k < log k ^ C

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/961.lean, line 76.

Erdos961.erdos_961.variants.erdos_upper_bound

Solved: stated here without proof.

Erdos [Er55d] proved \(f(k) < 3 \frac{k}{\log k}\) for sufficiently large \(k\).

theorem erdos_961.variants.erdos_upper_bound :
    ∀ᶠ k in atTop, f k < 3 * k / log k

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/961.lean, line 83.

Erdos961.erdos_961.variants.jutila_ramachandra_shorey_upper_bound

Solved: stated here without proof.

Jutila [Ju74], and Ramachandra--Shorey [RaSh73] proved a stronger upper bound \(f(k) \ll \frac{\log \log \log k}{\log \log k} \frac{k}{\log k}\).

theorem erdos_961.variants.jutila_ramachandra_shorey_upper_bound :
    (fun k => (f k : ℝ)) =O[atTop] fun k => log (log (log k)) / log (log k) * (k / log k)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/961.lean, line 92.

Sources

• FormalConjectures/ErdosProblems/961.lean at 2055e5ad
• erdosproblems.com/961

LeanErdos961.erdos_961.sylvester_schur · Erdos961.erdos_961.variants.well_defined · Erdos961.erdos_961 · Erdos961.erdos_961.variants.erdos_upper_bound · Erdos961.erdos_961.variants.jutila_ramachandra_shorey_upper_bound

TheoremErdős Problem 962#

References: - erdosproblems.com/962 - [Er65] Erdős, P., Extremal problems in number theory. Proc. Sympos. Pure Math., Vol. VIII (1965), 181-189. - [Er76e] Erdős, P., Problems and results on consecutive integers. Publ. Math. Debrecen (1976), 271-282. - Tang - Tao

Quoted from FormalConjectures/ErdosProblems/962.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/962.

The file states 3 research or textbook statements: 1 open and 2 solved.

Erdos962.erdos_962

Open: stated without proof.

Main conjecture:

\(\log k(n) \le (\log n)^{(1/2 + o(1))}\)

theorem erdos_962 :
    ∃ ε : ℕ → ℝ,
      (∀ δ > 0, ∀ᶠ n in atTop, |ε n| < δ) ∧
      ∀ᶠ n : ℕ in atTop,
        log (k n : ℝ)
          ≤ rpow (log n) ((1 : ℝ) / 2 + ε n)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/962.lean, line 59.

Erdos962.erdos_962.variants.tang_lower_bound

Solved: stated here without proof.

Tang's lower bound [Tang]:

\(\log k(n) \ge (1/\sqrt{2} - o(1)) * \sqrt{\log n * \log \log n}\)

theorem erdos_962.variants.tang_lower_bound :
    ∃ ε : ℕ → ℝ,
      (∀ δ > 0, ∀ᶠ n in atTop, |ε n| < δ) ∧
      ∀ᶠ n : ℕ in atTop,
          (1 / sqrt 2 - ε n) *
              sqrt (log n * log (log n))
            ≤ log (k n : ℝ)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/962.lean, line 73.

Erdos962.erdos_962.variants.tao_upper_bound

Solved: stated here without proof.

Tao's upper bound [Tao]:

\(k(n) \le (1 + o(1)) * n^{1/2}\)

theorem erdos_962.variants.tao_upper_bound :
    ∃ ε : ℕ → ℝ,
      (∀ δ > 0, ∀ᶠ n in atTop, |ε n| < δ) ∧
      ∀ᶠ n : ℕ in atTop,
          (k n : ℝ) ≤ (1 + ε n) * sqrt n

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/962.lean, line 88.

Sources

• FormalConjectures/ErdosProblems/962.lean at 2055e5ad
• erdosproblems.com/962

LeanErdos962.erdos_962 · Erdos962.erdos_962.variants.tang_lower_bound · Erdos962.erdos_962.variants.tao_upper_bound

TheoremErdős Problem 963#

References: - erdosproblems.com/963 - [Er65] Erdős, P., Extremal problems in number theory. Proc. Sympos. Pure Math., Vol. VIII (1965), 181-189. PDF

A set B of real numbers is dissociated if all sums over its finite subsets are distinct. This is AddDissociated in Mathlib.

Quoted from FormalConjectures/ErdosProblems/963.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/963.

The file states 4 research or textbook statements: 3 open and 1 solved. It also has 2 API statements, counted here but not shown.

Erdos963.erdos_963.parts.i

Open: stated without proof.

Let \(f(n)\) be the maximal \(k\) such that in any set \(A\subset \mathbb{R}\) of size \(n\) there is a subset \(B\subseteq A\) of size \(\lvert B\rvert\geq k\) which is dissociated that is, the sums \(\sum_{b\in S}b\) are distinct for all \(S\subseteq B\). Estimate \(f(n)\) - in particular, is it true that \(f(n)\geq \lfloor \log_2 n\rfloor\)?

This is the first part, a problem of Erdős [Er65, p. 188]. We read "estimate" as an asymptotic equivalence \(f(n)\sim\) answer n. The order of magnitude \(\log n\) is easy (see erdos_963.variants.greedy and the example \(a_i=i\) in [Er65, p. 188]), so the question is the constant.

theorem erdos_963.parts.i :
    (fun n : ℕ ↦ (f n : ℝ)) ~[atTop] erdos_963.parts.i.answer

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/963.lean, line 81.

Erdos963.erdos_963.parts.ii

Open: stated without proof.

Let \(f(n)\) be the maximal \(k\) such that in any set \(A\subset \mathbb{R}\) of size \(n\) there is a subset \(B\subseteq A\) of size \(\lvert B\rvert\geq k\) which is dissociated that is, the sums \(\sum_{b\in S}b\) are distinct for all \(S\subseteq B\). Estimate \(f(n)\) - in particular, is it true that \(f(n)\geq \lfloor \log_2 n\rfloor\)?

This is the second part. Erdős [Er65, p. 188] asks whether the bound \(\lfloor\log_3 n\rfloor\) can be improved to \(\lfloor\log_2 n\rfloor\). We state it for all \(n\geq 1\), with \(\lfloor\log_2 n\rfloor\) written as Nat.log 2 n.

As on the problem page, \(A\) is any set of reals. [Er65] speaks of "given numbers" and uses the example \(a_i=i\). Allowing negative numbers makes the question harder. A dissociated set never contains both \(x\) and \(-x\), and changing signs keeps a set dissociated. So the largest dissociated subsets of \(A\) and of \(\{\lvert a\rvert : a\in A,\ a\neq 0\}\) have the same size, and the sets \(\{\pm a : a\in S\}\) (with \(0\) added for odd \(n\)) show that \(f(2m)=f(2m+1)\) is the least size of a largest dissociated subset of a set of \(m\) positive reals. Hence this statement asks for \(\lfloor\log_2 m\rfloor+1\) for \(m\) positive reals. The question for positive reals with \(\lfloor\log_2\lvert A\rvert\rfloor\), one less, is erdos_963.variants.positive; it follows from this statement.

theorem erdos_963.parts.ii : ∀ n : ℕ, 1 ≤ n → Nat.log 2 n ≤ f n

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/963.lean, line 106.

Erdos963.erdos_963.variants.greedy

Solved: stated here without proof.

Erdős noted that the greedy algorithm showed \(f(n)\geq \lfloor \log_3 n\rfloor\) [Er65, p. 188].

theorem erdos_963.variants.greedy (n : ℕ) : Nat.log 3 n ≤ f n

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/963.lean, line 114.

Erdos963.erdos_963.variants.positive

Open: stated without proof.

The second part for sets of positive reals, with \(\lfloor\log_2\lvert A\rvert\rfloor\) as in [Er65, p. 188] and its example \(a_i=i\): every set \(A\) of positive reals has a dissociated subset with at least \(\lfloor\log_2 \lvert A\rvert\rfloor\) elements.

theorem erdos_963.variants.positive :
    ∀ A : Finset ℝ, (∀ a ∈ A, 0 < a) →
      ∃ B ⊆ A, Nat.log 2 A.card ≤ B.card ∧ AddDissociated (B : Set ℝ)

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/963.lean, line 123.

Sources

• FormalConjectures/ErdosProblems/963.lean at 2055e5ad
• erdosproblems.com/963

LeanErdos963.erdos_963.parts.i · Erdos963.erdos_963.parts.ii · Erdos963.erdos_963.variants.greedy · Erdos963.erdos_963.variants.positive

TheoremErdős Problem 964#

References: - erdosproblems.com/964 - [Er86b] Erdős, P., Some problems on number theory. Proceedings of the seventeenth Southeastern international conference on combinatorics, graph theory, and computing (Boca Raton, Fla., 1986), Congr. Numer. 54 (1986), 225-244. - [Eb25] Eberhard, S., Ratios of consecutive values of the divisor function. arXiv:2505.00727 (2025).

Quoted from FormalConjectures/ErdosProblems/964.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/964.

The file states 2 research or textbook statements: 2 solved. It also has 1 API statement, counted here but not shown.

Erdos964.erdos_964

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos964.lean#L1559.

Let \(\tau(n)\) count the number of divisors of \(n\). Is the sequence

\[\frac{\tau(n+1)}{\tau(n)}\]

everywhere dense in \((0,\infty)\)?

The answer is yes, proved by Eberhard [Eb25].

theorem erdos_964 : Set.Ioi (0 : ℝ) ⊆ closure (tauRatio '' Set.Ici 1)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/964.lean, line 60.

Erdos964.erdos_964.variants.eberhard

Solved: stated here without proof.

Eberhard [Eb25] proved that the ratios \(\tau(n+1)/\tau(n)\) attain every positive rational value infinitely many times. Since the positive rationals are dense in \((0,\infty)\), this implies erdos_964.

theorem erdos_964.variants.eberhard (q : ℚ) (hq : 0 < q) :
    {n : ℕ | 0 < n ∧ tauRatio n = q}.Infinite

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/964.lean, line 69.

Sources

• FormalConjectures/ErdosProblems/964.lean at 2055e5ad
• erdosproblems.com/964

LeanErdos964.erdos_964 · Erdos964.erdos_964.variants.eberhard

TheoremErdős Problem 965#

For every 2-coloring of ℝ, is there an uncountable set \(A ⊆ ℝ\) such that all sums \(a + b\) for \(a, b ∈ A, a ≠ b\) have the same colour?

References: - erdosproblems.com/965 - [Er75b] Erdős, Paul, Problems and results in combinatorial number theory. Journées Arithmétiques de Bordeaux (Conf., Univ. Bordeaux, Bordeaux, 1974) (1975), 295-310. - [HLS17] Hindman, Neil and Leader, Imre and Strauss, Dona, Pairwise sums in colourings of the reals. Abh. Math. Semin. Univ. Hambg. (2017), 275--287. - [Ko16] Komjáth, Péter, A certain 2-coloring of the reals. Real Anal. Exchange (2016), 227--231. - [SWCol] Sokoup Dániel and Weiss, William, Sums and Anti-Ramsey Colourings of ℝ. https://danieltsoukup.github.io/academic/finset_colouring.pdf

Quoted from FormalConjectures/ErdosProblems/965.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/965.

The file states 2 research or textbook statements: 2 solved.

Erdos965.erdos_965

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/dfe2d78128b493c572cf525b1b8edf4897fb7664/src/latest/ErdosProblems/Erdos965.lean#L42.

Erdős asks in [Er75b] if for every 2-coloring of ℝ, there is an uncountable set \(A ⊆ ℝ\) such that all sums \(a + b\) for \(a, b ∈ A, a ≠ b\) have the same colour.

In [Ko16] Péter Komjáth constructed a counterexample. The same result was proven independently in [SWCol] by Sokoup and Weiss.

theorem erdos_965 :
    ¬ ∀ f : ℝ → Fin 2, ∃ A : Set ℝ, ¬ A.Countable ∧
      ∀ᵉ (a ∈ A) (b ∈ A) (c ∈ A) (d ∈ A), a ≠ b → c ≠ d → f (a + b) = f (c + d)

Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/965.lean, line 48.

Erdos965.erdos_965.variants.generalization

Solved: stated here without proof.

For every 2-coloring of ℝ, is there some \(k ≥ 2\) and an uncountable set \(A ⊆ ℝ\) such that all sums \(a_1 + \cdots + a_k\) of \(k\) distinct elements of \(A\) have the same colour?

In fact, in both [Ko16] and [SWCol] a single 2-coloring of ℝ is constructed such that for every \(k ≥ 2\) and every uncountable \(A ⊆ ℝ\) the sums of \(k\) distinct elements of \(A\) are not monochromatic.

theorem erdos_965.variants.generalization :
    ¬ ∀ f : ℝ → Fin 2, ∃ k ≥ 2, ∃ A : Set ℝ, ¬ A.Countable ∧ ∀ s t : Finset ℝ,
      ↑s ⊆ A → ↑t ⊆ A → s.card = k → t.card = k → f (s.sum id) = f (t.sum id)

Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/965.lean, line 62.

Sources

• FormalConjectures/ErdosProblems/965.lean at 2055e5ad
• erdosproblems.com/965

LeanErdos965.erdos_965 · Erdos965.erdos_965.variants.generalization

TheoremErdős Problem 966#

References: - erdosproblems.com/966 - [Er75b] Erdős, Paul, Problems and results in combinatorial number theory. Journées Arithmétiques de Bordeaux (Conf., Univ. Bordeaux, Bordeaux, 1974) (1975), 295-310.

Quoted from FormalConjectures/ErdosProblems/966.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/966.

The file states 1 research or textbook statement: 1 solved.

Erdos966.erdos_966

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos966.lean.

Let \(k,r\geq 2\). Does there exist a set \(A\subseteq \mathbb{N}\) that contains no non-trivial arithmetic progression of length \(k+1\), yet in any \(r\)-colouring of \(A\) there must exist a monochromatic non-trivial arithmetic progression of length \(k\)?

Erdős [Er75b] reported that 'Spencer has recently shown that such a sequence exists', but gives no reference.

theorem erdos_966 :
    ∀ k r : ℕ, 2 ≤ k → 2 ≤ r → ∃ A : Set ℕ, A.IsAPOfLengthFree (k + 1) ∧
      ∀ coloring : A → Fin r, ContainsMonoAPofLength coloring k

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/966.lean, line 43.

Sources

• FormalConjectures/ErdosProblems/966.lean at 2055e5ad
• erdosproblems.com/966

LeanErdos966.erdos_966

TheoremErdős Problem 967#

References: - erdosproblems.com/967 - [ErIn64] Erdős, P. and Ingham, A. E., Arithmetical Tauberian theorems. Acta Arith. (1964), 341-356. - [Yi25] Yip, F., On a problem of Erdős and Ingham. arXiv:2512.16528 (2025).

Quoted from FormalConjectures/ErdosProblems/967.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/967.

The file states 5 research or textbook statements: 2 open and 3 solved.

Erdos967.erdos_967

Solved: stated here; a Lean proof is at https://gist.githubusercontent.com/llllvvuu/d25f037d1f1000bdabd6ca928c74c9bb/raw/c2d3e4ed5d88520993b508f84be029cf8808f565/967.lean.

Let \(1\lt a_1\lt \cdots\) be a sequence of integers such that \(\sum\frac{1}{a_i}\lt \infty\). Is it true that, for every \(t\in \mathbb{R}\),

\[1+\sum_{k}\frac{1}{a_k^{1+it}}\neq 0?\]

Yip [Yi25] has proved that this is not always true - in fact, for any real \(t\neq 0\), there exists a sequence of integers \(1\lt a_1\lt \cdots\) such that \(\sum \frac{1}{a_i}\lt \infty\) and \(1+\sum_{k}\frac{1}{a_k^{1+it}}=0\).

This was formalized in Lean by Wu using Aristotle.

theorem erdos_967 :
    ¬ ∀ a : ℕ → ℕ, StrictMono a → 1 < a 0 → Summable (fun k : ℕ => 1 / (a k : ℝ)) →
      ∀ t : ℝ, 1 + (∑' k, summand t (a k)) ≠ 0

Category research solved; AMS 11 Number theory, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/967.lean, line 55.

Erdos967.erdos_967.variants.yip

Solved: stated here without proof.

Yip [Yi25] has proved that this is not always true - in fact, for any real \(t\neq 0\), there exists a sequence of integers \(1\lt a_1\lt \cdots\) such that \(\sum \frac{1}{a_i}\lt \infty\) and \(1+\sum_{k}\frac{1}{a_k^{1+it}}=0\).

theorem erdos_967.variants.yip (t : ℝ) (ht : t ≠ 0) :
    ∃ a : ℕ → ℕ, StrictMono a ∧ 1 < a 0 ∧ Summable (fun k : ℕ => 1 / (a k : ℝ)) ∧
      (1 + (∑' k, summand t (a k)) = 0)

Category research solved; AMS 11 Number theory, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/967.lean, line 66.

Erdos967.erdos_967.variants.finite

Open: stated without proof.

It remains open whether this is true for every finite sequence of integers.

theorem erdos_967.variants.finite :
    ∀ A : Finset ℕ, (∀ n ∈ A, 1 < n) → ∀ t : ℝ, 1 + (∑ n ∈ A, summand t n) ≠ 0

Category research open; AMS 11 Number theory, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/967.lean, line 75.

Erdos967.erdos_967.variants.two_three_five

Open: stated without proof.

A question of Erdős and Ingham [ErIn64]. The simplest case they could not decide this question for was the finite sequence \(\{2,3,5\}\).

theorem erdos_967.variants.two_three_five :
    ∀ t : ℝ, 1 + (∑ n ∈ ({2, 3, 5} : Finset ℕ), summand t n) ≠ 0

Category research open; AMS 11 Number theory, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/967.lean, line 84.

Erdos967.erdos_967.variants.tauberian

Solved: stated here without proof.

Their interest in this problem arose from their proof that the statement that there are no such zeros is equivalent to the fact that, for any non-decreasing \(f:\mathbb{R}\to \mathbb{R}_{\geq 0}\) which is bounded on every bounded interval and is \(=0\) for \(x<1\), the relationship

\[f(x)+\sum_k f(x/a_k)=\left(1+\sum_k \frac{1}{a_k}+o(1)\right)x\]

implies \(f(x)=(1+o(1))x\).

theorem erdos_967.variants.tauberian (a : ℕ → ℕ) (ha : StrictMono a) (ha₀ : 1 < a 0)
    (hsum : Summable (fun k : ℕ => 1 / (a k : ℝ))) :
    (∀ t : ℝ, 1 + (∑' k, summand t (a k)) ≠ 0) ↔
      ∀ f : ℝ → ℝ, Monotone f → (∀ x : ℝ, 0 ≤ f x) → (∀ x < 1, f x = 0) →
        (∀ x y : ℝ, BddAbove (f '' Set.Icc x y)) →
        Tendsto (fun x : ℝ => (f x + ∑' k, f (x / (a k : ℝ))) / x) atTop
          (𝓝 (1 + ∑' k, 1 / (a k : ℝ))) →
        Tendsto (fun x : ℝ => f x / x) atTop (𝓝 1)

Category research solved; AMS 11 Number theory, 40 Sequences, series, summability. Declared in FormalConjectures/ErdosProblems/967.lean, line 96.

Sources

• FormalConjectures/ErdosProblems/967.lean at 2055e5ad
• erdosproblems.com/967

LeanErdos967.erdos_967 · Erdos967.erdos_967.variants.yip · Erdos967.erdos_967.variants.finite · Erdos967.erdos_967.variants.two_three_five · Erdos967.erdos_967.variants.tauberian

TheoremErdős Problem 968#

Let uₙ = pₙ / n, where pₙ is the nth prime. Does the set of n such that uₙ < uₙ₊₁ have positive lower density?

Erdős and Prachar also proved that ∑_{pₙ < x} |uₙ₊₁ - uₙ| ≍ (log x)^2, and that the set of n such that uₙ > uₙ₊₁ has positive lower density. Erdős also asked whether there are infinitely many increasing triples uₙ < uₙ₊₁ < uₙ₊₂ or decreasing triples uₙ > uₙ₊₁ > uₙ₊₂.

Reference: erdosproblems.com/968

[ErPr61] Erdős, P. and Prachar, K., Sätze und Probleme über pₖ/k. Abh. Math. Sem. Univ. Hamburg (1961/62), 251–256.

[FMT18] Ford, K. and Maynard, J. and Tao, T., Chains of large gaps between primes. Irregularities in the distribution of prime numbers, Springer (2018), 1–21.

[Ma15] Maynard, J., Small gaps between primes. Ann. of Math. (2015), 383–413.

[OAI26a] OpenAI, Positive lower density of large prime gaps. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Positive-lower-density-of-large-prime-gaps-September-25-2026/main.pdf

Quoted from FormalConjectures/ErdosProblems/968.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/968.

The file states 5 research or textbook statements: 5 solved.

Erdos968.erdos_968

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PrimeGaps/RatioCorollary.lean#L30.

Does the set {n | u n < u (n+1)} have positive lower density?

Yes. This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.

theorem erdos_968 : 0 < {n : ℕ | u n < u (n + 1)}.lowerDensity

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/968.lean, line 70.

Erdos968.erdos_968.variants.sum_abs_diff_isTheta_log_sq

Solved: stated here without proof.

Erdős and Prachar proved ∑_{pₙ < x} |u (n+1) - u n| ≍ (log x)^2 (see [ErPr61]).

We encode ∑_{pₙ < x} as a sum over n < Nat.primeCounting' x (the number of primes < x).

theorem erdos_968.variants.sum_abs_diff_isTheta_log_sq :
    (fun x : ℕ =>
        ∑ n < Nat.primeCounting' x, |u (n + 1) - u n|) =Θ[atTop]
      fun x : ℕ => log x ^ 2

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/968.lean, line 79.

Erdos968.erdos_968.variants.decreasing_steps_pos_lower_density

Solved: stated here without proof.

Erdős and Prachar proved that the set {n | u n > u (n+1)} has positive lower density (see [ErPr61]).

theorem erdos_968.variants.decreasing_steps_pos_lower_density :
    0 < {n : ℕ | u n > u (n + 1)}.lowerDensity

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/968.lean, line 90.

Erdos968.erdos_968.variants.infinite_increasingTriples

Solved: stated here without proof.

Erdős asked whether there are infinitely many solutions to uₙ < uₙ₊₁ < uₙ₊₂.

The answer is yes. Since uₙ < uₙ₊₁ is equivalent to pₙ₊₁ - pₙ > pₙ / n, it suffices to have infinitely many n with two consecutive prime gaps larger than pₙ / n ∼ log n. Ford, Maynard, and Tao [FMT18] proved that for every fixed k there are infinitely many n with k consecutive prime gaps all of size ≫ log pₙ · log log pₙ · log log log log pₙ / log log log pₙ.

theorem erdos_968.variants.infinite_increasingTriples :
    {n : ℕ | u n < u (n + 1) ∧ u (n + 1) < u (n + 2)}.Infinite

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/968.lean, line 103.

Erdos968.erdos_968.variants.infinite_decreasingTriples

Solved: stated here without proof.

Erdős asked whether there are infinitely many solutions to uₙ > uₙ₊₁ > uₙ₊₂.

The answer is yes. Since uₙ > uₙ₊₁ is equivalent to pₙ₊₁ - pₙ < pₙ / n, it suffices to have infinitely many n with pₙ₊₂ - pₙ bounded, because pₙ / n → ∞. Maynard [Ma15] proved that liminf (pₙ₊₂ - pₙ) < ∞.

theorem erdos_968.variants.infinite_decreasingTriples :
    {n : ℕ | u n > u (n + 1) ∧ u (n + 1) > u (n + 2)}.Infinite

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/968.lean, line 115.

Sources

• FormalConjectures/ErdosProblems/968.lean at 2055e5ad
• erdosproblems.com/968

LeanErdos968.erdos_968 · Erdos968.erdos_968.variants.sum_abs_diff_isTheta_log_sq · Erdos968.erdos_968.variants.decreasing_steps_pos_lower_density · Erdos968.erdos_968.variants.infinite_increasingTriples · Erdos968.erdos_968.variants.infinite_decreasingTriples

TheoremErdős Problem 969#

References: - Erdős Problem 969 - Moser, L. and MacLeod, R. A., The error term for the squarefree integers. Canadian Mathematical Bulletin 9 (1966), 303–306. https://doi.org/10.4153/CMB-1966-039-4

Quoted from FormalConjectures/ErdosProblems/969.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/969.

The file states 3 research or textbook statements: 1 open and 2 solved. It also has 1 test statement, counted here but not shown.

Erdos969.erdos_969

Open: stated without proof.

Let \(Q(x)\) count the squarefree integers in \([1,x]\), and define \(E(x)\) by

\[Q(x)=\frac{6}{\pi^2}x+E(x).\]

Determine the order of magnitude of \(E(x)\): an upper bound \(E(x)=O(g(x))\) with a matching oscillation bound \(E(x)\ne o(g(x))\).

theorem erdos_969 :
    let g := erdos_969.answer
    (fun x => |squarefreeCountingError x|) =O[atTop] g ∧
      ¬(fun x => |squarefreeCountingError x|) =o[atTop] g

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/969.lean, line 57.

Erdos969.erdos_969.variants.prime_number_theorem

Solved: stated here without proof.

The prime number theorem implies \(E(x)=o(\sqrt{x})\).

theorem erdos_969.variants.prime_number_theorem :
    (fun x => |squarefreeCountingError x|) =o[atTop] (fun x : ℕ => (x : ℝ).sqrt)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/969.lean, line 65.

Erdos969.erdos_969.variants.evelyn_linfoot

Solved: stated here without proof.

Evelyn and Linfoot proved \(E(x)=\Omega(x^{1/4})\).

theorem erdos_969.variants.evelyn_linfoot :
    ¬(fun x => |squarefreeCountingError x|) =o[atTop]
      (fun x : ℕ => (x : ℝ) ^ (1 / 4 : ℝ))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/969.lean, line 71.

Sources

• FormalConjectures/ErdosProblems/969.lean at 2055e5ad
• erdosproblems.com/969

LeanErdos969.erdos_969 · Erdos969.erdos_969.variants.prime_number_theorem · Erdos969.erdos_969.variants.evelyn_linfoot

TheoremErdős Problem 970#

References: - erdosproblems.com/970 - [FGKMT18] Ford, Kevin and Green, Ben and Konyagin, Sergei and Maynard, James and Tao, Terence, Long gaps between primes. J. Amer. Math. Soc. (2018), 65-105. - [Iw78] Iwaniec, Henryk, On the problem of {J}acobsthal. Demonstratio Math. (1978), 225--231. - [OAI26a] OpenAI, A quadratic bound for Jacobsthal's function. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-quadratic-bound-for-Jacobsthals-function-September-25-2026/paper.pdf

Quoted from FormalConjectures/ErdosProblems/970.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/970.

The file states 2 research or textbook statements: 2 solved.

Erdos970.erdos_970

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/Jacobsthal/Conclusions/QuadraticBound.lean#L13.

Let \(h(k)\) be Jacobsthal's function, defined to as the minimal \(m\) such that, if \(n\) has at most \(k\) prime factors, then in any set of \(m\) consecutive integers there exists an integer coprime to \(n\). Determine the order of magnitude of \(h(k)\). In particular, is it true that

\[h(k) \ll k^2?\]

The bound \(h(k) \ll k^2\) was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof. The order of magnitude of \(h(k)\) remains open.

theorem erdos_970 :
    ∃ C > (0 : ℝ), ∀ k : ℕ, 0 < k → (jacobsthalFunction k : ℝ) ≤ C * k ^ 2

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/970.lean, line 60.

Erdos970.erdos_970.variants.iterated_log

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/Jacobsthal/Conclusions/IteratedLogBound.lean#L59.

The stronger bound

\[h(k) \ll \frac{k^2}{(\log\log 3k)^2}\]

proved in [OAI26a].

theorem erdos_970.variants.iterated_log :
    ∃ C > (0 : ℝ), ∀ k : ℕ, 0 < k →
      (jacobsthalFunction k : ℝ) ≤ C * k ^ 2 / (Real.log (Real.log (3 * k))) ^ 2

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/970.lean, line 70.

Sources

• FormalConjectures/ErdosProblems/970.lean at 2055e5ad
• erdosproblems.com/970

LeanErdos970.erdos_970 · Erdos970.erdos_970.variants.iterated_log

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.