Erdős Problem 322 to Erdős Problem 347

TheoremErdős Problem 322 #

References: - erdosproblems.com/322 - [Er36] Erdős, Paul, On the Representation of an Integer as the Sum of k k-th Powers. J. London Math. Soc. (1936), 133-136. - [Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437. - [Ma36] Mahler, Kurt, Note on Hypothesis K of Hardy and Littlewood. J. London Math. Soc. (1936), 136-138.

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

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

`Erdos322.erdos_322`

Open: stated without proof.

Let $k\geq 3$ and $A\subset \mathbb{N}$ be the set of $k$th powers. What is the order of growth of $1_A^{(k)}(n)$, i.e. the number of representations of $n$ as the sum of $k$ many $k$th powers? Does there exist some $c>0$ and infinitely many $n$ such that

\[1_A^{(k)}(n) >n^c?\]

theorem erdos_322 :
    ∀ k : ℕ, 3 ≤ k → ∃ c > (0 : ℝ),
      {n : ℕ | (n : ℝ) ^ c < representationCount k n}.Infinite

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

Sources

LeanErdos322.erdos_322

TheoremErdős Problem 323 #

Reference: erdosproblems.com/323

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

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

`Erdos323.erdos_323.parts.i`

Open: stated without proof.

Is it true that $f_{k,k}(x) \gg_\epsilon x^{1-\epsilon}$ for all $\epsilon>0$?

This would have significant applications to Waring's problem. Erdős and Graham describe this as 'unattackable by the methods at our disposal'.

theorem erdos_323.parts.i :
    ∀ k ≥ 1, ∀ ε > (0 : ℝ),
      (fun (x : ℕ) ↦ (x : ℝ) ^ (1 - ε)) =O[atTop] (fun (x : ℕ) ↦ (f k k x : ℝ))

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

`Erdos323.erdos_323.parts.ii`

Open: stated without proof.

Is it true that if $m < k$ then $f_{k,m}(x) \gg x^{m/k}$ for sufficiently large $x$?

theorem erdos_323.parts.ii :
    ∀ k m : ℕ, 1 ≤ m → m < k →
      (fun (x : ℕ) ↦ (x : ℝ) ^ ((m : ℝ) / (k : ℝ))) =O[atTop] (fun (x : ℕ) ↦ (f k m x : ℝ))

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

`Erdos323.erdos_323.variants.k_eq_2`

Solved: stated here without proof.

The case $k=2$ was resolved by Landau, who showed $f_{2,2}(x) \sim \frac{cx}{\sqrt{\log x}}$ for some constant $c>0$.

theorem erdos_323.variants.k_eq_2 :
    ∃ c > 0, (fun (x : ℕ) ↦ (f 2 2 x : ℝ)) ~[atTop]
      (fun (x : ℕ) ↦ c * (x : ℝ) / Real.sqrt (Real.log (x : ℝ)))

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

`Erdos323.erdos_323.variants.k_gt_2`

Open: stated without proof.

For $k>2$ it is not known if $f_{k,k}(x)=o(x)$.

theorem erdos_323.variants.k_gt_2 :
    ∀ k > 2, (fun (x : ℕ) ↦ (f k k x : ℝ)) =o[atTop] (fun (x : ℕ) ↦ (x : ℝ))

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

Sources

LeanErdos323.erdos_323.parts.i · Erdos323.erdos_323.parts.ii · Erdos323.erdos_323.variants.k_eq_2 · Erdos323.erdos_323.variants.k_gt_2

TheoremErdős Problem 324 #

Reference: erdosproblems.com/324

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

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

`Erdos324.erdos_324`

Open: stated without proof.

Does there exist a polynomial $f(x)\in\mathbb{Z}[x]$ such that all the sums $f(a)+f(b)$ with $a < b$ nonnegative integers are distinct?

theorem erdos_324 :
    ∃ f : ℤ[X], {(a, b) : ℕ × ℕ | a < b}.InjOn fun (a, b) => f.eval (a : ℤ) + f.eval (b : ℤ)

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

`Erdos324.erdos_324.variants.quintic`

Open: stated without proof.

Probably $f(x) = x^5$ has the property that the sums $f(a)+f(b)$ with $a < b$ nonnegative integers are distinct.

theorem erdos_324.variants.quintic : {(a, b) : ℕ × ℕ | a < b}.InjOn fun (a, b) => a ^ 5 + b ^ 5

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

Sources

LeanErdos324.erdos_324 · Erdos324.erdos_324.variants.quintic

TheoremErdős Problem 325 #

Reference: erdosproblems.com/325

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

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

`Erdos325.erdos_325`

Open: stated without proof.

Writing $f_{k, 3}(x)$ for the number of integers $\leq x$ which are the sum of three $k$th powers, is it true that $f_{k, 3}(x) \gg x ^ (3 / k)$?

theorem erdos_325 :
     ∀ k : ℕ, 3 ≤ k → (fun x : ℕ => (x : ℝ) ^ (3 / k : ℝ)) =O[atTop]
      (fun x : ℕ => (cardIsSumThreePowerBelow k x : ℝ))

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

`Erdos325.erdos_325.variants.weaker`

Open: stated without proof.

Writing $f_{k, 3}(x)$ for the number of integers $\leq x$ which are the sum of three $k$th powers, is it even true that $f_{k, 3}(x) \gg_{\epsilon} x ^ (3 / k - \epsilon)$?

theorem erdos_325.variants.weaker :
    ∀ ε > 0, ∀ k : ℕ, 3 ≤ k → (fun x : ℕ => (x : ℝ) ^ ((3 / k : ℝ) - ε)) =O[atTop]
      (fun x => (cardIsSumThreePowerBelow k x : ℝ))

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

`Erdos325.erdos_325.variants.wooley`

Solved: stated here without proof.

For $k = 3$, the best known is due to Wooley [Wo15], who proved $f_{3, 3}(x) \gg x^{0.91709477}$.

[Wo15] Wooley, Trevor D., Sums of three cubes, II. Acta Arith. (2015), 73-100.

theorem erdos_325.variants.wooley :
    (fun x : ℕ => (x : ℝ) ^ (0.91709477 : ℝ)) =O[atTop]
      (fun x => (cardIsSumThreePowerBelow 3 x : ℝ))

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

Sources

LeanErdos325.erdos_325 · Erdos325.erdos_325.variants.weaker · Erdos325.erdos_325.variants.wooley

TheoremErdős Problem 326 #

References: - erdosproblems.com/326 - [ErGr80] Erdős, P. and Graham, R. L., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique (1980), p. 47. - [Ca57] Cassels, J. W. S., Über Basen der natürlichen Zahlenreihe. Abh. Math. Sem. Univ. Hamburg (1957), 247-257.

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

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

`Erdos326.erdos_326`

Open: stated without proof.

Does there exist $A = \{a_1 < a_2 < \cdots\} \subset \mathbb{N}$ which is a minimal basis of order $2$ (i.e. every large integer is the sum of $2$ elements from $A$, and no proper subset of $A$ has this property), such that

\[\lim_{k\to\infty} \frac{a_k}{k^2} = c\]

for some $c \neq 0$?

Erdős and Graham conjectured a negative answer to this question [ErGr80].

"Minimal basis of order $2$" is formalised as Minimal for the predicate Set.IsAsymptoticAddBasisOfOrder · 2 on sets of naturals ordered by inclusion.

theorem erdos_326 : ∃ (a : ℕ → ℕ), StrictMono a ∧
    Minimal (fun A : Set ℕ ↦ A.IsAsymptoticAddBasisOfOrder 2) (Set.range a) ∧
      ∃ (c : ℝ), c ≠ 0 ∧ Tendsto (fun n ↦ (a n : ℝ) / n ^ 2) atTop (𝓝 c)

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

`Erdos326.erdos_326.variants.eq`

Solved: stated here without proof.

Erdős originally asked this for any basis (not necessarily minimal); such a basis was constructed by Cassels [Ca57].

theorem erdos_326.variants.eq :
    ∃ (a : ℕ → ℕ) (_ : StrictMono a) (_ : Set.range a |>.IsAddBasisOfOrder 2) (x : ℝ) (_ : 0 < x),
      Tendsto (fun n ↦ (a n : ℝ) / n ^ 2) atTop (𝓝 x)

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

Sources

LeanErdos326.erdos_326 · Erdos326.erdos_326.variants.eq

TheoremErdős Problem 328 #

References: - erdosproblems.com/328 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique (1980). - [Er80e] Erdős, P., Some applications of Ramsey's theorem to additive number theory. European J. Combin. (1980), 43-46. - [NeRo85] J. Nešetřil and V. Rödl, Two proofs in combinatorial number theory. Proc. Amer. Math. Soc. (1985), 185-188.

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

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

`Erdos328.erdos_328`

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

Suppose $A\subseteq\mathbb{N}$ and $C>0$ is such that $1_A\ast 1_A(n)\leq C$ for all $n\in\mathbb{N}$. Can $A$ be partitioned into $t$ many subsets $A_1,\ldots,A_t$ (where $t=t(C)$ depends only on $C$) such that $1_{A_i}\ast 1_{A_i}(n)\lt C$ for all $1\leq i\leq t$ and $n\in \mathbb{N}$?

The answer is no. Asked by Erdős and Newman. Nešetřil and Rödl [NeRo85] have shown the answer is no for all $C$ (even if $t$ is also allowed to depend on $A$).

Erdős [Er80e] had previously shown the answer is no for $C=3,4$ and infinitely many other values of $C$.

See also [774].

The linked proof writes the representation function as Set.ncard {p : ℕ × ℕ | p.1 ∈ A ∧ p.2 ∈ A ∧ p.1 + p.2 = n}, which counts the same ordered pairs as sumRep, and states the partition condition as a named definition with the same two conjuncts used below. Its ∃ t additionally carries 1 ≤ t, which costs nothing: t = 0 forces A = ∅, and A = {1} has all representation counts at most C for C ≥ 1.

theorem erdos_328 :
    ¬ ∀ C : ℕ, 0 < C →
      ∃ t : ℕ, ∀ A : Set ℕ, (∀ n, sumRep A n ≤ C) →
        ∃ P : Fin t → Set ℕ, (⋃ i, P i) = A ∧
          Set.univ.PairwiseDisjoint P ∧
          ∀ i, ∀ n, sumRep (P i) n < C

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

Sources

LeanErdos328.erdos_328

TheoremErdős Problem 329: Maximum Density of Sidon Sets #

References: - erdosproblems.com/329 - [AlMi25] B. Alexeev and D. G. Mixon, Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof. arXiv:2510.19804 (2025). - [Ha47] Hall, Jr., Marshall, Cyclic projective planes. Duke Math. J. (1947), 1079--1090.

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

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

`Erdos329.erdos_329`

Open: stated without proof.

Erdős Problem 329. Let A ⊆ ℕ be a Sidon set. How large can lim sup_{N → ∞} |A ∩ {1,…,N}| / N^{1/2} be?

theorem erdos_329 : sSup {sidonUpperDensity A | (A : Set ℕ) (_ : IsSidon A)} =
    erdos_329.answer

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

`Erdos329.erdos_329.variants.lower_bound`

Solved: stated here without proof.

Erdős proved that upper density 1 / 2 can be attained; in particular, there exists a Sidon set whose upper density is at least 1 / 2.

theorem erdos_329.variants.lower_bound : ∃ (A : Set ℕ), IsSidon A ∧ sidonUpperDensity A ≥ 1/2

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

`Erdos329.erdos_329.variants.kruckeberg_1961`

Solved: stated here without proof.

Krückeberg ([Kr61]) exhibited an infinite Sidon set A with sidonUpperDensity A = 1 / Real.sqrt 2, improving Erdős’ earlier 1 / 2 lower bound.

[Kr61] Krückeberg, Fritz, $B\sb{2}$-Folgen und verwandte Zahlenfolgen. J. Reine Angew. Math. (1961), 53-60.

theorem erdos_329.variants.kruckeberg_1961 : ∃ (A : Set ℕ), IsSidon A ∧
    sidonUpperDensity A = 1 / Real.sqrt 2

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

`Erdos329.erdos_329.variants.turan_1941`

Solved: stated here without proof.

Erdős and Turán [ErTu41] proved the upper bound of 1.

[ErTu41] Erdős, P. and Turán, P., On a problem of Sidon in additive number theory, and on some related problems. J. London Math. Soc. (1941), 212-215.

theorem erdos_329.variants.turan_1941 : ∀ (A : Set ℕ), IsSidon A → sidonUpperDensity A ≤ 1

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

`Erdos329.erdos_329.variants.converse_implication`

Open: stated without proof.

The converse: if the maximum density is 1, then any finite Sidon set can be embedded in a perfect difference set modulo $n > 0$.

Since the consequent is false (due to the counterexamples in [Ha47] and [AlMi25]), this implication is logically equivalent to the statement that the maximum upper density of Sidon sets is NOT 1. Because the maximum upper density problem is still open, the truth value of this implication is also an open research problem.

theorem erdos_329.variants.converse_implication :
    (sSup {sidonUpperDensity A | (A : Set ℕ) (_ : IsSidon A)} = 1) →
    (∀ (A : Finset ℕ), IsSidon (A : Set ℕ) → ∃ (D : Set ℕ) (n : ℕ) (_ : n > 0),
      ↑A ⊆ D ∧ IsPerfectDifferenceSet D n)

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

`Erdos329.exists_sidon_pos_density`

Textbook result, stated without proof.

It is possible to construct a Sidon set with positive density.

theorem exists_sidon_pos_density : ∃ (A : Set ℕ), IsSidon A ∧ 0 < sidonUpperDensity A

Category textbook; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/329.lean, line 111.

Sources

LeanErdos329.erdos_329 · Erdos329.erdos_329.variants.lower_bound · Erdos329.erdos_329.variants.kruckeberg_1961 · Erdos329.erdos_329.variants.turan_1941 · Erdos329.erdos_329.variants.converse_implication · Erdos329.exists_sidon_pos_density

TheoremErdős Problem 330 #

Reference: erdosproblems.com/330

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

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

`Erdos330.erdos_330_statement`

Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/a5ffc87b3d684fc00ea906b9e746c283740da900/problems/330/Erdos330.lean.

Does there exist a minimal basis $A \subset \mathbb{N}$ with positive density such that, for any $n \in A$, the (upper) density of integers which cannot be represented without using $n$ is positive?

Neither set is asked to have a density, only to have positive upper density, so Set.upperDensity is used for both rather than Set.HasPosDensity. As with many of Erdős' questions "positive density" here most likely means positive upper density, and in [Er80] he considers either the lower or the upper density for the integers not representable without a fixed n. Requiring the density to exist would ask a strictly harder question than the one posed. See #3979.

Such a set exists, so the answer is yes. The linked proof gives one of order 2.

theorem erdos_330_statement :
    ∃ (A : Set ℕ), ∃ h, MinAsymptoticAddBasisOfOrder A h ∧
    0 < A.upperDensity ∧ ∀ n ∈ A, 0 < (UnrepWithout A n h).upperDensity

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

Sources

LeanErdos330.erdos_330_statement

TheoremErdős Problem 331 #

References: - erdosproblems.com/331 - [ErFr84] Erdős, P. and Freud, R., On disjoint sets of differences. J. Number Theory (1984), 99--109.

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

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

`Erdos331.erdos_331`

Solved: stated here; a Lean proof is at https://github.com/Woett/Lean-files/blob/d30552f64c55686d40b928a0a3b8e2396357a4ee/ErdosProblem331.lean.

Let $A,B\subseteq \mathbb{N}$ such that for all large $N

\[$\lvert A\cap \{1,\ldots,N\}\rvert \gg N^{1/2}\]

and

\[\lvert B\cap \{1,\ldots,N\}\rvert \gg N^{1/2}.\]

Is it true that there are infinitely many solutions to $a_1-a_2=b_1-b_2\neq 0$ with $a_1,a_2\in A$ and $b_1,b_2\in B$?

Ruzsa has observed that there is a simple counterexample: take $A$ to be the set of numbers whose binary representation has only non-zero digits in even places, and $B$ similarly but with non-zero digits only in odd places. It is easy to see $A$ and $B$ both grow like $\gg N^{1/2}$ and yet for any $n\geq 1$ there is exactly one solution to $n=a+b$ with $a\in A$ and $b\in B$.

This was formalized in Lean by van Doorn using Aristotle.

theorem erdos_331 :
    ¬ ∀ A B : Set ℕ,
    (fun (n : ℕ) ↦ (n : ℝ) ^ (1 / 2 : ℝ)) =O[atTop] (fun (n : ℕ) ↦ (count (· ∈ A) n : ℝ)) →
    (fun (n : ℕ) ↦ (n : ℝ) ^ (1 / 2 : ℝ)) =O[atTop] (fun (n : ℕ) ↦ (count (· ∈ B) n : ℝ)) →
    { s : ℕ × ℕ × ℕ × ℕ | let ⟨a₁, a₂, b₁, b₂⟩ := s
      a₁ ∈ A ∧ a₂ ∈ A ∧ b₁ ∈ B ∧ b₂ ∈ B ∧
      a₁ ≠ a₂ ∧ a₁ + b₂ = a₂ + b₁ }.Infinite

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

`Erdos331.erdos_331.variants.ruzsa`

Solved: stated here without proof.

Ruzsa suggests that a non-trivial variant of this problem arises if one imposes the stronger condition that $|A \cap \{1,\dots,N\}| \sim c_A N^{1/2}$ for some constant $c_A>0$, and similarly for $B$.

The answer is yes. Write $A(N) = |A \cap \{1,\dots,N\}|$ and $B(N) = |B \cap \{1,\dots,N\}|$. Erdős and Freud [ErFr84, Theorem 4] proved that if $a_1 - a_2 = b_1 - b_2$ has only trivial solutions and $\liminf_N \min(A(N), B(N)) / N^{1/2} > 0$, then neither $A(N) / N^{1/2}$ nor $B(N) / N^{1/2}$ tends to a limit. If there were only finitely many non-trivial solutions, removing the finitely many elements of $A$ that occur in them would give sets with the same asymptotics and no non-trivial solution.

theorem erdos_331.variants.ruzsa :
    ∀ A B : Set ℕ,
    (∃ c_A > 0, (fun (n : ℕ) ↦ (count (· ∈ A) n : ℝ)) ~[atTop] (fun (n : ℕ) ↦ c_A * (n : ℝ) ^ (1 / 2 : ℝ))) →
    (∃ c_B > 0, (fun (n : ℕ) ↦ (count (· ∈ B) n : ℝ)) ~[atTop] (fun (n : ℕ) ↦ c_B * (n : ℝ) ^ (1 / 2 : ℝ))) →
    { s : ℕ × ℕ × ℕ × ℕ | let ⟨a₁, a₂, b₁, b₂⟩ := s
      a₁ ∈ A ∧ a₂ ∈ A ∧ b₁ ∈ B ∧ b₂ ∈ B ∧
      a₁ ≠ a₂ ∧ a₁ + b₂ = a₂ + b₁ }.Infinite

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

Sources

LeanErdos331.erdos_331 · Erdos331.erdos_331.variants.ruzsa

TheoremErdős Problem 332 #

Reference: erdosproblems.com/332

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

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

`Erdos332.erdos_332`

Open: stated without proof.

Let $A\subseteq \mathbb{N}$ and $D(A)$ be the set of those numbers which occur infinitely often as $a_1 - a_2$ with $a_1, a_2\in A$. What conditions on $A$ are sufficient to ensure $D(A)$ has bounded gaps?

The sufficient conditions are the unknown erdos_332.answer. In order to solve this problem one has to provide what the sufficient conditions are, and proof that they imply the desired condition. If the condition is a solution to the problem is up to human judgement.

theorem erdos_332 (A : Set ℕ) : erdos_332.answer A → HasBoundedGaps (D_A A)

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

Sources

LeanErdos332.erdos_332

TheoremErdős Problem 333 #

References: - erdosproblems.com/333 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [ErNe77] Erdős, P. and Newman, D. J., Bases for sets of integers. J. Number Theory (1977), 420-425.

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

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

`Erdos333.erdos_333`

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

Let $A\subseteq \mathbb{N}$ be a set of density zero. Does there exist a $B$ such that $A\subseteq B+B$ and

\[\lvert B\cap \{1,\ldots,N\}\rvert =o(N^{1/2})\]

for all large $N$?

The answer is no. Erdős and Newman [ErNe77] have proved this is true when $A$ is the set of squares. In fact, Theorem 2 of [ErNe77] already implies a negative answer to this problem, but this seems to have been overlooked by Erdős and Graham.

See also [806].

theorem erdos_333 :
    ¬ ∀ A : Set ℕ, A.HasDensity 0 →
      ∃ B : Set ℕ, A ⊆ B + B ∧
        (fun N => ((B ∩ Set.Icc 1 N).ncard : ℝ)) =o[atTop]
          fun N => Real.sqrt N

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

Sources

LeanErdos333.erdos_333

TheoremErdős Problem 337 #

References: - erdosproblems.com/337 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [ErGr80b] Erdős, P. and Graham, R. L., On bases with an exact order. Acta Arith. (1980), 201-207. - [RT85] Ruzsa, I. Z. and Turjányi, S., A note on additive bases of integers. Publ. Math. Debrecen (1985), 101-104. - [Tu84] Turjányi, S., A note on basis sequences. Topics in classical number theory, Vol. I, II (Budapest, 1981) (1984), 1571-1576.

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

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

`Erdos337.erdos_337`

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/68da20b96673899166e94638f5a7fffeb7231d35/src/latest/ErdosProblems/Erdos337.lean.

Let $A\subseteq \mathbb{N}$ be an additive basis (of any finite order) such that $\lvert A\cap \{1,\ldots,N\}\rvert=o(N)$. Is it true that

\[ \lim_{N\to \infty}\frac{\lvert (A+A)\cap \{1,\ldots,N\}\rvert} {\lvert A\cap \{1,\ldots,N\}\rvert}=\infty? \]

The answer is no, and a counterexample was provided by Turjányi [Tu84]. This was generalised (to the replacement of $A+A$ by the $h$-fold sumset $hA$ for any $h\geq 2$) by Ruzsa and Turjányi [RT85].

"Additive basis" is Set.IsAsymptoticAddBasis: some finite $h$ has $hA$ containing every sufficiently large integer. The exact notion Set.IsAddBasis, which asks that $hA$ be all of $\mathbb{N}$, would force $0, 1 \in A$ and is not the class these results are about.

The linked file states the basis hypothesis as ∃ N₀, Set.Ici N₀ ⊆ iterated_sumset A k and indexes both counting functions by a real $x$ through $\lfloor x\rfloor$, where the counting functions here are indexed by $N : \mathbb{N}$.

theorem erdos_337 :
    ¬ ∀ A : Set ℕ, A.IsAsymptoticAddBasis →
      (fun N : ℕ ↦ ((A ∩ Icc 1 N).ncard : ℝ)) =o[atTop] (fun N : ℕ ↦ (N : ℝ)) →
      Tendsto (fun N : ℕ ↦ (((A + A) ∩ Icc 1 N).ncard : ℝ) / ((A ∩ Icc 1 N).ncard : ℝ))
        atTop atTop

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

`Erdos337.erdos_337.variants.h_fold`

Solved: stated here without proof.

This was generalised (to the replacement of $A+A$ by the $h$-fold sumset $hA$ for any $h\geq 2$) by Ruzsa and Turjányi [RT85].

theorem erdos_337.variants.h_fold : ∀ h : ℕ, 2 ≤ h →
    ∃ A : Set ℕ, A.IsAsymptoticAddBasis ∧
      (fun N : ℕ ↦ ((A ∩ Icc 1 N).ncard : ℝ)) =o[atTop] (fun N : ℕ ↦ (N : ℝ)) ∧
      ¬ Tendsto (fun N : ℕ ↦
          ((h • A ∩ Icc 1 N).ncard : ℝ) / ((A ∩ Icc 1 N).ncard : ℝ))
        atTop atTop

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

`Erdos337.erdos_337.variants.ruzsa_turjanyi`

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/9e4cd5617edacb313fb1da32adb4751f1fa8f603/FormalConjectures/ErdosProblems/337.lean#L95.

Ruzsa and Turjányi do prove (under the same hypotheses) that

\[ \lim_{N\to \infty}\frac{\lvert (A+A+A)\cap \{1,\ldots,3N\}\rvert} {\lvert A\cap \{1,\ldots,N\}\rvert}=\infty, \]

and conjecture that the same should be true with $(A+A)\cap \{1,\ldots,2N\}$ in the numerator.

This follows from the Plünnecke–Ruzsa inequality applied to $B=A\cap\{0,\ldots,N\}$: if $A$ is a basis of order $h$ then $hB$ contains every element of $\{N_0,\ldots,N\}$, so $(\lvert B+B\rvert/\lvert B\rvert)^h\geq \lvert hB\rvert/\lvert B\rvert\gg N/\lvert B\rvert$, which tends to infinity since $\lvert B\rvert=o(N)$.

theorem erdos_337.variants.ruzsa_turjanyi :
    ∀ A : Set ℕ, A.IsAsymptoticAddBasis →
      (fun N : ℕ ↦ ((A ∩ Icc 1 N).ncard : ℝ)) =o[atTop] (fun N : ℕ ↦ (N : ℝ)) →
      Tendsto (fun N : ℕ ↦
          (((A + A) ∩ Icc 1 (2 * N)).ncard : ℝ) / ((A ∩ Icc 1 N).ncard : ℝ))
        atTop atTop

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

`Erdos337.erdos_337.variants.three_fold`

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/9e4cd5617edacb313fb1da32adb4751f1fa8f603/FormalConjectures/ErdosProblems/337.lean#L240.

Ruzsa and Turjányi do prove (under the same hypotheses) that

\[ \lim_{N\to \infty}\frac{\lvert (A+A+A)\cap \{1,\ldots,3N\}\rvert} {\lvert A\cap \{1,\ldots,N\}\rvert}=\infty. \]

This is weaker than Erdos337.erdos_337.variants.ruzsa_turjanyi: translating by a fixed $a\in A$ with $1\leq a\leq N$ embeds $(A+A)\cap\{1,\ldots,2N\}$ into $(A+A+A)\cap\{1,\ldots,3N\}$.

theorem erdos_337.variants.three_fold :
    ∀ A : Set ℕ, A.IsAsymptoticAddBasis →
      (fun N : ℕ ↦ ((A ∩ Icc 1 N).ncard : ℝ)) =o[atTop] (fun N : ℕ ↦ (N : ℝ)) →
      Tendsto (fun N : ℕ ↦
          (((A + A + A) ∩ Icc 1 (3 * N)).ncard : ℝ) / ((A ∩ Icc 1 N).ncard : ℝ))
        atTop atTop

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

Sources

LeanErdos337.erdos_337 · Erdos337.erdos_337.variants.h_fold · Erdos337.erdos_337.variants.ruzsa_turjanyi · Erdos337.erdos_337.variants.three_fold

TheoremErdős Problem 338 #

References: - erdosproblems.com/338 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [ErGr80b] Erdős, P. and Graham, R. L., On bases with an exact order. Acta Arith. (1980), 201-207. - [HHP07] Hegyvári, Norbert and Hennecart, François and Plagne, Alain, Answer to a question by Burr and Erdős on restricted addition, and related results. Combin. Probab. Comput. (2007), 747--756. - [He05] Hennecart, François, On the restricted order of asymptotic bases of order two. Ramanujan J. (2005), 123--130. - [Ke57] Kelly, John B., Restricted bases. Amer. J. Math. (1957), 258-264. - [Pa33] Pall, Gordon, On Sums of Squares. Amer. Math. Monthly (1933), 10-18. - [Sc54] Schinzel, A., Sur la décomposition des nombres naturels en sommes de nombres triangulaires distincts. Bull. Acad. Polon. Sci. Cl. III. (1954), 409-410.

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

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

`Erdos338.erdos_338`

Open: stated without proof.

The restricted order of a basis $A$ is the least integer $t$ (if it exists) such that every large integer is the sum of at most $t$ distinct summands from $A$. What are necessary and sufficient conditions that this exists?

A solution must fill in Erdos338.erdos_338.answer with the condition and prove the equivalence. Whether a condition is a satisfactory answer is up to human judgement.

theorem erdos_338 :
    ∀ A : Set ℕ, (∃ h, HasOrder A h) → ((∃ t, HasRestrictedOrder A t) ↔ erdos_338.answer A)

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

`Erdos338.erdos_338.variants.bounded_by_order`

Open: stated without proof.

Can the restricted order of a basis be bounded (when it exists) in terms of the order of the basis?

HasOrder A h only says that the order of $A$ is at most $h$. This gives the same question, since $f$ can be replaced by its running maximum. Kelly [Ke57] showed that $f(2) = 4$ works, and Hennecart [He05] showed that $4$ is optimal. Hegyvári, Hennecart and Plagne [HHP07] showed that any such $f$ has $f(k) \geq 2^{k-2}+k-1$ for $k \geq 3$.

theorem erdos_338.variants.bounded_by_order :
    ∃ f : ℕ → ℕ, ∀ (A : Set ℕ) (h : ℕ), HasOrder A h →
      (∃ t, HasRestrictedOrder A t) → HasRestrictedOrder A (f h)

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

`Erdos338.erdos_338.variants.eq_order`

Open: stated without proof.

What are necessary and sufficient conditions that the restricted order of a basis $A$ is equal to the order of $A$?

For a basis, basisOrder A is finite, so the equality also says that the restricted order exists. The condition is Erdos338.erdos_338.variants.eq_order.answer, as in Erdos338.erdos_338.

theorem erdos_338.variants.eq_order :
    ∀ A : Set ℕ, (∃ h, HasOrder A h) →
      (restrictedOrder A = basisOrder A ↔ erdos_338.variants.eq_order.answer A)

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

`Erdos338.erdos_338.variants.basis_after_finite_removal`

Open: stated without proof.

Is it true that if $A \setminus F$ is a basis for all finite sets $F$ then $A$ must have a restricted order?

theorem erdos_338.variants.basis_after_finite_removal :
    ∀ A : Set ℕ, (∀ F : Set ℕ, F.Finite → ∃ h, HasOrder (A \ F) h) →
      ∃ t, HasRestrictedOrder A t

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

`Erdos338.erdos_338.variants.same_order_after_finite_removal`

Open: stated without proof.

Is it true that if the sets $A \setminus F$, for all finite sets $F$, are bases of the same order, then $A$ must have a restricted order?

We read "the same order" literally: every $A \setminus F$ has the same exact order $h$. This is equivalent to asking that the orders of the sets $A \setminus F$ are bounded. Removing elements can only raise the order, so if the orders are bounded, their maximum is attained at some $F_0$, and $A \setminus F_0 \subseteq A$ satisfies the literal hypothesis.

theorem erdos_338.variants.same_order_after_finite_removal :
    ∀ A : Set ℕ,
      (∃ h : ℕ, ∀ F : Set ℕ, F.Finite → basisOrder (A \ F) = (h : ℕ∞)) →
      ∃ t, HasRestrictedOrder A t

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

`Erdos338.erdos_338.variants.bateman`

Solved: stated here without proof.

Bateman observed that for $h \geq 3$ the set $A = \{1\} \cup \{x > 0 : h \mid x\}$ is a basis of order $h$ with no restricted order.

theorem erdos_338.variants.bateman (h : ℕ) (hh : 3 ≤ h) :
    basisOrder (insert 1 {x : ℕ | 0 < x ∧ h ∣ x}) = h ∧
      ¬ ∃ t, HasRestrictedOrder (insert 1 {x : ℕ | 0 < x ∧ h ∣ x}) t

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

`Erdos338.erdos_338.variants.kelly`

Solved: stated here without proof.

Kelly [Ke57] showed that any basis of order $2$ has restricted order at most $4$.

theorem erdos_338.variants.kelly (A : Set ℕ) (hA : HasOrder A 2) : HasRestrictedOrder A 4

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

`Erdos338.erdos_338.variants.kelly_lowerDensity`

Solved: stated here without proof.

Kelly [Ke57] showed that any basis of order $2$ with positive lower density has restricted order at most $3$.

theorem erdos_338.variants.kelly_lowerDensity (A : Set ℕ) (hA : HasOrder A 2)
    (hd : 0 < A.lowerDensity) : HasRestrictedOrder A 3

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

`Erdos338.erdos_338.variants.kelly_conjecture`

Solved: stated here without proof.

Kelly [Ke57] conjectured that any basis of order $2$ has restricted order at most $3$.

This was disproved by Hennecart [He05], who constructed a basis of order $2$ with restricted order $4$.

theorem erdos_338.variants.kelly_conjecture :
    ¬ ∀ A : Set ℕ, HasOrder A 2 → HasRestrictedOrder A 3

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

`Erdos338.erdos_338.variants.squares`

Solved: stated here without proof.

The set of squares has order $4$ and restricted order $5$ (see [Pa33]).

Here $0$ is a square. The order is $4$ by Lagrange's four-square theorem, and is not $3$ because no integer $\equiv 7 \pmod 8$ is a sum of three squares.

theorem erdos_338.variants.squares :
    basisOrder (Set.range fun k : ℕ ↦ k ^ 2) = 4 ∧
      restrictedOrder (Set.range fun k : ℕ ↦ k ^ 2) = 5

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

`Erdos338.erdos_338.variants.triangular`

Solved: stated here without proof.

The set of triangular numbers has order $3$ and restricted order $3$ (see [Sc54]).

Here $0$ is a triangular number.

theorem erdos_338.variants.triangular :
    basisOrder (Set.range fun k : ℕ ↦ k * (k + 1) / 2) = 3 ∧
      restrictedOrder (Set.range fun k : ℕ ↦ k * (k + 1) / 2) = 3

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

`Erdos338.erdos_338.variants.hegyvari_hennecart_plagne`

Solved: stated here without proof.

Hegyvári, Hennecart and Plagne [HHP07] showed that for all $k \geq 2$ there exists a basis of order $k$ which has restricted order at least $2^{k-2}+k-1$.

The basis built in the proof of Theorem 4 of [HHP07] (for $k \geq 3$) has order exactly $k$ and a finite restricted order, equal to $2^{k-2}+k-1$. The finiteness matters: without it, Bateman's example Erdos338.erdos_338.variants.bateman would already give the bound. For $k = 2$ the bound is $2$, and $A = \{1\} \cup \{x : 2 \mid x\}$ works.

theorem erdos_338.variants.hegyvari_hennecart_plagne :
    ∀ k : ℕ, 2 ≤ k → ∃ A : Set ℕ,
      basisOrder A = k ∧ restrictedOrder A = (2 ^ (k - 2) + k - 1 : ℕ)

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

Sources

TheoremErdős Problem 340 #

Reference: erdosproblems.com/340

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

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

`Erdos340.erdos_340`

Open: stated without proof.

Let $A = \{1, 2, 4, 8, 13, 21, 31, 45, 66, 81, 97, \ldots\}$ be the greedy Sidon sequence: we begin with $1$ and iteratively include the next smallest integer that preserves the Sidon property (i.e. there are no non-trivial solutions to $a + b = c + d$). What is the order of growth of $A$? Is it true that $|A \cap \{1, \ldots, N\}| \gg N^{1/2 - \varepsilon}$ for all $\varepsilon > 0$ and large $N$?

theorem erdos_340 (ε : ℝ) (hε : ε > 0) :
    (fun n : ℕ ↦ √n / n ^ ε) =O[atTop]
      fun n : ℕ ↦ ((Set.range greedySidon ∩ Set.Icc 1 n).ncard : ℝ)

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

`Erdos340.erdos_340.variants.isTheta`

Open: stated without proof.

Let $A = \{1, 2, 4, 8, 13, 21, 31, 45, 66, 81, 97, \ldots\}$ be the greedy Sidon sequence: we begin with $1$ and iteratively include the next smallest integer that preserves the Sidon property (i.e. there are no non-trivial solutions to $a + b = c + d$). What is the order of growth of $A$? Is it true that $|A \cap \{1, \ldots, N\}| \gg N^{1/2 - \varepsilon}$ for all $\varepsilon > 0$ and large $N$?

theorem erdos_340.variants.isTheta (ε : ℝ) (hε : ε > 0) :
    (fun n : ℕ ↦ ((Set.range greedySidon ∩ Set.Icc 1 n).ncard : ℝ)) =Θ[atTop]
      erdos_340.variants.isTheta.answer

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

`Erdos340.erdos_340.variants.third`

Textbook result, stated without proof.

It is trivial that this sequence grows at least like $\gg N^{1/3}$.

theorem erdos_340.variants.third (ε : ℝ) (hε : ε > 0) :
    (fun n : ℕ ↦ (n : ℝ) ^ ((1 : ℝ) / 3)) =O[atTop]
      fun n : ℕ ↦ ((Set.range greedySidon ∩ Set.Icc 1 n).ncard : ℝ)

Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/340.lean, line 104.

`Erdos340.erdos_340.variants.sub_hasPosDensity`

Open: stated without proof.

Erdős and Graham [ErGr80] also asked about the difference set $A - A$ and whether this has positive density.

[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

theorem erdos_340.variants.sub_hasPosDensity :
    Set.HasPosDensity (Set.range greedySidon - Set.range greedySidon)

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

`Erdos340.erdos_340.variants._22_mem_sub`

Proved here.

Erdős and Graham [ErGr80] also asked about the difference set $A - A$ and whether this contains $22$, which it does.

[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

theorem erdos_340.variants._22_mem_sub :
    22 ∈ Set.range greedySidon - Set.range greedySidon

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

`Erdos340.erdos_340.variants._33_mem_sub`

Open: stated without proof.

The smallest integer which is unknown to be in $A - A$ is $33$.

theorem erdos_340.variants._33_mem_sub :
    33 ∈ Set.range greedySidon - Set.range greedySidon

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

`Erdos340.erdos_340.variants.cofinite_sub`

Open: stated without proof.

It may be true that all or almost all integers are in $A - A$.

theorem erdos_340.variants.cofinite_sub :
    ∀ᶠ n in cofinite, n ∈ Set.range greedySidon - Set.range greedySidon

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

`Erdos340.erdos_340.variants.co_density_zero_sub`

Open: stated without proof.

It may be true that all or almost all integers are in $A - A$.

theorem erdos_340.variants.co_density_zero_sub :
    ∃ S : Set ℕ, S.HasDensity 0 ∧ ∀ n ∈ Sᶜ, n ∈ Set.range greedySidon - Set.range greedySidon

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

Sources

LeanErdos340.erdos_340 · Erdos340.erdos_340.variants.isTheta · Erdos340.erdos_340.variants.third · Erdos340.erdos_340.variants.sub_hasPosDensity · Erdos340.erdos_340.variants._22_mem_sub · Erdos340.erdos_340.variants._33_mem_sub · Erdos340.erdos_340.variants.cofinite_sub · Erdos340.erdos_340.variants.co_density_zero_sub

TheoremErdős Problem 341 #

References: * erdosproblems.com/341 * Ben Green's Open Problem 7 * [Li26] Li, Z., Counterexamples to Erdős Problem 341 (2026), https://github.com/LiAlreadyExists/Erdos-341/blob/main/paper/Erdos341.pdf

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

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

`Erdos341.erdos_341`

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

Let $A=\{a_1 < \cdots < a_k\}$ be a finite set of integers and extend it to an infinite sequence $\overline{A}=\{a_1 < a_2 < \cdots \}$ by defining $a_{n+1}$ for $n \geq k$ to be the least integer exceeding $a_n$ which is not of the form $a_i + a_j$ with $i,j \leq n$. Is it true that the sequence of differences $a_{m+1}-a_m$ is eventually periodic?

This problem is discussed under Problem 7 on Green's open problems list.

The answer is no: Li [Li26] (with GPT-5.6 Sol) showed that the greedy extension of the seed set $A = \{1, 2, 3, 5, 7, 13, 22, 27, 28, 32, 36, 40, 47, 48, 52, 63, 71, 77, 81, 89, 97\}$ has a sequence of differences that is not eventually periodic. The linked formal proof exhibits such a sequence a : ℕ → ℕ (strictly increasing, with the greedy rule holding from some index on, and with n ↦ a (n + 1) - a n not eventually periodic); casting it to ℤ gives a counterexample to the statement below.

theorem erdos_341 :
    ¬ ∀ (a : ℕ → ℤ),
      (∀ᶠ n in atTop,
        IsLeast { x | a n < x ∧ x ∉ { a i + a j | (i ≤ n) (j ≤ n) } } (a (n + 1))) →
      let d := fun i ↦ a (i + 1) - a i
      ∃ p > 0, ∀ᶠ m in atTop, d (m + p) = d m

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

Sources

LeanErdos341.erdos_341

TheoremErdős Problem 342 #

References: - erdosproblems.com/342 - Ben Green's Open Problem 7 - OEIS A002858 - [Gu04] Guy, Richard K., Unsolved problems in number theory (2004), xviii+437.

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

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

`Erdos342.erdos_342.parts.i`

Open: stated without proof.

Do infinitely many pairs $(a, a+2)$ occur in Ulam's sequence?

theorem erdos_342.parts.i :
    ∀ a : ℕ → ℕ, IsUlamSequence a →
      Set.Infinite {n : ℕ | ∃ m, a m = a n + 2}

Category research open; AMS 05 Combinatorics, 11 Number theory, 40 Sequences, series, summability. Declared in FormalConjectures/ErdosProblems/342.lean, line 115.

`Erdos342.erdos_342.parts.ii`

Open: stated without proof.

Does Ulam's sequence eventually have periodic differences? That is, is $a(n+1) - a(n)$ eventually periodic?

theorem erdos_342.parts.ii :
    ∀ a : ℕ → ℕ, IsUlamSequence a →
      let d (n : ℕ) : ℤ := a (n + 1) - a n
      ∃ p > 0, ∀ᶠ m in atTop, d (m + p) = d m

Category research open; AMS 05 Combinatorics, 11 Number theory, 40 Sequences, series, summability. Declared in FormalConjectures/ErdosProblems/342.lean, line 124.

`Erdos342.erdos_342.parts.iii`

Open: stated without proof.

Part (iii), is the density of the sequence 0?

theorem erdos_342.parts.iii :
    ∀ a : ℕ → ℕ, IsUlamSequence a →
      Set.upperDensity (Set.range a) = 0

Category research open; AMS 05 Combinatorics, 11 Number theory, 40 Sequences, series, summability. Declared in FormalConjectures/ErdosProblems/342.lean, line 134.

Sources

LeanErdos342.erdos_342.parts.i · Erdos342.erdos_342.parts.ii · Erdos342.erdos_342.parts.iii

TheoremErdős Problem 344 #

References: - erdosproblems.com/344 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Er61b] Erdős, P., On the representation of large integers as sums of distinct summands taken from a fixed set. Acta Arith. (1961/62), 345-354. - [Fo66] Folkman, J., On the representation of integers as sums of distinct terms from a fixed sequence. Canadian J. Math. 18 (1966), 643-655. - [SzVu06] Szemerédi, E. and Vu, V., Long arithmetic progressions in sumsets: thresholds and bounds. J. Amer. Math. Soc. 19 (2006), 119-169. - [SzVu06b] Szemerédi, E. and Vu, V., Finite and infinite arithmetic progressions in sumsets. Ann. of Math. 163 (2006), 1-35.

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

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

`Erdos344.erdos_344`

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

If $A\subseteq \mathbb{N}$ is a set of integers such that

\[\lvert A\cap \{1,\ldots,N\}\rvert\gg N^{1/2}\]

for all $N$ then must $A$ be subcomplete? That is, must

\[P(A) = \left\{\sum_{n\in B}n : B\subseteq A\textrm{ finite }\right\}\]

contain an infinite arithmetic progression?

This is true, and was proved by Szemerédi and Vu [SzVu06].

The implied constant is absolute, as in [SzVu06b, Corollary 1.4].

theorem erdos_344 :
    ∃ C : ℝ, 0 < C ∧ ∀ A : Set ℕ,
      (∀ᶠ N : ℕ in atTop, C * Real.sqrt N ≤ A.countUpTo N) → IsSubcomplete A

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

`Erdos344.erdos_344.variants.sqrt_two`

Open: stated without proof.

The stronger conjecture that this is true under

\[\lvert A\cap \{1,\ldots,N\}\rvert\geq (2N)^{1/2}\]

seems to be still open (this would be best possible as shown by [Er61b]).

The bound is required for all sufficiently large $N$: at $N=1$, it is impossible since $\lvert A\cap\{1\}\rvert\leq 1\lt \sqrt{2}$.

theorem erdos_344.variants.sqrt_two :
    ∀ A : Set ℕ, (∀ᶠ N : ℕ in atTop, Real.sqrt (2 * N) ≤ A.countUpTo N) →
      IsSubcomplete A

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

`Erdos344.erdos_344.variants.folkman`

Proved here.

Folkman proved this under the stronger assumption that

\[\lvert A\cap \{1,\ldots,N\}\rvert\gg N^{1/2+\epsilon}\]

for some $\epsilon>0$ [Fo66].

theorem erdos_344.variants.folkman :
    ∀ ε : ℝ, 0 < ε → ∀ c : ℝ, 0 < c → ∀ A : Set ℕ,
      (∀ᶠ N : ℕ in atTop, c * (N : ℝ) ^ ((1 : ℝ) / 2 + ε) ≤ A.countUpTo N) →
      IsSubcomplete A

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

Sources

LeanErdos344.erdos_344 · Erdos344.erdos_344.variants.sqrt_two · Erdos344.erdos_344.variants.folkman

TheoremErdős Problem 345 #

References: - erdosproblems.com/345 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980), p. 55. - [Ki17] Kim, D., On the largest integer that is not a sum of distinct positive nth powers. Journal of Integer Sequences 20 (2017), Article 17.7.5. arXiv:1610.02439

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

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

`Erdos345.erdos_345`

Open: stated without proof.

Let $A\subseteq \mathbb{N}$ be a complete sequence, and define the threshold of completeness $T(A)$ to be the least integer $m$ such that all $n\geq m$ are in

\[P(A) = \left\{\sum_{n\in B}n : B\subseteq A\textrm{ finite }\right\}\]

(the existence of $T(A)$ is guaranteed by completeness).

Is it true that there are infinitely many $k$ such that $T(n^k)>T(n^{k+1})$?

Here $T(n^k)$ means the threshold of the positive $k$-th powers. Least-threshold witnesses ensure that the thresholds exist. We restrict to $k\geq 1$, since the zeroth powers form $\{1\}$, which is incomplete. Positive powers are complete [Ki17].

theorem erdos_345 :
    {k : ℕ | 0 < k ∧ ∃ a b : ℕ, IsLeast (thresholds (kthPowers k)) a ∧
      IsLeast (thresholds (kthPowers (k + 1))) b ∧ b < a}.Infinite

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

`Erdos345.kthPowers_isAddComplete`

Solved: stated here without proof.

Every set of positive $k$-th powers with $k\geq 1$ is complete [Ki17].

theorem kthPowers_isAddComplete : ∀ k : ℕ, 0 < k → IsAddComplete (kthPowers k)

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

Sources

LeanErdos345.erdos_345 · Erdos345.kthPowers_isAddComplete

TheoremErdős Problem 346 #

References: - erdosproblems.com/346 - [Gr64d] Graham, R. L., A property of Fibonacci numbers. Fibonacci Quart. (1964), 1-10. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). -

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

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

