Erdős Problem 845 to Erdős Problem 867

TheoremErdős Problem 845#

Reference: erdosproblems.com/845

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

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

Erdos845.erdos_845

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

Let \(C > 0\). Is it true that the set of integers of the form \(n = b_1 + \cdots + b_t\), with \(b_1 < \cdots < b_t\), where \(b_i = 2^{k_i}3^{l_i}\) for \(1 \leq i\leq t\) and \(b_t \leq Cb_1\) has density \(0\)?

van Doorn and Everts \cite{vDEv25} have disproved this with \(C=6\) - in fact, they prove that all integers can be written as such a sum in which \(b_t<6b_1\).

This was formalized in Lean by Alexeev using Aristotle.

theorem erdos_845 :
    ¬ ∀ᵉ (C : ℝ) (hC : 0 < C),
      let f : ℕ × ℕ → ℕ := fun (k, l) ↦ 2 ^ k * 3 ^ l
      { ∑ x ∈ B, f x | (B : Finset (ℕ × ℕ)) (h : B.Nonempty)
        (hB : B.sup f ≤ C * B.inf' h f) }.HasDensity 0

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

Sources
LeanErdos845.erdos_845

TheoremErdős Problem 846#

Reference: erdosproblems.com/846

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

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

Erdos846.erdos_846

Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/2404258180688283e5141021c75464dc2acfb798/FormalConjectures/ErdosProblems/846.lean.

Erdős Problem 846 Let A ⊂ ℝ² be an infinite set for which there exists some ϵ>0 such that in any subset of A of size n there are always at least ϵn with no three on a line. Is it true that A is the union of a finite number of sets where no three are on a line?

In other words, prove or disprove the following statement: every infinite ε-non-trilinear subset of the plane is weakly non-trilinar.

theorem erdos_846 : ¬ ∀ᵉ (A : Set ℝ²) (ε > 0), A.Infinite → NonTrilinearFor A ε →
    WeaklyNonTrilinear A

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

Sources
LeanErdos846.erdos_846

TheoremErdős Problem 847#

References: - erdosproblems.com/847 - [RRS24] Reiher, Christian and R\"odl, Vojt\v ech and Sales, Marcelo, Colouring versus density in integers and {H}ales-{J}ewett cubes. J. Lond. Math. Soc. (2) (2024) arXiv:2311.08556

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

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

Erdos847.erdos_847

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

Let \(A \subset \mathbb{N}\) be an infinite set for which there exists some \(\epsilon > 0\) such that in any subset of \(A\) of size \(n\) there is a subset of size at least \(\epsilon n\) which contains no three-term arithmetic progression.

Is it true that \(A\) is the union of a finite number of sets which contain no three-term arithmetic progression?

A negative answer was given by Reiher, Rödl, and Sales [RRS24], who proved that, for any \(0\lt \mu<1/2\), there exists \(A\subseteq \mathbb{N}\) such that every finite colouring of \(A\) contains a three-term arithmetic progression, and yet every subset of \(A\) of size \(n\) contains a subset of size \(\geq \mu n\) without a three-term arithmetic progression.

theorem erdos_847 : ¬ ∀ (A : Set ℕ), Infinite A → HasFew3APs A →
    ∃ n, ∃ (S : Fin n → Set ℕ), (∀ i, ThreeAPFree (S i)) ∧ A = ⋃ i : Fin n, S i

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

Sources
LeanErdos847.erdos_847

TheoremErdős Problem 848#

Is the maximum size of a set \(A \subseteq \{1, \dots, N\}\) such that \(ab + 1\) is never squarefree (for all \(a, b \in A\)) achieved by taking those \(n \equiv 7 \pmod{25}\)?

References: - erdosproblems.com/848 - [Er92b] Erdős, P. "Some of my favourite problems in number theory, combinatorics, and geometry." Resenhas do Instituto de Matemático e Estatística da Universidade de São Paulo 2.2 (1995): 165-186. - [Sa25] Sawhney, M. "Problem 848." (2025) https://www.math.columbia.edu/~msawhney/Problem_848.pdf - Full formal proof of asymptotic result: https://github.com/The-Obstacle-Is-The-Way/erdos-banger

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

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

Erdos848.erdos_848

Solved: stated here without proof.

Is the maximum size of a set \(A ⊆ \{1, \dots, N\}\) such that \(ab + 1\) is never squarefree (for all \(a, b ∈ A\)) achieved by taking those \(n ≡ 7 \pmod{25}\)?

This asks whether Erdos848 N holds for all \(N\) (formulated using A ⊆ Finset.range N).

This was solved for all sufficiently large \(N\) by Sawhney in this note. In fact, Sawhney proves something slightly stronger, that there exists some constant \(c>0\) such that if \(\lvert A\rvert \geq (\frac{1}{25}-c)N\) and \(N\) is large then \(A\) is contained in either \(\{ n\equiv 7\pmod{25}\}\) or \(\{n\equiv 18\pmod{25}\}\).

theorem erdos_848 : ∀ N, Erdos848For N

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

Erdos848.erdos_848.variants.asymptotic

Solved: stated here; a Lean proof is at https://github.com/The-Obstacle-Is-The-Way/erdos-banger/blob/1cc2ac8e9d70516e979733c6ea5c4d2eb652d1f5/formal/lean/Erdos/848.lean.

There exists \(N₀\) such that for all \(N ≥ N₀\), if \(A ⊆ \{1, \dots, N\}\) satisfies that \(ab + 1\) is never squarefree for all \(a, b ∈ A\), then \(|A| ≤ |\{n ≤ N : n ≡ 7 \pmod{25}\}|\).

More precisely, Sawhney proves: there exist absolute constants \(η > 0\) and \(N₀\) such that for all \(N ≥ N₀\), if \(|A| ≥ (1/25 - η)N\) then \(A ⊆ \{n : n ≡ 7 \pmod{25}\}\) or \(A ⊆ \{n : n ≡ 18 \pmod{25}\}\).

A complete formal Lean 4 proof is available at: https://github.com/The-Obstacle-Is-The-Way/erdos-banger

theorem erdos_848.variants.asymptotic : ∀ᶠ N in Filter.atTop, Erdos848For N

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

Sources
LeanErdos848.erdos_848 · Erdos848.erdos_848.variants.asymptotic

TheoremErdős Problem 849#

Reference: erdosproblems.com/849

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

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

Erdos849.erdos_849

Open: stated without proof.

Is it true that, for every integer \(t\geq1\), there is some integer \(a\) such that \({n \choose k} = a\) with \(1\leq k \le \frac{n}{2}\) has exactly \(t\) solutions?

theorem erdos_849 :
    ∀ t ≥ 1, ∃ a : ℕ,
      {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a}.ncard = t

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

Sources
LeanErdos849.erdos_849

TheoremErdős Problem 850#

Reference: erdosproblems.com/850

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

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

Erdos850.erdos_850

Open: stated without proof.

Can there exist two distinct integers \(x\) and \(y\) such that \(x,y\) have the same prime factors, \(x+1,y+1\) have the same prime factors, and \(x+2,y+2\) also have the same prime factors?

theorem erdos_850 :
    ∃ x y : ℕ, x ≠ y ∧ x.primeFactors = y.primeFactors
      ∧ (x + 1).primeFactors = (y + 1).primeFactors
      ∧ (x + 2).primeFactors = (y + 2).primeFactors

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

Sources
LeanErdos850.erdos_850

TheoremErdős Problem 851#

References: - erdosproblems.com/851 - [Pr26] D. Price and GPT-5.2 Pro, Erdős problem 851 (2026)

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

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

Erdos851.erdos_851.variants.romanoff

Solved: stated here without proof.

The set of integers of the form 2^k+p (where p is prime) has positive lower density.

theorem erdos_851.variants.romanoff : 0 < Set.lowerDensity twoPowAddPrimeSet

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

Erdos851.erdos_851

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

Let \(\epsilon > 0\). Is there some \(r \ll_\epsilon 1\) such that the density of integers of the form \(2^k+n\), where \(k \geq 0\) and \(n\) has at most \(r\) prime divisors, is at least \(1-\epsilon\)?

This was proved affirmatively by Price and GPT-5.2 Pro [Pr26].

theorem erdos_851 (ε : ℝ) (hε : ε ∈ Set.Ioo 0 1) : ∃ r,
    1 - ε ≤ (TwoPowAddSet r).lowerDensity

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

Sources
LeanErdos851.erdos_851.variants.romanoff · Erdos851.erdos_851

TheoremErdős Problem 852#

References: - erdosproblems.com/852 - [Er85c] Erdős, P., On some of my problems in number theory I would most like to see solved. Number theory (Ootacamund, 1984) (1985), 74-84. - A001223 - A053597 - A078515

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

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

Erdos852.erdos_852.parts.i

Open: stated without proof.

Let \(d_n = p_{n+1} - p_n\), where \(p_n\) is the \(n\)th prime. Let \(h(x)\) be maximal such that for some \(n < x\) the numbers \(d_n, d_{n+1}, \ldots, d_{n+h(x)-1}\) are all distinct [Er85c]. Estimate \(h(x)\). In particular, is it true that

\[h(x) > (\log x)^c\]

for some constant \(c > 0\)?

The statement avoids defining \(h\). Since \(h(x)\) is the longest such run, \(h(x) > y\) holds exactly when some \(n < x\) starts a run of \(H > y\) distinct gaps. We state the question this way, with \(x\) real. We read it as asking for one \(c > 0\) such that the inequality holds for all large \(x\).

The primes are indexed from \(p_0 = 2\), as in primeGap. Shifting the index by one does not change the question.

theorem erdos_852.parts.i :
    ∃ c : ℝ, 0 < c ∧ ∀ᶠ x : ℝ in atTop,
      ∃ n : ℕ, (n : ℝ) < x ∧ ∃ H : ℕ, (Real.log x) ^ c < (H : ℝ) ∧ DistinctGapRun n H

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

Erdos852.erdos_852.parts.ii

Open: stated without proof.

Let \(d_n = p_{n+1} - p_n\), where \(p_n\) is the \(n\)th prime. Let \(h(x)\) be maximal such that for some \(n < x\) the numbers \(d_n, d_{n+1}, \ldots, d_{n+h(x)-1}\) are all distinct [Er85c]. Estimate \(h(x)\). In particular, is it true that

\[h(x) = o(\log x)?\]

The statement avoids defining \(h\). It says that for every \(\varepsilon > 0\) and all large real \(x\), every run of \(H\) distinct gaps \(d_n, \ldots, d_{n+H-1}\) with \(n < x\) satisfies \(H \leq \varepsilon \log x\). This is \(h(x) \leq \varepsilon \log x\), because \(h(x)\) is the longest such run.

The indexing is as in Erdos852.erdos_852.parts.i.

theorem erdos_852.parts.ii :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℝ in atTop,
      ∀ n : ℕ, (n : ℝ) < x → ∀ H : ℕ, DistinctGapRun n H → (H : ℝ) ≤ ε * Real.log x

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

Erdos852.erdos_852.variants.tendsto_atTop

Solved: stated here without proof.

Brun's sieve implies \(h(x) \to \infty\) as \(x \to \infty\) (remark on erdosproblems.com/852).

That is, for every \(H\) and all large \(x\) there is some \(n < x\) such that \(d_n, \ldots, d_{n+H-1}\) are all distinct. Since more values of \(n\) are allowed as \(x\) grows, this holds exactly when, for every \(H\), some \(n\) has \(d_n, \ldots, d_{n+H-1}\) all distinct.

This also follows from Erdos6.erdos_6.variants.increasing, because strictly increasing prime gaps are distinct.

theorem erdos_852.variants.tendsto_atTop :
    ∀ H : ℕ, ∀ᶠ x : ℝ in atTop, ∃ n : ℕ, (n : ℝ) < x ∧ DistinctGapRun n H

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

Sources
LeanErdos852.erdos_852.parts.i · Erdos852.erdos_852.parts.ii · Erdos852.erdos_852.variants.tendsto_atTop

TheoremErdős Problem 853#

Reference: erdosproblems.com/853

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

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

Erdos853.erdos_853.parts.i

Open: stated without proof.

Let \(d_n = p_{n+1} - p_n\), where \(p_n\) is the \(n\)th prime. Let \(r(x)\) be the smallest even integer \(t\) such that \(d_n = t\) has no solutions for \(n \le x\).

Is it true that \(r(x) \to \infty\)?

theorem erdos_853.parts.i : atTop.Tendsto r atTop

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

Erdos853.erdos_853.parts.ii

Open: stated without proof.

Let \(d_n = p_{n+1} - p_n\), where \(p_n\) is the \(n\)th prime. Let \(r(x)\) be the smallest even integer \(t\) such that \(d_n = t\) has no solutions for \(n \le x\).

Is it true that \(r(x) / \log x \to \infty\)?

theorem erdos_853.parts.ii :
    atTop.Tendsto (fun n ↦ r n / Real.log n) atTop

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

Sources
LeanErdos853.erdos_853.parts.i · Erdos853.erdos_853.parts.ii

TheoremErdős Problem 854#

References: - erdosproblems.com/854 - [Er85c] Erdős, P., On some of my problems in number theory I would most like to see solved. Number theory (Ootacamund, 1984), Lecture Notes in Math. 1122 (1985), 74-84. PDF - [Ob1] Erdős, P., Oberwolfach Mathematical Problems, Volume 1. Mathematisches Forschungsinstitut Oberwolfach. - OEIS A389839: smallest even number which cannot be written as the difference of two consecutive numbers which are relatively prime to the \(n\)th primorial. It agrees with minEvenNonGap k for \(k\geq 3\). - OEIS A048670: Jacobsthal's function of the product of the first \(n\) primes, which is the largest gap.

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

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

Erdos854.erdos_854.parts.i

Open: stated without proof.

Let \(n_k\) denote the \(k\)th primorial, i.e. the product of the first \(k\) primes.

If \(1=a_1\lt a_2\lt \cdots \lt a_{\phi(n_k)}=n_k-1\) is the sequence of integers coprime to \(n_k\), then estimate the smallest even integer not of the form \(a_{i+1}-a_i\). Are there

\[\gg \max_i (a_{i+1}-a_i)\]

many even integers of the form \(a_{j+1}-a_j\)?

This is the first part. A problem of Erdős [Er85c, p. 80], who writes "integer" instead of "even integer"; all differences \(a_{i+1}-a_i\) are even, so only even integers are meaningful. Here "estimate" is read as \(\Theta\). Erdős first thought that for large \(k\) every even \(t \leq \max_i(a_{i+1}-a_i)\) is a gap, but [Ob1] reports computations of Lacampagne and Selfridge showing this fails for \(n_6 = 30030\) (OEIS A389839 and A048670 give \(20\) and \(22\)).

theorem erdos_854.parts.i :
    (fun k ↦ (minEvenNonGap k : ℝ)) =Θ[atTop] erdos_854.parts.i.answer

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

Erdos854.erdos_854.parts.ii

Open: stated without proof.

Let \(n_k\) denote the \(k\)th primorial, i.e. the product of the first \(k\) primes.

If \(1=a_1\lt a_2\lt \cdots \lt a_{\phi(n_k)}=n_k-1\) is the sequence of integers coprime to \(n_k\), then estimate the smallest even integer not of the form \(a_{i+1}-a_i\). Are there

\[\gg \max_i (a_{i+1}-a_i)\]

many even integers of the form \(a_{j+1}-a_j\)?

This is the second part. We read it as: there is an absolute constant \(c > 0\) such that, for all large \(k\), the number of distinct gap values is at least \(c\) times the largest gap.

theorem erdos_854.parts.ii :
    ∃ c > (0 : ℝ), ∀ᶠ k : ℕ in atTop,
      c * (maxGap (kthPrimorial k) : ℝ) ≤ ((gapSet (kthPrimorial k)).card : ℝ)

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

Sources
LeanErdos854.erdos_854.parts.i · Erdos854.erdos_854.parts.ii

TheoremErdős Problem 855#

Reference: erdosproblems.com/855

This is an "eventually" formulation of the Second Hardy–Littlewood conjecture.

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

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

Erdos855.erdos_855

Open: stated without proof.

Erdős Problem 855 (Segal's conjecture): \(\pi(x + y) \le \pi(x) + \pi(y)\) for all sufficiently large \(x, y\), i.e. for all \(x, y \ge N\) for some \(N\).

theorem erdos_855 :
    ∀ᶠ (xy : ℕ × ℕ) in atTop ×ˢ atTop, π (xy.1 + xy.2) ≤ π xy.1 + π xy.2

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

Sources
LeanErdos855.erdos_855

TheoremErdős Problem 856#

References: - erdosproblems.com/856 - [Er70] Erdős, P., Some extremal problems in combinatorial number theory. Mathematical Essays Dedicated to A. J. Macintyre (1970), 123-133. PDF - [TaZh25b] Tang, Q. and Zhang, S., Harmonic LCM patterns and sunflower-free capacity. arXiv:2512.20055 (2025).

The problem is closely related to the sunflower problem erdosproblems.com/857. The version with natural density in place of the harmonic sum is erdosproblems.com/536.

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

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

Erdos856.erdos_856

Open: stated without proof.

Let \(k\geq 3\) and \(f_k(N)\) be the maximum value of \(\sum_{n\in A}\frac{1}{n}\), where \(A\) ranges over all subsets of \(\{1,\ldots,N\}\) which contain no subset of size \(k\) with the same pairwise least common multiple.

Estimate \(f_k(N)\).

This is the question of Erdős [Er70, p. 127]. We read "estimate" as \(f_k(N) = \Theta(\text{answer})\) as \(N \to \infty\), for each fixed \(k\).

theorem erdos_856 (k : ℕ) (hk : 3 ≤ k) :
    f k =Θ[atTop] erdos_856.answer k

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

Erdos856.erdos_856.variants.erdos_upper

Solved: stated here without proof.

Erdős [Er70, p. 127] notes that

\[f_k(N) \ll \frac{\log N}{\log\log N}.\]

The implied constant depends on \(k\).

theorem erdos_856.variants.erdos_upper (k : ℕ) (hk : 3 ≤ k) :
    ∃ C > (0 : ℝ), ∀ᶠ N : ℕ in atTop, f k N ≤ C * (Real.log N / Real.log (Real.log N))

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

Erdos856.erdos_856.variants.tang_zhang_lower

Solved: stated here without proof.

Tang and Zhang [TaZh25b, Theorem 1.2] proved that, for fixed \(k\geq 3\) and as \(N\to\infty\),

\[f_k(N) \geq (\log N)^{c_k - o(1)}, \qquad c_k = \frac{k-2}{e\,((k-2)!)^{1/(k-2)}}.\]

The \(o(1)\) is stated with an arbitrary \(\varepsilon > 0\).

theorem erdos_856.variants.tang_zhang_lower (k : ℕ) (hk : 3 ≤ k) (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop, Real.log N ^ (tangZhangExponent k - ε) ≤ f k N

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

Erdos856.erdos_856.variants.tang_zhang_three_lower

Solved: stated here without proof.

Tang and Zhang [TaZh25b, Corollary 1.7] proved, as \(N\to\infty\),

\[(\log N)^{\log(1.551)-o(1)}\leq f_3(N)\ll(\log N)^{\frac{3}{2^{2/3}}-1+o(1)}.\]

This is the lower bound, with the \(o(1)\) stated with an arbitrary \(\varepsilon > 0\). Since \(\log(1.551) = 0.4389\ldots\), it implies the site's \((\log N)^{0.438}\leq f_3(N)\) for large \(N\).

theorem erdos_856.variants.tang_zhang_three_lower (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop, Real.log N ^ (Real.log 1.551 - ε) ≤ f 3 N

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

Erdos856.erdos_856.variants.tang_zhang_three_upper

Solved: stated here without proof.

Tang and Zhang [TaZh25b, Corollary 1.7] proved, as \(N\to\infty\),

\[(\log N)^{\log(1.551)-o(1)}\leq f_3(N)\ll(\log N)^{\frac{3}{2^{2/3}}-1+o(1)}.\]

This is the upper bound, with the \(o(1)\) and the implied constant absorbed into an arbitrary \(\varepsilon > 0\). The site rounds the exponent to \(0.889\), but \(\frac{3}{2^{2/3}}-1=0.8898\ldots\).

theorem erdos_856.variants.tang_zhang_three_upper (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop, f 3 N ≤ Real.log N ^ (3 / (2 : ℝ) ^ ((2 : ℝ) / 3) - 1 + ε)

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

Sources
LeanErdos856.erdos_856 · Erdos856.erdos_856.variants.erdos_upper · Erdos856.erdos_856.variants.tang_zhang_lower · Erdos856.erdos_856.variants.tang_zhang_three_lower · Erdos856.erdos_856.variants.tang_zhang_three_upper

TheoremErdős Problem 857#

Reference: erdosproblems.com/857

For fixed n, k, let m(n, k) be minimal such that every family of subsets of [n] of size at least m(n, k) contains a k-sunflower. The problem asks to estimate m(n, k), ideally asymptotically.

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

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

Erdos857.erdos_857

Open: stated without proof.

Estimate m(n,k), or better give an asymptotic formula.

theorem erdos_857 :
    ∀ k : ℕ, 3 ≤ k → Tendsto (fun n : ℕ => (m n k : ℝ) / erdos_857.answer k n) atTop (nhds 1)

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

Sources
LeanErdos857.erdos_857

TheoremErdős Problem 858#

References: - erdosproblems.com/858 - [Er70] Erdős, Paul, Some extremal problems in combinatorial number theory. Mathematical Essays Dedicated to A. J. Macintyre (1970), 123-133. - [Al66] Alexander, Ralph, Density and multiplicative structure of sets of integers. Acta Arith. (1966/67), 321--332. - [ESS68] Erdős, P. and Sárközi, A. and Szemerédi, E., On the solvability of certain equations in sequences of positive upper logarithmic density. J. London Math. Soc. (1968), 71--78. - [Be35] Behrend, F., On sequences of numbers not divisible by another. London Math. Soc. Journal (1935), 42-45.

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

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

Erdos858.erdos_858

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

Let \(A\subseteq \{1,\ldots,N\}\) be such that there is no solution to \(at=b\) with \(a,b\in A\) and the smallest prime factor of \(t\) is \(>a\). Estimate the maximum of

\[\frac{1}{\log N}\sum_{n\in A}\frac{1}{n}.\]

This has been solved by Chojecki and GPT-5.4 Pro, who show that for large \(N\)

\[\max_A \sum_{n\in A}\frac{1}{n}=(c+o(1))\log N\]

where the maximum is over all \(A\subseteq \{1,\ldots,N\}\) with the stated property and \(c\approx 0.618\cdots\) is an explicit constant.

theorem erdos_858 : ∃ c : ℝ, Tendsto (fun N : ℕ ↦ M N / log N) atTop (nhds c)

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

Erdos858.erdos_858.variants.positive

Solved: stated here without proof.

The limit \(c\approx 0.618\cdots\) is positive: for any fixed large \(N\) the maximum is bounded away from \(0\) (Alexander [Al66], Erdős–Sárközi–Szemerédi [ESS68]).

theorem erdos_858.variants.positive :
    ∃ c : ℝ, 0 < c ∧ Tendsto (fun N : ℕ ↦ M N / log N) atTop (nhds c)

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

Erdos858.erdos_858.variants.infinite

Solved: stated here without proof.

Alexander [Al66] and Erdős, Sárközi, and Szemerédi [ESS68] proved that if \(A\) is an infinite set with this property then \(\sum_{n\in A\cap [1,N]}\frac{1}{n}=o(\log N)\).

theorem erdos_858.variants.infinite (A : Set ℕ) (hA : A.Infinite) (h0 : 0 ∉ A)
    (hadm : ∀ a ∈ A, ∀ b ∈ A, ∀ t : ℕ, a * t = b → t.minFac ≤ a) :
    (fun N : ℕ ↦ ∑ n ∈ (Finset.Icc 1 N).filter (· ∈ A), (1 : ℝ) / n) =o[atTop]
      fun N : ℕ ↦ log N

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

Sources
LeanErdos858.erdos_858 · Erdos858.erdos_858.variants.positive · Erdos858.erdos_858.variants.infinite

TheoremErdős Problem 859#

Reference: erdosproblems.com/859

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

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

Erdos859.erdos_859.variants.erdos_upper_lower_bounds

Solved: stated here without proof.

A weaker version of the problem proved by Erdos: The density dₜ of DivisorSumSet (t : ℕ) is bounded from below by 1 / log (t) ^ c₃ and from above by 1 / log (t) ^ c₄ for some positive constants c₃ and c₄.

theorem erdos_859.variants.erdos_upper_lower_bounds : ∃ᵉ (c₃ > (0 : ℝ)) (c₄ > (0 : ℝ)) (t₀ : ℕ),
    ∀ᶠ t in atTop, ∃ dₜ : ℝ, (DivisorSumSet t).HasDensity dₜ ∧
    1 / Real.log t ^ c₃ < dₜ ∧ dₜ < 1 / Real.log t ^ c₄

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

Erdos859.erdos_859

Open: stated without proof.

The density of the divisor sum set is asymptotically equivalent to \(c_1 / \log(t)^{c_2}\).

theorem erdos_859 :
    ∃ c₁ > 0, ∃ c₂ > (0 : ℝ), ∃ d : ℕ → ℝ, (∀ t > 0, (DivisorSumSet t).HasDensity (d t)) ∧
      (fun (t : ℕ) ↦ d t) ~[atTop] (fun t ↦ c₁ / Real.log t ^ c₂)

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

Erdos859.erdos_859.variants.trivial_case

Textbook result, proved here.

A case where we can easily calculate the density of DivisorSumSet t is that of t=0.

lemma erdos_859.variants.trivial_case : DivisorSumSet 0 = Set.univ

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

Erdos859.erdos_859.variants.positive_density

Textbook result, stated without proof.

An easy sanity check is to prove that for every natural number t the density dₜ is a positive number. Hint: investigate some multiplicative structure of DivisorSumSet t.

lemma erdos_859.variants.positive_density (t : ℕ) :
    (DivisorSumSet t).HasPosDensity

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

Sources
LeanErdos859.erdos_859.variants.erdos_upper_lower_bounds · Erdos859.erdos_859 · Erdos859.erdos_859.variants.trivial_case · Erdos859.erdos_859.variants.positive_density

TheoremErdős Problem 860#

References: - erdosproblems.com/860 - [ErPo80] Erdős, P. and Pomerance, C., Matching the natural numbers up to \(n\) with distinct multiples in another interval. Nederl. Akad. Wetensch. Indag. Math. 42 (1980), 147-161. PDF - [Er92c] Erdős, P., Some of my forgotten problems in number theory. Hardy-Ramanujan J. 15 (1992), 34-50. PDF

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

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

Erdos860.erdos_860

Open: stated without proof.

Let \(h(n)\) be such that, for any \(m\geq 1\), in the interval \((m,m+h(n))\) there exist distinct integers \(a_i\) for \(1\leq i\leq \pi(n)\) such that \(p_i\mid a_i\), where \(p_i\) denotes the \(i\)th prime.

Estimate \(h(n)\).

theorem erdos_860 : (fun n ↦ (h n : ℝ)) =Θ[atTop] erdos_860.answer

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

Erdos860.erdos_860.variants.erdos_pomerance_upper

Solved: stated here without proof.

Erdős and Pomerance [ErPo80] proved that

\[h(n) \ll \frac{n^{3/2}}{(\log n)^{1/2}}.\]
theorem erdos_860.variants.erdos_pomerance_upper :
    (fun n : ℕ ↦ (h n : ℝ)) =O[atTop]
      fun n : ℕ ↦ (n : ℝ) ^ (3 / 2 : ℝ) / Real.sqrt (Real.log n)

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

Erdos860.erdos_860.variants.erdos_selfridge_lower

Solved: stated here without proof.

Erdős and Selfridge proved \(h(n)>(3-o(1))n\).

[ErPo80, (19), p. 159] states this as \(\limsup h(n)/n \geq 3\), that is, it holds for infinitely many \(n\). We state that form.

theorem erdos_860.variants.erdos_selfridge_lower :
    ∀ ε > (0 : ℝ), ∃ᶠ n : ℕ in atTop, (3 - ε) * n ≤ (h n : ℝ)

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

Erdos860.erdos_860.variants.ruzsa

Solved: stated here without proof.

Ruzsa proved \(h(n)/n\to \infty\), as reported in [Er92c, p. 36].

theorem erdos_860.variants.ruzsa :
    Tendsto (fun n : ℕ ↦ (h n : ℝ) / n) atTop atTop

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

Sources
LeanErdos860.erdos_860 · Erdos860.erdos_860.variants.erdos_pomerance_upper · Erdos860.erdos_860.variants.erdos_selfridge_lower · Erdos860.erdos_860.variants.ruzsa

TheoremErdős Problem 862#

References: - erdosproblems.com/862 - [Er92c] Erdős, P., Some of my forgotten problems in number theory. Hardy-Ramanujan J. (1992), 34-50. - [SaTh15] Saxton, David and Thomason, Andrew, Hypergraph containers. Invent. Math. (2015), 925-992.

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

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

Erdos862.erdos_862.parts.i

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

Let \(A_1(N)\) be the number of maximal Sidon subsets of \(\{1,\ldots,N\}\). Is it true that

\[A_1(N) < 2^{o(N^{1/2})}?\]

A problem of Cameron and Erdős. This is resolved as a consequence of results of Saxton and Thomason [SaTh15] - they prove that the number of Sidon sets in \(\{1,\ldots,N\}\) is at least \(2^{(1.16+o(1))N^{1/2}}\). Since each Sidon set is contained in a maximal Sidon set, and each maximal Sidon set contains at most \(2^{(1+o(1))N^{1/2}}\) Sidon sets, it follows that

\[A_1(N) \geq 2^{(0.16+o(1))N^{1/2}}.\]
theorem erdos_862.parts.i :
    ¬ (fun N : ℕ => Real.logb 2 (numMaximalSidonSets N : ℝ)) =o[atTop]
      (fun N : ℕ => (N : ℝ) ^ (1 / 2 : ℝ))

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

Erdos862.erdos_862.parts.ii

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

Let \(A_1(N)\) be the number of maximal Sidon subsets of \(\{1,\ldots,N\}\). Is it true that

\[A_1(N) > 2^{N^c}\]

for some constant \(c>0\)?

A problem of Cameron and Erdős. This is resolved as a consequence of results of Saxton and Thomason [SaTh15] - they prove that the number of Sidon sets in \(\{1,\ldots,N\}\) is at least \(2^{(1.16+o(1))N^{1/2}}\). Since each Sidon set is contained in a maximal Sidon set, and each maximal Sidon set contains at most \(2^{(1+o(1))N^{1/2}}\) Sidon sets, it follows that

\[A_1(N) \geq 2^{(0.16+o(1))N^{1/2}}.\]
theorem erdos_862.parts.ii :
    ∃ c : ℝ, 0 < c ∧ ∀ᶠ N : ℕ in atTop,
      (2 : ℝ) ^ ((N : ℝ) ^ c) < (numMaximalSidonSets N : ℝ)

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

Erdos862.erdos_862.variants.lower_bound

Solved: stated here without proof.

This is resolved as a consequence of results of Saxton and Thomason [SaTh15] - they prove that the number of Sidon sets in \(\{1,\ldots,N\}\) is at least \(2^{(1.16+o(1))N^{1/2}}\). Since each Sidon set is contained in a maximal Sidon set, and each maximal Sidon set contains at most \(2^{(1+o(1))N^{1/2}}\) Sidon sets, it follows that

\[A_1(N) \geq 2^{(0.16+o(1))N^{1/2}}.\]
theorem erdos_862.variants.lower_bound (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop,
      (2 : ℝ) ^ (((0.16 : ℝ) - ε) * (N : ℝ) ^ (1 / 2 : ℝ)) ≤ (numMaximalSidonSets N : ℝ)

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

Sources
LeanErdos862.erdos_862.parts.i · Erdos862.erdos_862.parts.ii · Erdos862.erdos_862.variants.lower_bound

TheoremErdős Problem 864#

References: - erdosproblems.com/864 - A389182 - [ErFr91] Erdős, P. and Freud, R., On sums of a Sidon-sequence. J. Number Theory 38 (1991), 196--205. - [Er92c] Erdős, P., Some of my forgotten problems in number theory. Hardy-Ramanujan J. 15 (1992), 34-50.

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

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

Erdos864.erdos_864

Open: stated without proof.

Let \(A\subseteq \{1,\ldots,N\}\) be a set such that there exists at most one \(n\) with more than one solution to \(n=a+b\) (with \(a\leq b\in A\)). Estimate the maximal possible size of \(|A|\). In particular, is it true that

\[|A| \leq (1+o(1))\frac{2}{\sqrt{3}} N^{1/2}?\]

A problem of Erdős and Freud [ErFr91] [Er92c]. For the analogous question with \(n=a-b\) they prove that \(\lvert A\rvert\sim N^{1/2}\). This is a weaker form of Erdős Problem 840.

The condition on \(A\) is HasAtMostOneRepeatedSum. We state the question as follows: for every \(\varepsilon > 0\) and all large \(N\), every such set \(A\) satisfies \(|A| \leq (1+\varepsilon)\frac{2}{\sqrt{3}} N^{1/2}\).

theorem erdos_864 :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ N : ℕ in atTop, ∀ A ⊆ Finset.Icc 1 N,
      HasAtMostOneRepeatedSum A →
        (#A : ℝ) ≤ (1 + ε) * (2 / Real.sqrt 3) * Real.sqrt (N : ℝ)

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

Erdos864.erdos_864.variants.lower_bound

Solved: stated here without proof.

Erdős and Freud [ErFr91] [Er92c] prove that

\[\lvert A\rvert \geq (1+o(1))\frac{2}{\sqrt{3}}N^{1/2}.\]

This is shown by taking a genuine Sidon set \(B\subset [1,N/3]\) of size \(\sim N^{1/2}/\sqrt{3}\) and taking the union with \(\{N-b : b\in B\}\).

That is, for every \(\varepsilon > 0\) and all large \(N\) there is a set \(A\subseteq \{1,\ldots,N\}\) with the property of Erdos864.erdos_864 and \(|A| \geq (1-\varepsilon)\frac{2}{\sqrt{3}}N^{1/2}\). So the constant \(2/\sqrt{3}\) there cannot be replaced by a smaller one.

theorem erdos_864.variants.lower_bound :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ N : ℕ in atTop, ∃ A ⊆ Finset.Icc 1 N,
      HasAtMostOneRepeatedSum A ∧
        (1 - ε) * (2 / Real.sqrt 3) * Real.sqrt (N : ℝ) ≤ #A

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

Sources
LeanErdos864.erdos_864 · Erdos864.erdos_864.variants.lower_bound

TheoremErdős Problem 865#

References: - erdosproblems.com/865 - [CES75] Choi, S. L. G. and Erdős, P. and Szemerédi, E., Some additive and multiplicative problems in number theory. Acta Arith. (1975), 37--50. - [Ci26] R. Cipollini, A sharp \(5/8\) bound for an Erdős–Sós pairwise-sums problem (2026).

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

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

Erdos865.erdos_865

Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/f8a51976fd2e66a52b4928c109fb9ae877a1a507/problems/865/Erdos865.lean; a Lean proof is at https://github.com/mrricky22/erdos-865-lean/blob/f861539107a7adeaa97462ce7c7171127696b63a/RequestProject/Main.lean#L45.

There exists a constant \(C>0\) such that, for all large \(N\), if \(A\subseteq \{1,\ldots,N\}\) has size at least \(\frac{5}{8}N+C\) then there are distinct \(a,b,c\in A\) such that \(a+b,a+c,b+c\in A\).

A problem of Erdős and Sós (also earlier considered by Choi, Erdős, and Szemerédi [CES75], but Erdős had forgotten this).

This problem was solved in the affirmative by Cipollini and GPT Pro [Ci26].

This is true. The linked proof gives it in the contrapositive and with the constant cleared: every triple-free \(A\subseteq\{1,\ldots,N\}\) satisfies \(8\lvert A\rvert\leq 5N+C\) for a fixed \(C\), for every \(N\) rather than only for large \(N\). It also shows the threshold is sharp, by exhibiting triple-free sets of size \((5N+16)/8\) for every \(N\) divisible by \(8\).

theorem erdos_865 :
    ∃ C > 0, ∀ᶠ (N : ℕ) in atTop,
      ∀ A ⊆ Icc 1 N, A.card ≥ (5 / 8 : ℝ) * N + C →
      ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, a ≠ b ∧ a ≠ c ∧ b ≠ c ∧
      a + b ∈ A ∧ a + c ∈ A ∧ b + c ∈ A

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

Erdos865.erdos_865.variants.k2

Proved here.

It is a classical folklore fact that if \(A\subseteq \{1,\ldots,2N\}\) has size \(\geq N+2\) then there are distinct \(a,b\in A\) such that \(a+b\in A\), which establishes the \(k=2\) case.

theorem erdos_865.variants.k2 (N : ℕ) :
    ∀ A ⊆ Icc 1 (2 * N), A.card ≥ N + 2 →
    ∃ a ∈ A, ∃ b ∈ A, a ≠ b ∧ a + b ∈ A

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

Erdos865.erdos_865.variants.sos

Open: stated without proof.

Erdős and Sós conjectured that \(f_k(N)\sim \frac{1}{2}\left(1+\sum_{1\leq r\leq k-2}\frac{1}{4^r}\right) N\), where \(f_k(N)\) is the minimal size of a subset of \(\{1, \dots, N\}\) guaranteeing \(k\) elements have all pairwise sums in the set.

theorem erdos_865.variants.sos :
    ∀ᵉ (k : ℕ) (hk : 2 ≤ k),
    (fun N ↦ (f N k : ℝ)) ~[atTop] (fun N ↦ (1 / 2 : ℝ) * (1 + ∑ r ∈ Icc 1 (k - 2),
      (1 / 4 : ℝ) ^ r) * N)

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

Erdos865.erdos_865.variants.upper_bound

Solved: stated here without proof.

Choi, Erdős, and Szemerédi [CES75] have proved that, for all \(k\geq 3\), there exists \(\epsilon_k>0\) such that (for large enough \(N\)) \(f_k(N)\leq \left(\frac{2}{3}-\epsilon_k\right)N\).

theorem erdos_865.variants.upper_bound (k : ℕ) (hk : 3 ≤ k) :
    ∃ ε > 0, ∀ᶠ N in atTop, (f N k : ℝ) ≤ (2 / 3 - ε) * N

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

Sources
LeanErdos865.erdos_865 · Erdos865.erdos_865.variants.k2 · Erdos865.erdos_865.variants.sos · Erdos865.erdos_865.variants.upper_bound

TheoremErdős Problem 867#

References: - erdosproblems.com/867 - [CoPh96] Coppersmith, Don and Phillips, Steven, On a question of Erdős on subsequence sums. SIAM J. Discrete Math. (1996), 173-177. - [Fr93] Freud, R., Adding numbers - on a problem of P. Erdős. James Cook Mathematical Notes (1993), 6199-6202.

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

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

Erdos867.erdos_867

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

Is it true that if \(A=\{a_1\lt \cdots \lt a_t\}\subseteq \{1,\ldots,N\}\) has no solutions to

\[a_i+a_{i+1}+\cdots+a_j\in A\]

then

\[\lvert A\rvert \leq \frac{N}{2}+O(1)?\]

In fact this problem is false. Freud [Fr93] constructed a sequence with density \(\geq 19/36\). The current best bounds are due to Coppersmith and Phillips [CoPh96], who prove that the maximal size of such an \(A\) satisfies

\[\frac{13}{24}N -O(1)\leq \lvert A\rvert \leq \left(\frac{2}{3}-\frac{1}{512}\right)N+\log N.\]
theorem erdos_867 :
    ¬ ∃ C : ℝ, ∀ N : ℕ, ∀ A ⊆ Finset.Icc 1 N, ConsecutiveSumFree A →
      (A.card : ℝ) ≤ (N : ℝ) / 2 + C

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

Erdos867.erdos_867.variants.lower_bound

Proved here.

Taking \(A=(N/2,N]\cap \mathbb{N}\) shows \(\lvert A\rvert \geq N/2-O(1)\) is possible.

theorem erdos_867.variants.lower_bound :
    ∃ C : ℝ, ∀ N : ℕ, ∃ A ⊆ Finset.Icc 1 N, ConsecutiveSumFree A ∧
      ((N : ℝ) / 2 - C ≤ (A.card : ℝ))

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

Erdos867.erdos_867.variants.adenwalla

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_Erdos867_erdos_867_variants_adenwalla.lean#L262.

Adenwalla has observed that

\[\lvert A\rvert \leq (\tfrac{2}{3}+o(1))N.\]
theorem erdos_867.variants.adenwalla (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop, ∀ A ⊆ Finset.Icc 1 N, ConsecutiveSumFree A →
      (A.card : ℝ) ≤ (2 / 3 + ε) * (N : ℝ)

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

Erdos867.erdos_867.variants.freud

Solved: stated here without proof.

Freud [Fr93] constructed a sequence with density \(\geq 19/36\).

theorem erdos_867.variants.freud :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ N : ℕ in atTop, ∃ A ⊆ Finset.Icc 1 N, ConsecutiveSumFree A ∧
      (((19 / 36 : ℝ) - ε) * (N : ℝ) ≤ (A.card : ℝ))

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

Erdos867.erdos_867.variants.coppersmith_phillips_lower_bound

Solved: stated here without proof.

The current best bounds are due to Coppersmith and Phillips [CoPh96], who prove that the maximal size of such an \(A\) satisfies

\[\frac{13}{24}N -O(1)\leq \lvert A\rvert.\]
theorem erdos_867.variants.coppersmith_phillips_lower_bound :
    ∃ C : ℝ, ∀ N : ℕ, ∃ A ⊆ Finset.Icc 1 N, ConsecutiveSumFree A ∧
      ((13 / 24 : ℝ) * (N : ℝ) - C ≤ (A.card : ℝ))

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

Erdos867.erdos_867.variants.coppersmith_phillips_upper_bound

Solved: stated here without proof.

The current best bounds are due to Coppersmith and Phillips [CoPh96], who prove that the maximal size of such an \(A\) satisfies

\[\lvert A\rvert \leq \left(\frac{2}{3}-\frac{1}{512}\right)N+\log N.\]
theorem erdos_867.variants.coppersmith_phillips_upper_bound :
    ∀ᶠ N : ℕ in atTop, ∀ A ⊆ Finset.Icc 1 N, ConsecutiveSumFree A →
      (A.card : ℝ) ≤ (2 / 3 - 1 / 512) * (N : ℝ) + Real.log (N : ℝ)

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

Sources
LeanErdos867.erdos_867 · Erdos867.erdos_867.variants.lower_bound · Erdos867.erdos_867.variants.adenwalla · Erdos867.erdos_867.variants.freud · Erdos867.erdos_867.variants.coppersmith_phillips_lower_bound · Erdos867.erdos_867.variants.coppersmith_phillips_upper_bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.