Erdős Problem 868 to Erdős Problem 891

TheoremErdős Problem 868#

References: - erdosproblems.com/868 - [LaLa26] Larsen and Larsen, Erdős problem 868 (2026)

Quoted from FormalConjectures/ErdosProblems/868.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/868.

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

Erdos868.erdos_868.parts.i

Solved: stated here without proof.

Let \(A\) be an additive basis of order \(2\), let \(f(n)\) denote the number of ways in which \(n\) can be written as the sum of two elements from \(A\). If \(f(n) \to \infty\) as \(n \to \infty\), then must \(A\) contain a minimal additive basis of order \(2\)?

Larsen and Larsen [LaLa26] answered this in the negative.

theorem erdos_868.parts.i :
    ¬ ∀ (A : Set ℕ), A.IsAsymptoticAddBasisOfOrder 2 →
      atTop.Tendsto (fun n => ncard_add_repr A 2 n) atTop → ∃ B ⊆ A,
      B.IsAsymptoticAddBasisOfOrder 2 ∧ ∀ b ∈ B, ¬(B \ {b}).IsAsymptoticAddBasisOfOrder 2

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

Erdos868.erdos_868.parts.ii

Solved: stated here without proof.

Let \(A\) be an additive basis of order \(2\), let \(f(n)\) denote the number of ways in which \(n\) can be written as the sum of two elements from \(A\). If \(f(n) > \epsilon \log n\) for large \(n\) and an arbitrary fixed \(\epsilon > 0\), then must \(A\) contain a minimal additive basis of order \(2\)?

Larsen and Larsen [LaLa26] constructed a counterexample with \(f(n) > c \log n\) for all large \(n\).

theorem erdos_868.parts.ii :
    ¬ ∀ᵉ (A : Set ℕ) (ε > 0), A.IsAsymptoticAddBasisOfOrder 2 →
      (∀ᶠ (n : ℕ) in atTop, ε * Real.log n < ncard_add_repr A 2 n) → ∃ B ⊆ A,
      B.IsAsymptoticAddBasisOfOrder 2 ∧ ∀ b ∈ B, ¬(B \ {b}).IsAsymptoticAddBasisOfOrder 2

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

Erdos868.erdos_868.variants.fixed_ε

Solved: stated here without proof.

Erdős and Nathanson proved that this is true if \(f(n) > c \log n\) for all large \(n\), for some fixed constant \(c > (\log \frac{4}{3})^{-1}\).

theorem erdos_868.variants.fixed_ε :
    ∀ᵉ (A : Set ℕ) (c > (Real.log (4 / 3))⁻¹), A.IsAsymptoticAddBasisOfOrder 2 →
      (∀ᶠ (n : ℕ) in atTop, c * Real.log n < ncard_add_repr A 2 n) → ∃ B ⊆ A,
      B.IsAsymptoticAddBasisOfOrder 2 ∧ ∀ b ∈ B, ¬(B \ {b}).IsAsymptoticAddBasisOfOrder 2

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

Erdos868.erdos_868.variants.Hartter_Nathanson

Solved: stated here; a Lean proof is at https://github.com/hjyuh/formal-conjectures/blob/e0da6ec78953b17618895a093d4bee90fd3f6f67/FormalConjectures/ErdosProblems/868.lean#L132.

Härtter and Nathanson proved that there exist additive bases which do not contain any minimal additive bases.

theorem erdos_868.variants.Hartter_Nathanson (o : ℕ) (ho : 1 < o) : ∃ (A : Set ℕ),
    A.IsAsymptoticAddBasisOfOrder o ∧ ∀ B ⊆ A, B.IsAsymptoticAddBasisOfOrder o →
    ∃ b ∈ B, (B \ {b}).IsAsymptoticAddBasisOfOrder o

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

Sources
LeanErdos868.erdos_868.parts.i · Erdos868.erdos_868.parts.ii · Erdos868.erdos_868.variants.fixed_ε · Erdos868.erdos_868.variants.Hartter_Nathanson

TheoremErdős Problem 869#

References: - erdosproblems.com/869 - [ErNa88] Erdős, Paul and Nathanson, Melvyn B., Partitions of bases into disjoint unions of bases. J. Number Theory (1988), 1-9. - [Er92c] Erdős, P., Some of my forgotten problems in number theory. Hardy-Ramanujan J. (1992), 34-50. - [La26] Larsen, D., Three questions of Erdős–Nathanson on asymptotic bases of order 2. arXiv:2603.03472 (2026).

Quoted from FormalConjectures/ErdosProblems/869.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/869.

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

Erdos869.erdos_869

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

If \(A_1, A_2\) are disjoint additive bases of order \(2\) (i.e. \(A_i + A_i\) contains all large integers) then must \(A = A_1 \cup A_2\) contain a minimal additive basis of order \(2\) (one such that deleting any element creates infinitely many \(n \notin A + A\))?

A question of Erdős and Nathanson [ErNa88, Er92c]. The answer is no: Larsen [La26] constructed disjoint bases \(A_1, A_2\) of order \(2\) such that \(A_1 \cup A_2\) contains no minimal basis of order \(2\).

theorem erdos_869 :
    ¬ ∀ (A₁ A₂ : Set ℕ), Disjoint A₁ A₂ →
      A₁.IsAsymptoticAddBasisOfOrder 2 → A₂.IsAsymptoticAddBasisOfOrder 2 →
      ∃ D ⊆ A₁ ∪ A₂, D.IsAsymptoticAddBasisOfOrder 2 ∧
        ∀ d ∈ D, ¬ (D \ {d}).IsAsymptoticAddBasisOfOrder 2

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

Sources
LeanErdos869.erdos_869

TheoremErdős Problem 871#

References: - erdosproblems.com/871 - [ErNa88] Erdős, Paul and Nathanson, Melvyn B., Partitions of bases into disjoint unions of bases. J. Number Theory (1988), 1-9. - [ErNa89] Erdős, Paul and Nathanson, Melvyn B., Additive bases with many representations. Acta Arith. (1989), 399-406.

Quoted from FormalConjectures/ErdosProblems/871.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/871.

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

Erdos871.erdos_871

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

Let \(A\) be an additive basis of order \(2\), and suppose \(1_A\ast 1_A(n)\to \infty\) as \(n\to \infty\). Can \(A\) be partitioned into two disjoint additive bases of order \(2\)?

A question of Erdős and Nathanson [ErNa88], who proved this is true if \(1_A\ast 1_A(n) > c\log n\) (for all large \(n\)) for some constant \(c>(\log\frac{4}{3})^{-1}\). Erdős and Nathanson [ErNa89] also proved that for every \(t\) there exists a basis \(A\) of order \(2\) such that \(1_A\ast 1_A(n)\geq t\) for all large \(n\) and yet \(A\) cannot be partitioned into two disjoint additive bases. This has been disproved by Larsen using Claude Opus 4.5 - in fact only a small modification of the argument of [ErNa89] is required.

theorem erdos_871 :
    ¬ ∀ (A : Set ℕ),
      (∀ᶠ n in Filter.atTop, ∃ a ∈ A, ∃ b ∈ A, a + b = n) ∧
      (∀ t, ∀ᶠ n in Filter.atTop, ∃ pairs : Finset (ℕ × ℕ),
        pairs.card ≥ t ∧
          ∀ p ∈ pairs, p.1 ∈ A ∧ p.2 ∈ A ∧ p.1 + p.2 = n ∧ p.1 ≤ p.2) →
      ∃ (B C : Set ℕ),
        (∀ x, x ∈ A ↔ x ∈ B ∨ x ∈ C) ∧
        Disjoint B C ∧
        (∀ᶠ n in Filter.atTop, ∃ a ∈ B, ∃ b ∈ B, a + b = n) ∧
        (∀ᶠ n in Filter.atTop, ∃ a ∈ C, ∃ b ∈ C, a + b = n)

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

Sources
LeanErdos871.erdos_871

TheoremErdős Problem 872#

This file states Erdős Problem 872 for the primitive-set saturation game on \(\{2, \dots, n\}\). The game value L n is defined by a finite minimax recursion: Prolonger moves first and maximizes the final size of the claimed primitive set, while Shortener minimizes it.

The problem statement does not fix the turn order. This file fixes Prolonger to move first, following the convention used in the forum discussion of the problem. The choice is not cosmetic: computational data suggests the Shortener-first value tracks \(\pi(n)\) while the Prolonger-first value grows linearly, and the questions below concern the Prolonger-first quantity.

References: - erdosproblems.com/872 - erdosproblems.com/forum/thread/872

Quoted from FormalConjectures/ErdosProblems/872.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/872.

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

Erdos872.erdos_872.parts.i

Open: stated without proof.

Erdős Problem 872, part (i) (weak form): there exists a constant \(\epsilon > 0\) such that the game length is at least \(\epsilon \cdot n\) for all sufficiently large \(n\).