`Erdos346.erdos_346`

Solved: stated here without proof.

Is it true that for every lacunary, strongly complete sequence A that is not complete whenever infinitely many terms are removed from it, lim A (n + 1) / A n = (1 + √5) / 2?

The answer is no. A counterexample recorded at [erdosproblems.com/346] has all successive ratios at least 6 / 5, but has subsequences of successive ratios tending to two different limits, (1 + √5) / 2 and (1 + √5) / 2 + 1 / 4.

theorem erdos_346 : ¬ ∀ {A : ℕ → ℕ}, IsLacunary A → IsAddStronglyCompleteNatSeq A →
    (∀ B : Set ℕ, B ⊆ range A → B.Infinite → ¬ IsAddComplete (range A \ B)) →
    Tendsto (fun n => A (n + 1) / (A n : ℝ)) atTop (𝓝 ((1 + √5) / 2))

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

`Erdos346.erdos_346.variants.f_isAddStronglyCompleteNatSeq`

Solved: stated here without proof.

The sequence f is strongly complete, and this is proved in [Gr64d].

theorem erdos_346.variants.f_isAddStronglyCompleteNatSeq : IsAddStronglyCompleteNatSeq f

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

`Erdos346.erdos_346.variants.f_not_isAddComplete`

Proved here.

The sequence f is not complete whenever infinitely many terms are removed from it, and this is proved in [Gr64d].

theorem erdos_346.variants.f_not_isAddComplete {B : Set ℕ} (h : B ⊆ range f) (hB : B.Infinite) :
    ¬ IsAddComplete (range f \ B)

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

`Erdos346.erdos_346.variants.gt_goldenRatio_not_IsAddComplete`

Proved here.

Erdős and Graham [ErGr80] remark that it is easy to see that if A (n + 1) / A n > (1 + √5) / 2 then the second property is automatically satisfied.

theorem erdos_346.variants.gt_goldenRatio_not_IsAddComplete {A : ℕ → ℕ}
    (hA : ∀ n, (1 + √5) / 2 * A n < A (n + 1)) {B : Set ℕ} (h : B ⊆ range A) (hB : B.Infinite) :
    ¬ IsAddComplete (range A \ B)

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

`Erdos346.erdos_346.variants.example`

Solved: stated here without proof.

Erdős and Graham [ErGr80] also say that it is not hard to construct very irregular sequences satisfying the aforementioned properties: there is a strictly increasing sequence A that is strongly complete and not complete whenever infinitely many terms are removed from it, but with $\liminf_n A(n+1)/A(n) = 1$ and $\limsup_n A(n+1)/A(n) = \infty$.