theorem erdos_872.parts.i :
    ∃ ε > (0 : ℝ), ∀ᶠ n in atTop, (L n : ℝ) ≥ ε * n

Category research open; AMS 05 Combinatorics, 11 Number theory, 91 Game theory, economics, social and behavioral sciences. Declared in FormalConjectures/ErdosProblems/872.lean, line 161.

Erdos872.erdos_872.parts.ii

Solved: stated here; a Lean proof is at https://github.com/ilpauzner/formal-conjectures/blob/d9299da16287d2347e375d9eec253eec455bae75/FormalConjectures/ErdosProblems/872.lean#L1180.

Erdős Problem 872, part (ii) (strong form): for every \(\epsilon > 0\), the game length is at least \((1-\epsilon) \cdot n / 2\) for all sufficiently large \(n\).

The forum thread (April-May 2026) records Shortener strategies giving \(L(n) \leq (23/48 + o(1)) \cdot n\) (described in the thread as accepted as correct, with a Lean formalization in progress) and a claimed \(L(n) \leq 0.19 \cdot n\), either of which would answer this question negatively under the Prolonger-first convention.

The \(23/48\) upper bound for C-respecting plays (following old-bielefelder's strategy in the forum thread) was formalized in Lean 4 by Pommeret using Aristotle and Claude Opus 4.7, and completed to a proof for the full minimax game value L n by Ilia Pauzner using Gemini 4 Argon.

theorem erdos_872.parts.ii :
    ¬ ∀ ε > (0 : ℝ), ∀ᶠ n in atTop, (L n : ℝ) ≥ (1 - ε) * n / 2

Category research solved; AMS 05 Combinatorics, 11 Number theory, 91 Game theory, economics, social and behavioral sciences. Declared in FormalConjectures/ErdosProblems/872.lean, line 178.

Erdos872.erdos_872.trivial_upper_bound

Textbook result, proved here.

A trivial upper bound: a play can claim at most the \(n - 1\) elements of \(\{2, \dots, n\}\), so \(L(n) \leq n - 1\).

theorem erdos_872.trivial_upper_bound (n : ℕ) (hn : 2 ≤ n) :
    L n ≤ n - 1

Category textbook; AMS 05 Combinatorics, 11 Number theory, 91 Game theory, economics, social and behavioral sciences. Declared in FormalConjectures/ErdosProblems/872.lean, line 185.

Erdos872.erdos_872.variants.prime_question

Solved: stated here; a Lean proof is at https://github.com/mnn31/erdos-lean/blob/5cb725981b3ad137103ef908eb6ecff9e7ed9bdf/ErdosLean/Erdos872.lean#L114.

Forum-related variant: how small can a maximal primitive subset of \(\{2, \dots, n\}\) be? The set of primes in \(\{2, \dots, n\}\) is a maximal primitive subset of size \(\pi(n)\), and the forum thread asks whether this is the smallest possible for all \(n \geq 2\). Equivalently: must every completed play of the saturation game, by both players and regardless of strategy, claim at least \(\pi(n)\) elements? (Terminal positions of the game are exactly the maximal primitive subsets.)

The answer is yes. For each prime \(q \le n\), let \(q^k\) be the largest power of \(q\) that is at most \(n\). Maximality gives an element of \(A\) comparable with \(q^k\) under divisibility, and no element is comparable with two such prime powers, so \(|A| \ge \pi(n)\). This argument was posted on the forum by old-bielefelder (May 2026); the statement also appears as Theorem 2.3(i) of [El23] S. Elsakhawy, Independence and domination in divisor graph and mod-difference graphs, J. Egyptian Math. Soc. 31 (2023).

theorem erdos_872.variants.prime_question :
    ∀ n ≥ 2, ∀ A : Finset ℕ, Maximal (IsPrimitive n) A →
      ((Finset.Icc 2 n).filter Nat.Prime).card ≤ A.card

Category research solved; AMS 05 Combinatorics, 11 Number theory, 91 Game theory, economics, social and behavioral sciences. Declared in FormalConjectures/ErdosProblems/872.lean, line 208.

Sources
LeanErdos872.erdos_872.parts.i · Erdos872.erdos_872.parts.ii · Erdos872.erdos_872.trivial_upper_bound · Erdos872.erdos_872.variants.prime_question

TheoremErdős Problem 873#

References: - erdosproblems.com/873 - [Er92c] Erdős, P., Some of my forgotten problems in number theory. Hardy-Ramanujan J. 15 (1992), 34-50.

Quoted from FormalConjectures/ErdosProblems/873.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/873.

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

Erdos873.erdos_873

Open: stated without proof.

Let \(A = \{a_1 < a_2 < \dots\} \subseteq \mathbb{N}\) and let \(F(A,X,k)\) count the number of \(i\) such that \([a_i,a_{i+1}, \dots ,a_{i+k−1}] < X\), where the left-hand side is the least common multiple. Is it true that, for every \(\epsilon > 0\), there exists some \(k\) such that \(F(A,X,k) < X^\epsilon\)?

theorem erdos_873 : ∀ᵉ (a : ℕ → ℕ) (ε > (0 : ℝ)), 0 < a 0 → StrictMono a →
    ∃ k, ∀ X > 0, F a X k < (X^ε).toEReal

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

Erdos873.erdos_873.variants.triple_upper_bound

Solved: stated here without proof.

The upper bound (2).

theorem erdos_873.variants.triple_upper_bound :
    ∃ C : ℝ, 0 < C ∧
      ∀ (a : ℕ → ℕ), 0 < a 0 → StrictMono a →
        ∀ᶠ X : ℝ in Filter.atTop,
          (F a X 3 : EReal) ≤
            (C * X ^ (1 / 3 : ℝ) * Real.log X).toEReal

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

Erdos873.erdos_873.variants.triple_lower_bound_infinitely_often

Solved: stated here without proof.

The infinitely-often lower bound (3).

theorem erdos_873.variants.triple_lower_bound_infinitely_often :
    ∃ (a : ℕ → ℕ) (c : ℝ),
      0 < a 0 ∧ StrictMono a ∧ 0 < c ∧
        ∀ X₀ : ℝ, ∃ X > X₀,
          (c * X ^ (1 / 3 : ℝ) * Real.log X).toEReal ≤ (F a X 3 : EReal)

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

Erdos873.erdos_873.variants.supplement_all_scale

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-873-lean/blob/44cbf183239517795522bd3f18124b08c095cc6d/lean/RealBridge.lean#L138-L146.

There may be a sequence for which the lower bound in (3) holds for every \(X\), that is, for all sufficiently large \(X\) rather than only for infinitely many \(X\). (Asking it for every \(X > 0\) fails trivially: the lcm of three distinct positive integers is at least \(4\), so \(F(A,X,3) = 0\) for \(X \le 4\).)

theorem erdos_873.variants.supplement_all_scale :
    ¬ ∃ (a : ℕ → ℕ) (c : ℝ),
      0 < a 0 ∧ StrictMono a ∧ 0 < c ∧
        ∀ᶠ X : ℝ in Filter.atTop,
          (c * X ^ (1 / 3 : ℝ) * Real.log X).toEReal ≤ (F a X 3 : EReal)

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

Sources
LeanErdos873.erdos_873 · Erdos873.erdos_873.variants.triple_upper_bound · Erdos873.erdos_873.variants.triple_lower_bound_infinitely_often · Erdos873.erdos_873.variants.supplement_all_scale

TheoremErdős Problem 875#

References: - erdosproblems.com/875 - [Er98] Erdős, P., Some of my new and almost new problems and results in combinatorial number theory. Number theory (Eger, 1996) (1998), 169-180. - [Er62c] Erdős, P., Some remarks on number theory. III (in Hungarian). Mat. Lapok 13 (1962), 28-38. PDF - [ENS91] Erdős, P., Nicolas, J.-L. and Sárközy, A., Sommes de sous-ensembles. J. Théor. Nombres Bordeaux 3 (1991), 55-72. Numdam - [DeFr99] Deshouillers, J.-M. and Freiman, G. A., On an additive problem of Erdős and Straus, 2. Astérisque 258 (1999), 141-148. Numdam

The finite version of this problem is erdosproblems.com/874.

Quoted from FormalConjectures/ErdosProblems/875.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/875.

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

Erdos875.erdos_875

Open: stated without proof.

Let \(A=\{a_1\lt a_2\lt \cdots\}\subset \mathbb{N}\) be an infinite set such that the sets

\[S_r = \{ a_1+\cdots +a_r : a_1\lt \cdots\lt a_r\in A\}\]

are disjoint for distinct \(r\geq 1\). How fast can such a sequence grow? How small can \(a_{n+1}-a_n\) be? In particular, for which \(c\) is it possible that \(a_{n+1}-a_n\leq n^{c}\)?

A problem of Deshouillers and Erdős [Er98] (an infinite version of 874). Such sets are sometimes called admissible. We state the last question: the set of such \(c\) is erdos_875.answer. The bound is required for all large \(n\), since otherwise the first few \(n\) would constrain the answer. The first two questions are not formalised separately. Erdős also writes that it is not completely trivial to find such a sequence with \(a_{n+1}/a_n\to 1\) (not formalised).

theorem erdos_875 :
    {c : ℝ | ∃ A : Set ℕ, A.Infinite ∧ IsAdmissible A ∧
      ∀ᶠ n : ℕ in atTop, (gap A n : ℝ) ≤ (n : ℝ) ^ c} = erdos_875.answer

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

Erdos875.erdos_875.variants.erdos_nicolas_sarkozy

Solved: stated here without proof.

Erdős, Nicolas and Sárközy [ENS91, Theorem 2] constructed an infinite admissible set \(A\) with

\[A(x)=\lvert\{a\in A: a\leq x\}\rvert \gg x^{5-2\sqrt6}.\]

The implied constant is positive and the inequality is required for all large \(x\). This improves a result of Erdős [Er62c], who obtained \(A(x)\gg x^{c}\) for some unspecified \(c>0\).

theorem erdos_875.variants.erdos_nicolas_sarkozy :
    ∃ A : Set ℕ, A.Infinite ∧ IsAdmissible A ∧ ∃ c : ℝ, 0 < c ∧
      ∀ᶠ x : ℕ in atTop, c * (x : ℝ) ^ (5 - 2 * Real.sqrt 6) ≤ (countingFunction A x : ℝ)

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

Erdos875.erdos_875.variants.polynomial_gaps

Solved: stated here without proof.

Since \(5-2\sqrt6=(5+2\sqrt6)^{-1}\), the result of [ENS91, Theorem 2] gives \(a_n\ll n^{5+2\sqrt6}\), hence \(a_{n+1}-a_n\leq a_{n+1}\ll n^{5+2\sqrt6}\). So every \(c>5+2\sqrt6\) is possible in the main question.

theorem erdos_875.variants.polynomial_gaps (c : ℝ) (hc : 5 + 2 * Real.sqrt 6 < c) :
    ∃ A : Set ℕ, A.Infinite ∧ IsAdmissible A ∧
      ∀ᶠ n : ℕ in atTop, (gap A n : ℝ) ≤ (n : ℝ) ^ c

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

Erdos875.erdos_875.variants.deshouillers_freiman

Solved: stated here without proof.

Deshouillers and Freiman [DeFr99, Theorem 1] proved a conjecture of Erdős on the finite version (874): for all sufficiently large \(N\), every admissible set \(A\subseteq\{1,\ldots,N\}\) satisfies

\[\lvert A\rvert\leq 2\sqrt{N+\tfrac14}-1.\]

This is sharp: by Straus, the set of \(k\) consecutive integers ending at \(N\) is admissible if and only if \(k\leq 2\sqrt{N+\frac14}-1\).

theorem erdos_875.variants.deshouillers_freiman :
    ∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N → ∀ A : Finset ℕ, (A : Set ℕ) ⊆ Set.Icc 1 N →
      IsAdmissible (A : Set ℕ) → (A.card : ℝ) ≤ 2 * Real.sqrt ((N : ℝ) + 1 / 4) - 1

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

Sources
LeanErdos875.erdos_875 · Erdos875.erdos_875.variants.erdos_nicolas_sarkozy · Erdos875.erdos_875.variants.polynomial_gaps · Erdos875.erdos_875.variants.deshouillers_freiman

TheoremErdős Problem 876#

References: - erdosproblems.com/876 - [Er62c] Erdős, P., Some remarks on number theory. III (in Hungarian). Mat. Lapok 13 (1962), 28-38. PDF - [Er75b] Erdős, P., Problems and results in combinatorial number theory. Journées Arithmétiques de Bordeaux (Conf., Univ. Bordeaux, 1974), Astérisque 24-25 (1975), 295-310. PDF - [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 (1977), 43-72. PDF - [Er98] Erdős, P., Some of my new and almost new problems and results in combinatorial number theory. Number theory (Eger, 1996) (1998), 169-180. - [DEM99] Deshouillers, J.-M., Erdős, P. and Melfi, G., On a question about sum-free sequences. Discrete Math. 200 (1999), 49-54. - [LeOS77] Levine, E. and O'Sullivan, J., An upper estimate for the reciprocal sum of a sum-free sequence. Acta Arith. 34 (1977), 9-24. - [Ab87] Abbott, H. L., On sum-free sequences. Acta Arith. 48 (1987), 93-96.

See also erdosproblems.com/790.

Quoted from FormalConjectures/ErdosProblems/876.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/876.

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

Erdos876.erdos_876.parts.i

Open: stated without proof.

Let \(A=\{a_1\lt a_2\lt \cdots\}\subset \mathbb{N}\) be an infinite sum-free set - that is, there are no solutions to

\[a=b_1+\cdots+b_r\]

with \(b_1\lt \cdots\lt b_r\lt a\in A\). How small can \(a_{n+1}-a_n\) be? Is it possible that \(a_{n+1}-a_n\lt n\)?

The gap question is discussed by Erdős in [Er98]. We state the second question. The inequality \(a_{n+1}-a_n\lt n\) is required for all large \(n\), because it fails for \(n=1\). The first question is vaguer and is not formalised.

theorem erdos_876.parts.i :
    ∃ A : Set ℕ, A.Infinite ∧ IsSubsetSumFree A ∧ ∀ᶠ n : ℕ in atTop, gap A n < n

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

Erdos876.erdos_876.parts.ii

Open: stated without proof.

In [Er75b] and [Er77c] Erdős asks to determine the maximum possible value of \(\sum_{n\in A}\frac{1}{n}\). Erdős had proved this is \(<100\), and Sullivan had shown that this is \(<4\), and Sullivan conjectured the maximum is slightly larger than \(2\) [Er77c, p. 52].

Here \(A\) ranges over infinite sum-free sets, and the maximum is read as the supremum maxRecipSum.

theorem erdos_876.parts.ii : maxRecipSum = erdos_876.parts.ii.answer

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

Erdos876.erdos_876.variants.density_zero

Solved: stated here without proof.

Erdős [Er62c, Theorem I] proved that a sum-free set has density zero (restated as [DEM99, Theorem 1]).

theorem erdos_876.variants.density_zero (A : Set ℕ) (hA : A.Infinite) (hs : IsSubsetSumFree A) :
    A.HasDensity 0

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

Erdos876.erdos_876.variants.recip_sum_lt

Solved: stated here without proof.

Erdős [Er62c, Theorem II] proved that \(\sum_{a\in A}1/a\) converges and is \(<103\) for every infinite sum-free set \(A\); see also [Er75b, p. 302] and [DEM99, p. 49]. The later paper [Er77c, p. 52] states the bound as \(100\).

theorem erdos_876.variants.recip_sum_lt (A : Set ℕ) (hA : A.Infinite) (hs : IsSubsetSumFree A) :
    ∃ s : ℝ, s < 103 ∧ HasSum (fun a : A ↦ (1 : ℝ) / (a : ℕ)) s

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

Erdos876.erdos_876.variants.recip_sum_bounds

Solved: stated here without proof.

Let \(R\) be the supremum of \(\sum_j 1/n_j\) over sum-free sequences \(\{n_j\}\). Levine and O'Sullivan [LeOS77] proved \(R<4\) (and \(R>2.035\)), and Abbott [Ab87] improved the lower bound to \(R>2.064\), as reported in [DEM99, p. 50].

theorem erdos_876.variants.recip_sum_bounds : 2.064 < maxRecipSum ∧ maxRecipSum < 4

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

Erdos876.erdos_876.variants.dem_ratio

Solved: stated here without proof.

Deshouillers, Erdős and Melfi [DEM99, Theorem 3] constructed an infinite sum-free set with \(a_{n+1}/a_n\to 1\).

theorem erdos_876.variants.dem_ratio :
    ∃ A : Set ℕ, A.Infinite ∧ IsSubsetSumFree A ∧
      Tendsto (fun k : ℕ ↦ (Nat.nth (· ∈ A) (k + 1) : ℝ) / (Nat.nth (· ∈ A) k : ℝ))
        atTop (nhds 1)

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

Erdos876.erdos_876.variants.dem_polynomial

Solved: stated here without proof.

Deshouillers, Erdős and Melfi [DEM99, Theorem 4] proved that for every \(\delta>0\) there is an infinite sum-free set with \(a_n\sim n^{3+\delta}\); we state the consequence \(a_n\ll n^{3+\delta}\). The site writes \(a_n\sim n^{3+o(1)}\).

theorem erdos_876.variants.dem_polynomial (δ : ℝ) (hδ : 0 < δ) :
    ∃ A : Set ℕ, A.Infinite ∧ IsSubsetSumFree A ∧
      ∃ C : ℝ, ∀ k : ℕ, (Nat.nth (· ∈ A) k : ℝ) ≤ C * ((k : ℝ) + 1) ^ (3 + δ)

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

Sources
LeanErdos876.erdos_876.parts.i · Erdos876.erdos_876.parts.ii · Erdos876.erdos_876.variants.density_zero · Erdos876.erdos_876.variants.recip_sum_lt · Erdos876.erdos_876.variants.recip_sum_bounds · Erdos876.erdos_876.variants.dem_ratio · Erdos876.erdos_876.variants.dem_polynomial

TheoremErdős Problem 877#

References: - erdosproblems.com/877 - [CaEr90] Cameron, P. J. and Erdős, P., On the number of sets of integers with various properties. (1990), 61-79. - [Er98] Erdős, Paul, Some of my new and almost new problems and results in combinatorial number theory. Number theory (Eger, 1996) (1998), 169-180. - [LuSc01] Łuczak, Tomasz and Schoen, Tomasz, On the number of maximal sum-free sets. Proc. Amer. Math. Soc. (2001), 2205--2207. - [BLST15] Balogh, József and Liu, Hong and Sharifzadeh, Maryam and Treglown, Andrew, The number of maximal sum-free subsets of integers. Proc. Amer. Math. Soc. (2015), 4713--4721. - [BLST18] Balogh, József and Liu, Hong and Sharifzadeh, Maryam and Treglown, Andrew, Sharp bound on the number of maximal sum-free subsets of integers. J. Eur. Math. Soc. (JEMS) (2018), 1885--1911.

Quoted from FormalConjectures/ErdosProblems/877.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/877.

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

Erdos877.erdos_877

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

Let \(f_m(n)\) count the number of maximal sum-free subsets \(A\subseteq\{1,\ldots,n\}\) - that is, there are no solutions to \(a=b+c\) in \(A\) and \(A\) is maximal with this property. Estimate \(f(n)\) - is it true that \(f_m(n)=o(2^{n/2})\)?

A problem of Cameron and Erdős. Łuczak and Schoen [LuSc01] proved that there exists a constant \(c<1/2\) such that \(f_m(n)<2^{cn}\), resolving this question. Balogh, Liu, Sharifzadeh, and Treglown [BLST15] proved that \(f_m(n)=2^{(\frac{1}{4}+o(1))n}\).

See 748 for the non-maximal case.

theorem erdos_877 :
    (fun n : ℕ ↦ (fm n : ℝ)) =o[atTop] fun n : ℕ ↦ (2 : ℝ) ^ ((n : ℝ) / 2)

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

Erdos877.erdos_877.variants.luczak_schoen

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

Łuczak and Schoen [LuSc01] proved that there exists a constant \(c<1/2\) such that \(f_m(n)<2^{cn}\) for all large \(n\).

theorem erdos_877.variants.luczak_schoen :
    ∃ c : ℝ, c < 1 / 2 ∧ ∀ᶠ n : ℕ in atTop, (fm n : ℝ) ≤ 2 ^ (c * n)

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

Erdos877.erdos_877.variants.cameron_erdos

Solved: stated here without proof.

Cameron and Erdős [CaEr90] proved that \(f_m(n)>2^{n/4}\).

theorem erdos_877.variants.cameron_erdos :
    ∀ᶠ n : ℕ in atTop, (2 : ℝ) ^ ((n : ℝ) / 4) < fm n

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

Erdos877.erdos_877.variants.balogh_liu_sharifzadeh_treglown

Solved: stated here without proof.

Balogh, Liu, Sharifzadeh, and Treglown [BLST15] proved that \(f_m(n)=2^{(\frac{1}{4}+o(1))n}\).

theorem erdos_877.variants.balogh_liu_sharifzadeh_treglown :
    Tendsto (fun n : ℕ ↦ logb 2 (fm n) / n) atTop (nhds (1 / 4))

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

Sources
LeanErdos877.erdos_877 · Erdos877.erdos_877.variants.luczak_schoen · Erdos877.erdos_877.variants.cameron_erdos · Erdos877.erdos_877.variants.balogh_liu_sharifzadeh_treglown

TheoremErdős Problem 878#

References: - erdosproblems.com/878 - [Er84e] Erdős, P., On two unconventional number theoretic functions and on some related problems. (1984), 113--121. - [Ki26] Kitamura, K., Erdős Problem #878 in Lean, GitHub repository (2026).

Quoted from FormalConjectures/ErdosProblems/878.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/878.

The file states 14 research or textbook statements: 3 open and 11 solved.

Erdos878.erdos_878.parts.i

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-878-lean/blob/d4a8eecf0606b3eee7342c2040a31c8c30eb5d76/lean/Erdos878/FixedLoss.lean#L120.

Is it true that, for almost all \(n\), \(f(n)=o(n\log\log n)\) and \(F(n)\gg n\log\log n\)?

The answer is yes; a Lean proof is given in [Ki26].

theorem erdos_878.parts.i :
    ∃ A : Set ℕ, A.HasDensity 1 ∧
      (fun n : A ↦ (f n : ℝ)) =o[atTop]
        (fun n : A ↦ (n : ℝ) * Real.log (Real.log (n : ℝ))) ∧
      (fun n : A ↦ (n : ℝ) * Real.log (Real.log (n : ℝ))) =O[atTop]
        (fun n : A ↦ (F n : ℝ))

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

Erdos878.erdos_878.parts.ii

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-878-lean/blob/d4a8eecf0606b3eee7342c2040a31c8c30eb5d76/lean/Erdos878/TrackBEndpointParameters.lean#L630.

Is it true that \(\max_{n\le x}f(n)\sim x\log x/\log\log x\)?

The answer is yes; a Lean proof is given in [Ki26].

theorem erdos_878.parts.ii :
    Tendsto (fun x : ℕ ↦
        (maxUpTo f x : ℝ) / ((x : ℝ) * Real.log x / Real.log (Real.log x)))
        atTop (𝓝 1)

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

Erdos878.erdos_878.parts.iii_all

Solved: stated here without proof.

Is it true that, for all \(x\), \(\max_{n\le x}f(n)=\max_{n\le x}F(n)\)? Barreto noted that this is false at \(x=210\).

theorem erdos_878.parts.iii_all :
    ¬ ∀ x : ℕ, maxUpTo f x = maxUpTo F x

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

Erdos878.erdos_878.parts.iii_eventually

Solved: stated here; a Lean proof is at https://github.com/ilpauzner/formal-conjectures/blob/b7742e7d900ca30503c0dd4c940625a6d9cf0a0c/FormalConjectures/ErdosProblems/878.lean#L435.

Is it true that, for all large \(x\), \(\max_{n\le x}f(n)=\max_{n\le x}F(n)\)?

This is false, as formalized in Lean 4 by Ilia Pauzner using Gemini 4 Argon.

theorem erdos_878.parts.iii_eventually :
    ¬ ∀ᶠ x : ℕ in atTop, maxUpTo f x = maxUpTo F x

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

Erdos878.erdos_878.parts.iv

Open: stated without proof.

Find an asymptotic formula for the number of \(n\lt x\) such that \(f(n)=F(n)\).

theorem erdos_878.parts.iv :
    (fun x : ℕ ↦
      (((Finset.Ico 1 x).filter fun n ↦ f n = F n).card : ℝ))
      ~[atTop] erdos_878.parts.iv.answer

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

Erdos878.erdos_878.parts.v

Open: stated without proof.

Find an asymptotic formula for \(H(x)=\sum_{n\lt x}f(n)/n\).

theorem erdos_878.parts.v :
    H ~[atTop] erdos_878.parts.v.answer

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

Erdos878.erdos_878.parts.vi

Open: stated without proof.

Is it true that \(H(x)\ll x\log\log\log\log x\)?

theorem erdos_878.parts.vi :
    H =O[atTop] fun x : ℕ ↦
        (x : ℝ) * Real.log (Real.log (Real.log (Real.log (x : ℝ))))

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

Erdos878.erdos_878.variants.second_question_subsequence

Solved: stated here without proof.

Erdős [Er84e] proved that \(\max_{n\le x}f(n)\sim x\log x/\log\log x\) for a sequence of \(x\to\infty\).

theorem erdos_878.variants.second_question_subsequence :
    ∃ X : ℕ → ℕ, Tendsto X atTop atTop ∧
      Tendsto (fun k : ℕ ↦
        (maxUpTo f (X k) : ℝ) /
          ((X k : ℝ) * Real.log (X k) / Real.log (Real.log (X k))))
        atTop (𝓝 1)

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

Erdos878.erdos_878.variants.proposed_first_question_sharp

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-878-lean/blob/d4a8eecf0606b3eee7342c2040a31c8c30eb5d76/lean/Erdos878/SharpFirstAsymptotic.lean#L168.

For almost all \(n\), \(F(n)\sim \frac12 n\log\log n\). A Lean proof is given in [Ki26].

theorem erdos_878.variants.proposed_first_question_sharp :
    ∃ A : Set ℕ, A.HasDensity 1 ∧
      Tendsto (fun n : A ↦
        (F n : ℝ) / ((n : ℝ) * Real.log (Real.log (n : ℝ))))
        atTop (𝓝 (1 / 2 : ℝ))

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

Erdos878.erdos_878.variants.H_div_self_limsup_infinite

Solved: stated here without proof.

Erdős [Er84e] showed that \(\limsup_{x\to\infty}H(x)/x=\infty\).

theorem erdos_878.variants.H_div_self_limsup_infinite :
    ∀ C : ℝ, ∃ᶠ x : ℕ in atTop, C ≤ H x / (x : ℝ)

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

Erdos878.erdos_878.variants.H_div_self_liminf_finite

Solved: stated here without proof.

Erdős [Er84e] showed that \(\liminf_{x\to\infty}H(x)/x\lt \infty\).

theorem erdos_878.variants.H_div_self_liminf_finite :
    ∃ C : ℝ, ∃ᶠ x : ℕ in atTop, H x / (x : ℝ) ≤ C

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

Erdos878.erdos_878.variants.H_upper_triple_log

Solved: stated here without proof.

Erdős [Er84e] proved that \(H(x)\ll x\log\log\log x\).

theorem erdos_878.variants.H_upper_triple_log :
    H =O[atTop] fun x : ℕ ↦
      (x : ℝ) * Real.log (Real.log (Real.log (x : ℝ)))

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

Erdos878.erdos_878.variants.H_lower_quadruple_log_infinitely_often

Solved: stated here without proof.

Erdős [Er84e] proved that \(x\log\log\log\log x\ll H(x)\); this entry records the infinitely-often consequence.

theorem erdos_878.variants.H_lower_quadruple_log_infinitely_often :
    ∃ c : ℝ, 0 < c ∧ ∃ᶠ x : ℕ in atTop,
      c * ((x : ℝ) * Real.log (Real.log (Real.log (Real.log (x : ℝ))))) ≤ H x

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

Erdos878.erdos_878.variants.original_formula_17

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-878-lean/blob/d4a8eecf0606b3eee7342c2040a31c8c30eb5d76/lean/Erdos878/Formula17.lean#L192.

Formula (17) of [Er84e]: does \((x h(x)-m(x))/x\to\infty\)?

The answer is yes; a Lean proof is given in [Ki26].

theorem erdos_878.variants.original_formula_17 :
    Tendsto (fun x : ℕ ↦
        ((x * h x - m x : ℕ) : ℝ) / (x : ℝ)) atTop atTop

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

Sources
LeanErdos878.erdos_878.parts.i · Erdos878.erdos_878.parts.ii · Erdos878.erdos_878.parts.iii_all · Erdos878.erdos_878.parts.iii_eventually · Erdos878.erdos_878.parts.iv · Erdos878.erdos_878.parts.v · Erdos878.erdos_878.parts.vi · Erdos878.erdos_878.variants.second_question_subsequence · Erdos878.erdos_878.variants.proposed_first_question_sharp · Erdos878.erdos_878.variants.H_div_self_limsup_infinite · Erdos878.erdos_878.variants.H_div_self_liminf_finite · Erdos878.erdos_878.variants.H_upper_triple_log · Erdos878.erdos_878.variants.H_lower_quadruple_log_infinitely_often · Erdos878.erdos_878.variants.original_formula_17

TheoremErdős Problem 881#

Reference: erdosproblems.com/881

Quoted from FormalConjectures/ErdosProblems/881.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/881.

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

Erdos881.erdos_881

Open: stated without proof.

Let A ⊂ ℕ be an additive basis of order k which is minimal in the sense that if B ⊂ A is any infinite set, then A \ B is not a basis of order k.

Must there exist an infinite B ⊂ A such that A \ B is an additive basis of order k + 1?

theorem erdos_881 :
    ∀ (k : ℕ) (A : Set ℕ),
      IsMinimalAsymptoticAddBasisOfOrder k A →
        ∃ (B : Set ℕ), B ⊆ A ∧ B.Infinite ∧
          (A \ B).IsAsymptoticAddBasisOfOrder (k + 1)

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

Sources
LeanErdos881.erdos_881

TheoremErdős Problem 882#

References: - erdosproblems.com/882 - [Er98] Erdős, Paul, Some of my new and almost new problems and results in combinatorial number theory. Number theory (Eger, 1996) (1998), 169-180. - [ELRSS99] Erdős, P., Lev, V., Rauzy, G., Sándor, C. and Sárközy, A., Greedy algorithm, arithmetic progressions, subset sums and divisibility. Discrete Math. (1999), 119-135. - Erdős Problem 1 for the upper bound. - [Alexeev] Boris Alexeev's sorry-free Lean 4 formalisation of the lower bound, plby/lean-proofs.

Quoted from FormalConjectures/ErdosProblems/882.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/882.

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

Erdos882.erdos_882

Solved: stated here without proof.

What is the size of the largest \(A\subseteq \{1,\ldots,n\}\) such that in the set

\[\left\{ \sum_{a\in S} a : \emptyset\neq S\subseteq A\right\}\]

no two distinct elements divide each other?

A problem of Erdős and Sárközy. The answer is \((1+o(1))\log_2 n\): the lower bound \(\lvert A\rvert > \log_2 n - 1\) is achieved by the construction of Erdős, Lev, Rauzy, Sándor and Sárközy [ELRSS99] (see erdos_882.variants.lower_bound), while Erdős Problem 1 gives \(\lvert A\rvert \leq \log_2 n + \tfrac{1}{2}\log_2\log n + O(1)\).

theorem erdos_882 :
    Filter.Tendsto (fun n : ℕ => (maxAntichainCard n : ℝ) / Real.logb 2 n)
      Filter.atTop (nhds 1)

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

Erdos882.erdos_882.variants.lower_bound

Solved: stated here; a Lean proof is at https://github.com/ToshiDad/erdos-882/blob/6ea233aed4b3efce92e2754177ef15c4085f8732/Erdos882.lean#L394.

Erdős, Lev, Rauzy, Sándor and Sárközy [ELRSS99] proved that \(\lvert A\rvert > \log_2 n - 1\) is achievable, taking \(A = \{2^m - 2^{m-1}, 2^m - 2^{m-2}, \ldots, 2^m - 1\}\).

The key property of this construction is that distinct nonempty subsets have subset sums which never divide one another.

The linked theorem no_div is phrased in terms of index sets \(S \subseteq \{0, \ldots, m-1\}\), i.e. \(\sum_{i \in S_1} (2^m - 2^i) \nmid \sum_{i \in S_2} (2^m - 2^i)\) for distinct nonempty \(S_1, S_2\); it transfers to subsets of A m via the injectivity of \(i \mapsto 2^m - 2^i\) (see card_A).

theorem erdos_882.variants.lower_bound (m : ℕ) : IsSubsetSumAntichain (A m)

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

Erdos882.erdos_882.variants.lower_bound_explicit

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

The lower bound of [ELRSS99] in quantitative form: for every \(n \geq 1\) there is a subset-sum antichain \(A \subseteq \{1, \ldots, n\}\) with \(\lvert A\rvert > \log_2 n - 1\), namely \(A_m\) with \(m = \lfloor \log_2 n \rfloor\) (by erdos_882.variants.lower_bound, A_subset_Icc and card_A).

A sorry-free Lean 4 proof of this statement is the theorem erdos_882 of [Alexeev]. That formalisation expresses the antichain condition as primitivity of the set of nonempty subset sums (no element divides another one). For \(A \subseteq \{1, \ldots, n\}\) this is equivalent to IsSubsetSumAntichain A: if two distinct subsets had the same sum, then removing their common elements would leave two disjoint nonempty subsets with a common sum \(t \geq 1\), so that \(t\) and \(2t\) would both be nonempty subset sums.

theorem erdos_882.variants.lower_bound_explicit (n : ℕ) (hn : 0 < n) :
    Real.logb 2 n - 1 < (maxAntichainCard n : ℝ)

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

Erdos882.erdos_882.variants.sandor

Solved: stated here without proof.

Sándor's construction (reported without reference in [Er98]) is claimed to achieve \(\lvert A\rvert = (1-o(1))\log_2 n\) with \(A = \{2^i + m 2^m : 0 \leq i < m\}\) and \(n = 2^{m-1} + m 2^m\).

theorem erdos_882.variants.sandor (m : ℕ) (hm : 1 ≤ m) :
    IsSubsetSumAntichain ((Finset.range m).image (fun i => 2 ^ i + m * 2 ^ m))

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

Erdos882.erdos_882.variants.greedy

Solved: stated here without proof.

The greedy algorithm shows that \(\lvert A\rvert \geq (1-o(1))\log_3 n\) is possible.

theorem erdos_882.variants.greedy :
    ∀ᶠ n : ℕ in Filter.atTop, (Real.logb 3 n - 1 : ℝ) ≤ (maxAntichainCard n : ℝ)

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

Sources
LeanErdos882.erdos_882 · Erdos882.erdos_882.variants.lower_bound · Erdos882.erdos_882.variants.lower_bound_explicit · Erdos882.erdos_882.variants.sandor · Erdos882.erdos_882.variants.greedy

TheoremErdős Problem 883#

References: - erdosproblems.com/883 - [ErSa97] Erdős, P. and Sárközy, G. N., On cycles in the coprime graph of integers. Electron. J. Combin. (1997), Research Paper 8. - [Sa99] Sárközy, G. N., Complete tripartite subgraphs in the coprime graph of integers. Discrete Math. (1999), 227-238.

Quoted from FormalConjectures/ErdosProblems/883.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/883.

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

Erdos883.erdos_883.parts.i

Open: stated without proof.

For \(A\subseteq \{1,\ldots,n\}\) let \(G(A)\) be the graph with vertex set \(A\), where two integers are joined by an edge if they are coprime.

Is it true that if

\[|A| > \lfloor n/2 \rfloor + \lfloor n/3 \rfloor - \lfloor n/6 \rfloor\]

then \(G(A)\) contains all odd cycles of length \(\leq n/3 + 1\)?

A problem of Erdős and Sárközy [ErSa97].

theorem erdos_883.parts.i :
    ∀ (n : ℕ) (A : Finset ℕ),
      A ⊆ Finset.Icc 1 n →
      n / 2 + n / 3 - n / 6 < A.card →
      ∀ l : ℕ, Odd l → 3 ≤ l → l ≤ n / 3 + 1 →
        l ∈ (coprimeGraph.induce (A : Set ℕ)).oddCycleLengths

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

Erdos883.erdos_883.parts.ii

Solved: stated here without proof.

Is it true that, for every \(\ell\geq 1\), if \(n\) is sufficiently large and

\[|A| > \lfloor n/2\rfloor + \lfloor n/3\rfloor - \lfloor n/6\rfloor\]

then \(G(A)\) must contain a complete \((1,\ell,\ell)\) tripartite graph on \(2\ell+1\) vertices?

The second question was solved by Sárközy [Sa99], who proved this with \(\ell \gg \log n/\log\log n\).

theorem erdos_883.parts.ii :
    ∀ l : ℕ, 1 ≤ l → ∀ᶠ n : ℕ in atTop, ∀ A : Finset ℕ,
      A ⊆ Finset.Icc 1 n →
      n / 2 + n / 3 - n / 6 < A.card →
      (SimpleGraph.completeMultipartiteGraph (fun i : Fin 3 ↦ Fin (![1, l, l] i))).IsContained
        (coprimeGraph.induce (A : Set ℕ))

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

Sources
LeanErdos883.erdos_883.parts.i · Erdos883.erdos_883.parts.ii

TheoremErdős Problem 884#

References: - erdosproblems.com/884 - Tao25 - Larsen

Quoted from FormalConjectures/ErdosProblems/884.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/884.

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

Erdos884.erdos_884

Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/f8a51976fd2e66a52b4928c109fb9ae877a1a507/problems/884/Erdos884.lean.

For a natural number n, let \(1 = d_1 < \dotsc < d_{\tau(n)} = n\) denote the divisors of \(n\) in increasing order. Does it hold that \(\sum_{1 \le i < j \le \tau(n)} \frac{1}{d_j - d_i} \ll 1 + \sum_{1 \le i < \tau(n)} \frac{1}{d_{i + 1} - d_i}\) for \(n \to \infty\), i.e. \(\sum_{1 \le i < j \le \tau(n)} \frac{1}{d_j - d_i} \in O \left( 1 + \sum_{1 \le i < \tau(n)} \frac{1}{d_{i + 1} - d_i} \right)\)?

This conjecture has been disproved: - In September 2025, Terence Tao gave a conditional negative answer assuming the prime tuples conjecture, see erdos_884_false_of_hardy_littlewood for this implication. - Daniel Larsen subsequently gave an unconditional disproof.

Reference: erdosproblems.com/884

theorem erdos_884 :
    ¬ Erdos884Prop

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

Erdos884.erdos_884_false_of_hardy_littlewood

Solved: stated here without proof.

In September 2025, Terence Tao gave a conditional negative answer to Erdős problem 884, disproving it under the assumption of the qualitative Hardy–Littlewood prime tuples conjecture, see Conjecture 1.1 and Theorem 1.1 of Tao25.

The qualitative conjecture states that for every admissible tuple \((h_1, \dotsc, h_k)\) of integers, i.e. one which avoids at least one residue class modulo \(p\) for every prime \(p\), there are infinitely many natural numbers \(n\) such that \(n + h_1, \dotsc, n + h_k\) are all prime. Unlike the full Hardy–Littlewood conjecture, it does not give an asymptotic for the number of such \(n\).

theorem erdos_884_false_of_hardy_littlewood
    (hHL : ∀ H : Finset ℤ, (∀ p : ℕ, p.Prime → ∃ a : ℤ, ∀ h ∈ H, ¬ (p : ℤ) ∣ a + h) →
      {n : ℕ | ∀ h ∈ H, Prime ((n : ℤ) + h)}.Infinite) :
    ¬Erdos884Prop

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

Sources
LeanErdos884.erdos_884 · Erdos884.erdos_884_false_of_hardy_littlewood

TheoremErdős Problem 885#

References: - erdosproblems.com/885 - [ErRo97] Erdős, P. and Rosenfeld, M., The factor-difference set of integers. (1997) - [Ji99] Jiménez-Urroz, J., A note on a conjecture of Erdős and {R}osenfeld. (1999) - [Br19] Bremner, A., On a problem of Erdős related to common factor differences. (2019)

Quoted from FormalConjectures/ErdosProblems/885.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/885.

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

Erdos885.erdos_885

Open: stated without proof.

Is it true that, for every \(k \geq 1\), there exist integers \(N_1 < \dots < N_k\) such that \(|\cap_i D(N_i)| \geq k\)?

theorem erdos_885 : ∀ k ≥ 1,
    ∃ Ns : Finset ℕ,
      (∀ n ∈ Ns, 1 ≤ n) ∧
      Ns.card = k ∧
      (⋂ n ∈ Ns, factorDifferenceSet n).ncard ≥ k

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

Erdos885.erdos_885.variants.k_eq_2

Proved here.

Erdős and Rosenfeld [ErRo97] proved this is true for \(k=2\).

theorem erdos_885.variants.k_eq_2 :
    ∃ Ns : Finset ℕ,
      (∀ n ∈ Ns, 1 ≤ n) ∧
      Ns.card = 2 ∧
      (⋂ n ∈ Ns, factorDifferenceSet n).ncard ≥ 2

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

Erdos885.erdos_885.variants.k_eq_3

Proved here.

Jiménez-Urroz [Ji99] proved this for \(k=3\).

theorem erdos_885.variants.k_eq_3 :
    ∃ Ns : Finset ℕ,
      (∀ n ∈ Ns, 1 ≤ n) ∧
      Ns.card = 3 ∧
      (⋂ n ∈ Ns, factorDifferenceSet n).ncard ≥ 3

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

Erdos885.erdos_885.variants.k_eq_4

Proved here.

Bremner [Br19] proved this for \(k=4\).

theorem erdos_885.variants.k_eq_4 :
    ∃ Ns : Finset ℕ,
      (∀ n ∈ Ns, 1 ≤ n) ∧
      Ns.card = 4 ∧
      (⋂ n ∈ Ns, factorDifferenceSet n).ncard ≥ 4

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

Sources
LeanErdos885.erdos_885 · Erdos885.erdos_885.variants.k_eq_2 · Erdos885.erdos_885.variants.k_eq_3 · Erdos885.erdos_885.variants.k_eq_4

TheoremErdős Problem 886#

References: - erdosproblems.com/886 - [ErRo97] Erdős, Paul and Rosenfeld, Moshe, The factor-difference set of integers. Acta Arith. (1997), 353--359.

Quoted from FormalConjectures/ErdosProblems/886.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/886.

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

Erdos886.erdos_886

Open: stated without proof.

Let \(\epsilon>0\). Is it true that, for all large \(n\), the number of divisors of \(n\) in \((n^{1/2},n^{1/2}+n^{1/2-\epsilon})\) is \(O_\epsilon(1)\)?

Erdős attributes this conjecture to Ruzsa.

theorem erdos_886 :
    ∀ ε > 0, ∃ K : ℕ, ∀ᶠ n in atTop, (Erdos886Divisors n ε 1).card ≤ K

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

Erdos886.erdos_886.variants.rosenfeld_infinite

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/4a1f92f2aca5f32edb0c681f1e8fdca88b5d9494/erdos-886/Solution.lean#L38.

Erdős and Rosenfeld [ErRo97] proved that there are infinitely many \(n\) such that there are four divisors of \(n\) in \((n^{1/2},n^{1/2}+16n^{1/4})\).

theorem erdos_886.variants.rosenfeld_infinite :
    Set.Infinite {n | 4 ≤ (Erdos886Divisors n (1/4) 16).card}

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

Erdos886.erdos_886.variants.rosenfeld_bound

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/4a1f92f2aca5f32edb0c681f1e8fdca88b5d9494/erdos-886/Solution.lean#L45.

Erdős and Rosenfeld [ErRo97] proved that, for any constant \(C>0\), all large \(n\) have at most \(1+C^2\) many divisors in \([n^{1/2}, n^{1/2}+Cn^{1/4}]\).

theorem erdos_886.variants.rosenfeld_bound :
    ∀ C > 0, ∀ᶠ (n : ℕ) in atTop,
    ((divisors n).filter (fun (d : ℕ) =>
      (n : ℝ) ^ (1 / 2 : ℝ) ≤ (d : ℝ) ∧ (d : ℝ) ≤ (n : ℝ) ^ (1 / 2 : ℝ) + C * (n : ℝ) ^ (1 / 4 : ℝ))).card
      ≤ 1 + C ^ 2

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

Sources
LeanErdos886.erdos_886 · Erdos886.erdos_886.variants.rosenfeld_infinite · Erdos886.erdos_886.variants.rosenfeld_bound

TheoremErdős Problem 887#

References: * erdosproblems.com/887 * [ErRo97] Erdős, Paul and Rosenfeld, Moshe, The factor-difference set of integers. Acta Arith. (1997), 353--359.

Quoted from FormalConjectures/ErdosProblems/887.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/887.

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

Erdos887.erdos_887.parts.i

Open: stated without proof.

Is there an absolute constant \(K\) such that, for every \(C > 0\), if \(n\) is sufficiently large then \(n\) has at most \(K\) divisors in \((n^{\frac{1}{2}}, n^{\frac{1}{2}} + C n^{\frac{1}{4}})\).

theorem erdos_887.parts.i : ∀ C > (0 : ℝ), ∀ᶠ n in atTop,
    #{ d ∈ Ioo ⌊√n⌋₊ ⌈√n + C * n^((1 : ℝ) / 4)⌉₊ | d ∣ n } ≤ erdos_887.parts.i.answer

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

Erdos887.erdos_887.parts.ii

Open: stated without proof.

Is there an absolute constant \(K\) such that, for every \(C > 0\), if \(n\) is sufficiently large then \(n\) has at most \(K\) divisors in \((n^{\frac{1}{2}}, n^{\frac{1}{2}} + C n^{\frac{1}{4}})\).

theorem erdos_887.parts.ii : ∃ K, ∀ C > (0 : ℝ), ∀ᶠ n in atTop,
    #{ d ∈ Ioo ⌊√n⌋₊ ⌈√n + C * n^((1 : ℝ) / 4)⌉₊ | d ∣ n } ≤ K

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

Erdos887.erdos_887.variants.rosenfeld_infinite

Solved: stated here without proof.

A question of Erdős and Rosenfeld, who proved that there are infinitely many \(n\) with (at least) \(4\) divisors in \((n^{\frac{1}{2}}, n^{\frac{1}{2}} + cn^{\frac{1}{4}})\).

theorem erdos_887.variants.rosenfeld_infinite : ∃ C > (0 : ℝ),
    Infinite {n : ℕ | 4 ≤ #{ d ∈ Ioo ⌊√n⌋₊ ⌈√n + C * n^((1 : ℝ) / 4)⌉₊ | d ∣ n }}

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

Erdos887.erdos_887.variants.rosenfeld_4

Solved: stated here; a Lean proof is at https://github.com/mnn31/erdos-lean/blob/5cb725981b3ad137103ef908eb6ecff9e7ed9bdf/ErdosLean/Erdos887.lean#L538.

Erdős and Rosenfeld ask whether \(4\) is the best possible \(K\) for the infinitude of \(n\) with (at least) \(K\) divisors in \((n^{\frac{1}{2}}, n^{\frac{1}{2}} + C n^{\frac{1}{4}})\), for some constant \(C > 0\). The constant cannot be taken to be \(1\). Distinct divisors \(d > \sqrt{n}\) give distinct integers \(d + n/d\), and a divisor in the interval has \(2\sqrt{n} < d + n/d < 2\sqrt{n} + C^2\), so for \(C = 1\) there is at most one such divisor.

The answer is no. In a forum post (July 2026), m-czech showed that for \(C = 31\) infinitely many \(n\) have \(5\) divisors in the interval. The construction is \(n = (x^2 - 1)(x^2 - 4)(x^2 - 16)(x^2 - 49)\) with \(z^2 = 56 x^2 + 65\).

theorem erdos_887.variants.rosenfeld_4 :
    ¬ IsGreatest {K | ∃ C > (0 : ℝ),
      Infinite {n : ℕ | K ≤ #{ d ∈ Ioo ⌊√n⌋₊ ⌈√n + C * n^((1 : ℝ) / 4)⌉₊ | d ∣ n }}} 4

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

Sources
LeanErdos887.erdos_887.parts.i · Erdos887.erdos_887.parts.ii · Erdos887.erdos_887.variants.rosenfeld_infinite · Erdos887.erdos_887.variants.rosenfeld_4

TheoremErdős Problem 888#

References: - erdosproblems.com/888 - [Er98] Erdős, Paul, Some of my new and almost new problems and results in combinatorial number theory. Number theory (Eger, 1996) (1998), 169-180.

Quoted from FormalConjectures/ErdosProblems/888.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/888.

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

Erdos888.erdos_888

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

What is the size of the largest \(A\subseteq \{1,\ldots,n\}\) such that if \(a\leq b\leq c\leq d\in A\) are such that \(abcd\) is a square then \(ad=bc\)?

This was proved by GPT-5.5 Pro (prompted by Chojecki).

theorem erdos_888 :
    (fun n : ℕ ↦ (Nat.findGreatest (p n) n : ℝ)) =Θ[atTop]
      (fun n : ℕ ↦ (n : ℝ) * Real.log (Real.log n) / Real.log n)

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

Erdos888.erdos_888.variants.sarkozy

Solved: stated here without proof.

Erdős claims that Sárközy proved that \(\lvert A\rvert =o(n)\) (a proof of this bound is provided by Tao in the comments).

theorem erdos_888.variants.sarkozy :
    (fun n ↦ (Nat.findGreatest (p n) n : ℝ)) =o[atTop] (Nat.cast : ℕ → ℝ)

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

Erdos888.erdos_888.variants.primes

Solved: stated here without proof.

The primes show that \(\lvert A\rvert \gg n/\log n\) is possible.

theorem erdos_888.variants.primes :
    (fun n : ℕ ↦ (Nat.findGreatest (p n) n : ℝ)) ≫ (fun n : ℕ ↦ (n : ℝ) / Real.log n)

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

Erdos888.erdos_888.variants.semiprimes

Solved: stated here without proof.

Cambie and Weisenberg have noted in the comments that the set of semiprimes also works, showing \((1+o(1))\frac{\log\log n}{\log n}n \leq \lvert A\rvert\) is achievable.

theorem erdos_888.variants.semiprimes :
    ∃ c : ℕ → ℝ, c =o[atTop] (1 : ℕ → ℝ) ∧ ∀ᶠ n : ℕ in atTop,
      (1 + c n) * ((n : ℝ) * Real.log (Real.log n) / Real.log n) ≤ Nat.findGreatest (p n) n

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

Sources
LeanErdos888.erdos_888 · Erdos888.erdos_888.variants.sarkozy · Erdos888.erdos_888.variants.primes · Erdos888.erdos_888.variants.semiprimes

TheoremErdős Problem 889#

Reference: erdosproblems.com/889

Quoted from FormalConjectures/ErdosProblems/889.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/889.

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

Erdos889.erdos_889

Open: stated without proof.

Let \(v(n,k)\) count the prime factors of \(n+k\) which do not divide \(n+i\) for \(0\leq i < k\). Is it true that \(v_0(n)=\max_{k\geq 0}v(n,k)\to \infty\) as \(n\to \infty\)?

theorem erdos_889 : Tendsto v₀ atTop (𝓝 ⊤)

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

Erdos889.erdos_889.variants.v0_gt_1

Solved: stated here without proof.

\(v_0(n) > 1\) for all \(n\) except \(n\) = 0, 1, 2, 3, 4, 7, 8, 16

[ErSe67] Erdős, P. and Selfridge, J. L., Some problems on the prime factors of consecutive integers. Illinois J. Math. (1967), 428--430.

theorem erdos_889.variants.v0_gt_1 :
    ∀ n : ℕ, n ∉ ({0, 1, 2, 3, 4, 7, 8, 16} : Finset ℕ) → 1 < v₀ n

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

Erdos889.erdos_889.variants.general

Open: stated without proof.

Let \(v_l(n) = \max_{k\geq l} v(n,k)\). For every fixed \(l\), \(v_l(n) \to \infty\) as \(n \to \infty\)

[ErSe67] Erdős, P. and Selfridge, J. L., Some problems on the prime factors of consecutive integers. Illinois J. Math. (1967), 428--430.

theorem erdos_889.variants.general :
    ∀ l, Tendsto (v_l l) atTop (𝓝 ⊤)

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

Erdos889.erdos_889.variants.v1_eq_1_finite

Open: stated without proof.

Does \(v_1(n) = 1\) have finite solutions?

[ErSe67] Erdős, P. and Selfridge, J. L., Some problems on the prime factors of consecutive integers. Illinois J. Math. (1967), 428--430.

theorem erdos_889.variants.v1_eq_1_finite :
    {n | v_l 1 n = 1}.Finite

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

Erdos889.erdos_889.variants.V1_eq_1_finite

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-889-capital-v1-finite/blob/44d38dd7f618dbaa0b08fb976c0378b4897021cd/lean/Erdos889V1FiniteFC.lean#L999-L1004.

Does \(V_1(n) = 1\) have finite solutions?

This is a modification of erdos_889.variants.v1_eq_1_finite, which might make it more amenable to attack according to [ErSe67].

Kenta Kitamura (KitaKen1 on GitHub) has given a Lean proof (erdos-889-capital-v1-finite) that there are only finitely many \(n\) with \(V_1(n) = 1\).

[ErSe67] Erdős, P. and Selfridge, J. L., Some problems on the prime factors of consecutive integers. Illinois J. Math. (1967), 428--430.

theorem erdos_889.variants.V1_eq_1_finite :
    {n | V_l 1 n = 1}.Finite

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

Sources
LeanErdos889.erdos_889 · Erdos889.erdos_889.variants.v0_gt_1 · Erdos889.erdos_889.variants.general · Erdos889.erdos_889.variants.v1_eq_1_finite · Erdos889.erdos_889.variants.V1_eq_1_finite

TheoremErdős Problem 890#

Reference: - erdosproblems.com/890 - [ErSe67] Erdős, P. and Selfridge, J. L., Some problems on the prime factors of consecutive integers. Illinois J. Math. (1967), 428--430.

Quoted from FormalConjectures/ErdosProblems/890.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/890.

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

Erdos890.erdos_890.parts.a

Open: stated without proof.

If \(\omega_k(n)\) counts the number of distinct prime factors of \(n\) which are \(>k\), then is it true that, for every \(k\geq 1\),

\[\liminf_{n\to \infty}\sum_{0\leq i < k}\omega_k(n+i)\leq k?\]
theorem erdos_890.parts.a :
    ∀ k ≥ 1, liminf (fun n ↦ (∑ i ∈ range k, (ω_gt k (n + i) : EReal))) atTop ≤ k

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

Erdos890.erdos_890.parts.b

Open: stated without proof.

Is it true that

\[\limsup_{n\to \infty}\left(\sum_{0\leq i < k}\omega(n+i)\right) \frac{\log\log n}{\log n}=1,\]

where \(\omega\) counts the number of distinct prime factors without restriction?

theorem erdos_890.parts.b :
    ∀ k ≥ 1, limsup (fun n ↦ (∑ i ∈ range k, (ω (n + i) : EReal)) *
      (log (log n) / log n)) atTop = 1

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

Erdos890.erdos_890.variants.liminf_lower_bound

Solved: stated here without proof.

A question of Erdős and Selfridge [ErSe67], who observe that \(\liminf_{n\to \infty}\sum_{0\leq i < k}\omega(n+i)\geq k+\pi(k)-1\) for every \(k\). This follows from Pólya's theorem that the set of \(k\)-smooth integers has unbounded gaps - indeed, \(n(n+1)\cdots (n+k-1)\) is divisible by all primes \(\leq k\) and, provided \(n\) is large, all but at most one of \(n,n+1,\ldots,n+k-1\) has a prime factor \(>k\) by Pólya's theorem.

theorem erdos_890.variants.liminf_lower_bound (k : ℕ) :
    liminf (fun n ↦ (∑ i ∈ range k, (ω (n + i) : EReal))) atTop ≥ k + π k - 1

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

Erdos890.erdos_890.variants.omega_limsup

Solved: stated here without proof.

It is a classical fact that \(\limsup_{n\to \infty}\omega(n)\frac{\log\log n}{\log n}=1.\)

theorem erdos_890.variants.omega_limsup :
    limsup (fun n ↦ (ω n : EReal) * (log (log n) / log n)) atTop = 1

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

Sources
LeanErdos890.erdos_890.parts.a · Erdos890.erdos_890.parts.b · Erdos890.erdos_890.variants.liminf_lower_bound · Erdos890.erdos_890.variants.omega_limsup

TheoremErdős Problem 891#

References: - erdosproblems.com/891 - [Po18] Pólya, Georg, Zur arithmetischen {U}ntersuchung der {P}olynome. Math. Z. (1918), 143--148. - [Wikipedia] https://en.wikipedia.org/wiki/Dickson%27s_conjecture

Quoted from FormalConjectures/ErdosProblems/891.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/891.

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

Erdos891.erdos_891

Open: stated without proof.

Let \(2=p_1 < p_2 < \cdots\) be the primes and \(k\geq 2\). Is it true that, for all sufficiently large \(n\), there must exist an integer in \([n,n+p_1\cdots p_k)\) with \(>k\) many prime factors?

theorem erdos_891 :
    ∀ k ≥ 2, ∀ᶠ n in atTop,
    ∃ m ∈ Ico n (n + ∏ i ∈ range k, i.nth Nat.Prime), k < ω m

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

Erdos891.erdos_891.variants.schinzel

Solved: stated here without proof.

Schinzel deduced from Pólya's theorem [Po18] (that the sequence of \(k\)-smooth integers has unbounded gaps) that this is true with \(p_1\cdots p_k\) replaced by \(p_1\cdots p_{k-1}p_{k+1}\).

theorem erdos_891.variants.schinzel :
    ∀ k ≥ 2, ∀ᶠ n in atTop,
      ∃ m ∈ Ico n (n + (∏ i ∈ range (k - 1), i.nth Nat.Prime) * k.nth Nat.Prime),
      k < ω m

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

Erdos891.erdos_891.variants.case_k_2

Open: stated without proof.

This is unknown even for \(k=2\) - that is, is it true that in every interval of \(6\) (sufficiently large) consecutive integers there must exist one with at least \(3\) prime factors?

theorem erdos_891.variants.case_k_2 :
    ∀ᶠ n in atTop,
      ∃ m ∈ Ico n (n + 6), 3 ≤ ω m

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

Erdos891.erdos_891.variants.weisenberg

Solved: stated here without proof.

Weisenberg has observed that Dickson's conjecture implies the answer is no if we replace \(p_1\cdots p_k\) with \(p_1\cdots p_k-1\). Indeed, let \(L_k\) be the lowest common multiple of all integers at most \(p_1\cdots p_k\). By Dickson's conjecture [Wikipedia], there are infinitely many \(n'\) such that \(\frac{L_k}{m}n'+1\) is prime for all \(1\leq m < p_1\cdots p_k\). It follows that, if \(n=L_kn'+1\), then all integers in \([n,n+p_1\cdots p_k-1)\) have at most \(k\) prime factors.

The statement is conditional on Dickson's conjecture, formalised as Dickson.dickson_conjecture.

theorem erdos_891.variants.weisenberg (k : ℕ) (hk : k ≥ 2)
    (hdickson : type_of% Dickson.dickson_conjecture) :
    ∃ᶠ n in atTop,
      ∀ m ∈ Ico n (n + (∏ i ∈ range k, i.nth Nat.Prime) - 1),
      ω m ≤ k

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

Sources
LeanErdos891.erdos_891 · Erdos891.erdos_891.variants.schinzel · Erdos891.erdos_891.variants.case_k_2 · Erdos891.erdos_891.variants.weisenberg

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.