theorem erdos_346.variants.example : ∃ A : ℕ → ℕ, StrictMono A ∧ IsAddStronglyCompleteNatSeq A ∧
    (∀ B : Set ℕ, B ⊆ range A → B.Infinite → ¬ IsAddComplete (range A \ B)) ∧
    liminf (fun n => A (n + 1) / (A n : ℝ)) atTop = 1 ∧
    limsup (fun n => A (n + 1) / (A n : ENNReal)) atTop = ⊤

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

Sources

LeanErdos346.erdos_346 · Erdos346.erdos_346.variants.f_isAddStronglyCompleteNatSeq · Erdos346.erdos_346.variants.f_not_isAddComplete · Erdos346.erdos_346.variants.gt_goldenRatio_not_IsAddComplete · Erdos346.erdos_346.variants.example

TheoremErdős Problem 347 #

Reference: erdosproblems.com/347

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

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

`Erdos347.erdos_347`

Solved: stated here; a Lean proof is at https://github.com/ebarschkis/ErdosProblem/blob/main/Problem347/Formalization.lean.

Is there a sequence $A=\{a_1\leq a_2\leq \cdots\}$ of integers with

\[\lim \frac{a_{n+1}}{a_n}=2\]

such that

\[P(A')= \left\{\sum_{n\in B}n : B\subseteq A'\textrm{ finite }\right\}\]

has density $1$ for every cofinite subsequence $A'$ of $A$?

This has been solved in the affirmative by ebarschkis in the comments (based on idea of Tao and van Doorn, also in the comments).

This was formalized in Lean by Barschkis using Aristotle.

theorem erdos_347 :
    ∃ a : ℕ → ℕ, (Monotone a) ∧
      (Tendsto (fun n ↦ (a (n + 1) : ℝ) / (a n : ℝ)) atTop (𝓝 2)) ∧
      (∀ ι : ℕ → ℕ, (range ι)ᶜ.Finite → HasDensity (𝓟 (range (a ∘ ι))) 1)

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

Sources

LeanErdos347.erdos_347

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Erdős Problem 322 to Erdős Problem 347

TheoremErdős Problem 322#

Erdos322.erdos_322

Sources

TheoremErdős Problem 323#

Erdos323.erdos_323.parts.i

Erdos323.erdos_323.parts.ii

Erdos323.erdos_323.variants.k_eq_2

Erdos323.erdos_323.variants.k_gt_2

Sources

TheoremErdős Problem 324#

Erdos324.erdos_324

Erdos324.erdos_324.variants.quintic

Sources

TheoremErdős Problem 325#

Erdos325.erdos_325

Erdos325.erdos_325.variants.weaker

Erdos325.erdos_325.variants.wooley

Sources

TheoremErdős Problem 326#

Erdos326.erdos_326

Erdos326.erdos_326.variants.eq

Sources

TheoremErdős Problem 328#

Erdos328.erdos_328

Sources

TheoremErdős Problem 329: Maximum Density of Sidon Sets#

Erdos329.erdos_329

Erdos329.erdos_329.variants.lower_bound

Erdos329.erdos_329.variants.kruckeberg_1961

Erdos329.erdos_329.variants.turan_1941

Erdos329.erdos_329.variants.converse_implication

Erdos329.exists_sidon_pos_density

Sources

TheoremErdős Problem 330#

Erdos330.erdos_330_statement

Sources

TheoremErdős Problem 331#

Erdos331.erdos_331

Erdos331.erdos_331.variants.ruzsa

Sources

TheoremErdős Problem 332#

Erdos332.erdos_332

Sources

TheoremErdős Problem 333#

Erdos333.erdos_333

Sources

TheoremErdős Problem 337#

Erdos337.erdos_337

Erdos337.erdos_337.variants.h_fold

Erdos337.erdos_337.variants.ruzsa_turjanyi

Erdos337.erdos_337.variants.three_fold

Sources

TheoremErdős Problem 338#

Erdos338.erdos_338

Erdos338.erdos_338.variants.bounded_by_order

Erdos338.erdos_338.variants.eq_order

Erdos338.erdos_338.variants.basis_after_finite_removal

Erdos338.erdos_338.variants.same_order_after_finite_removal

Erdos338.erdos_338.variants.bateman

Erdos338.erdos_338.variants.kelly

Erdos338.erdos_338.variants.kelly_lowerDensity

Erdos338.erdos_338.variants.kelly_conjecture

Erdos338.erdos_338.variants.squares

Erdos338.erdos_338.variants.triangular

Erdos338.erdos_338.variants.hegyvari_hennecart_plagne

Sources

TheoremErdős Problem 340#

Erdos340.erdos_340

Erdos340.erdos_340.variants.isTheta

Erdos340.erdos_340.variants.third

Erdos340.erdos_340.variants.sub_hasPosDensity

Erdos340.erdos_340.variants._22_mem_sub

Erdos340.erdos_340.variants._33_mem_sub

Erdos340.erdos_340.variants.cofinite_sub

Erdos340.erdos_340.variants.co_density_zero_sub

Sources

TheoremErdős Problem 341#

Erdos341.erdos_341

Sources

TheoremErdős Problem 322 #

`Erdos322.erdos_322`

TheoremErdős Problem 323 #

`Erdos323.erdos_323.parts.i`

`Erdos323.erdos_323.parts.ii`

`Erdos323.erdos_323.variants.k_eq_2`

`Erdos323.erdos_323.variants.k_gt_2`

TheoremErdős Problem 324 #

`Erdos324.erdos_324`

`Erdos324.erdos_324.variants.quintic`

TheoremErdős Problem 325 #

`Erdos325.erdos_325`

`Erdos325.erdos_325.variants.weaker`

`Erdos325.erdos_325.variants.wooley`

TheoremErdős Problem 326 #

`Erdos326.erdos_326`

`Erdos326.erdos_326.variants.eq`

TheoremErdős Problem 328 #

`Erdos328.erdos_328`

TheoremErdős Problem 329: Maximum Density of Sidon Sets #

`Erdos329.erdos_329`

`Erdos329.erdos_329.variants.lower_bound`

`Erdos329.erdos_329.variants.kruckeberg_1961`

`Erdos329.erdos_329.variants.turan_1941`

`Erdos329.erdos_329.variants.converse_implication`

`Erdos329.exists_sidon_pos_density`

TheoremErdős Problem 330 #

`Erdos330.erdos_330_statement`

TheoremErdős Problem 331 #

`Erdos331.erdos_331`

`Erdos331.erdos_331.variants.ruzsa`

TheoremErdős Problem 332 #

`Erdos332.erdos_332`

TheoremErdős Problem 333 #

`Erdos333.erdos_333`

TheoremErdős Problem 337 #

`Erdos337.erdos_337`

`Erdos337.erdos_337.variants.h_fold`

`Erdos337.erdos_337.variants.ruzsa_turjanyi`

`Erdos337.erdos_337.variants.three_fold`

TheoremErdős Problem 338 #

`Erdos338.erdos_338`

`Erdos338.erdos_338.variants.bounded_by_order`

`Erdos338.erdos_338.variants.eq_order`

`Erdos338.erdos_338.variants.basis_after_finite_removal`

`Erdos338.erdos_338.variants.same_order_after_finite_removal`

`Erdos338.erdos_338.variants.bateman`

`Erdos338.erdos_338.variants.kelly`

`Erdos338.erdos_338.variants.kelly_lowerDensity`

`Erdos338.erdos_338.variants.kelly_conjecture`

`Erdos338.erdos_338.variants.squares`

`Erdos338.erdos_338.variants.triangular`

`Erdos338.erdos_338.variants.hegyvari_hennecart_plagne`

TheoremErdős Problem 340 #

`Erdos340.erdos_340`

`Erdos340.erdos_340.variants.isTheta`

`Erdos340.erdos_340.variants.third`

`Erdos340.erdos_340.variants.sub_hasPosDensity`

`Erdos340.erdos_340.variants._22_mem_sub`

`Erdos340.erdos_340.variants._33_mem_sub`

`Erdos340.erdos_340.variants.cofinite_sub`

`Erdos340.erdos_340.variants.co_density_zero_sub`

TheoremErdős Problem 341 #

`Erdos341.erdos_341`

TheoremErdős Problem 342 #

`Erdos342.erdos_342.parts.i`

`Erdos342.erdos_342.parts.ii`

`Erdos342.erdos_342.parts.iii`

TheoremErdős Problem 344 #

`Erdos344.erdos_344`

`Erdos344.erdos_344.variants.sqrt_two`

`Erdos344.erdos_344.variants.folkman`

TheoremErdős Problem 345 #

`Erdos345.erdos_345`

`Erdos345.kthPowers_isAddComplete`

TheoremErdős Problem 346 #

`Erdos346.erdos_346`

`Erdos346.erdos_346.variants.f_isAddStronglyCompleteNatSeq`

`Erdos346.erdos_346.variants.f_not_isAddComplete`

`Erdos346.erdos_346.variants.gt_goldenRatio_not_IsAddComplete`