Erdős Problem 773 to Erdős Problem 798

TheoremErdős Problem 773#

References: - erdosproblems.com/773 - [AlEr85] Alon, Noga and Erdős, P., An application of graph theory to additive number theory. European J. Combin. (1985), 201-203. - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [LeTh95] Lefmann, Hanno and Thiele, Torsten, Point sets with distinct distances. Combinatorica (1995), 379--408.

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

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

Erdos773.erdos_773

Open: stated without proof.

What is the size of the largest Sidon subset \(A\subseteq\{1,2^2,\ldots,N^2\}\)? Is it \(N^{1-o(1)}\)?

theorem erdos_773 :
    ∀ ε > (0 : ℝ), ∀ᶠ N : ℕ in atTop,
      (N : ℝ) ^ (1 - ε) ≤
        (Finset.maxSidonSubsetCard
          (Finset.image (fun n : ℕ => n ^ 2) (Finset.Icc 1 N)) : ℝ)

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

Sources

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

LeanErdos773.erdos_773

TheoremErdős Problem 774#

Reference: erdosproblems.com/774

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

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

Erdos774.erdos_774

Open: stated without proof.

Is every proportionately dissociated (infinite) set the union of a finite number of dissociated sets?

theorem erdos_774 : ∀ (A : Set ℕ), A.Infinite → A.IsProportionatelyDissociated →
    ∃ (T : Set (Set ℕ)), (∀ S ∈ T, S.IsDissociated) ∧ T.Finite ∧ A = ⋃₀ T

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

Sources

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

LeanErdos774.erdos_774

TheoremErdős Problem 775#

References: - erdosproblems.com/775 - [Ga25] Gao, J., On cliques in hypergraphs. arXiv:2510.14804 (2025). - [MoMo65] Moon, J. W. and Moser, L., On cliques in graphs. Israel J. Math. (1965), 23-28. - [Sp71] Spencer, J. H., On cliques in graphs. Israel J. Math. (1971), 419-421.

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

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

Erdos775.erdos_775

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

Is there a \(3\)-uniform hypergraph on \(n\) vertices which contains at least \(n-O(1)\) different sizes of cliques (maximal complete subgraphs)?

The answer is no, as proved by Gao [Ga25]: more generally, for any \(k\geq 3\), every \(k\)-uniform hypergraph on \(n\) vertices contains at most \(n-f_k(n)\) different sizes of cliques, where \(f_k(n)\to \infty\) as \(n\to \infty\).

theorem erdos_775 :
    ¬ ∃ C : ℕ, ∃ᶠ n : ℕ in atTop, ∃ H : UniformHypergraph (Fin n) 3,
      n - C ≤ (UniformHypergraph.cliqueSizes H).ncard

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

Erdos775.erdos_775.variants.gao

Solved: stated here without proof.

The answer is no, as proved by Gao [Ga25]: more generally, for any \(k\geq 3\), every \(k\)-uniform hypergraph on \(n\) vertices contains at most \(n-f_k(n)\) different sizes of cliques, where \(f_k(n)\to \infty\) as \(n\to \infty\).

theorem erdos_775.variants.gao :
    ∃ f : ℕ → ℕ, Tendsto f atTop atTop ∧
      ∀ᶠ n : ℕ in atTop, ∀ H : UniformHypergraph (Fin n) 3,
        (UniformHypergraph.cliqueSizes H).ncard + f n ≤ n

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

Erdos775.erdos_775.variants.spencer

Solved: stated here without proof.

For graphs, Spencer [Sp71] constructed a graph which contains cliques of at least \(n-\log_2n+O(1)\) different sizes.

theorem erdos_775.variants.spencer :
    ∃ C : ℝ, ∀ n : ℕ, ∃ G : SimpleGraph (Fin n),
      (n : ℝ) - Real.logb 2 (n : ℝ) - C ≤ ((SimpleGraph.cliqueSizes G).ncard : ℝ)

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

Erdos775.erdos_775.variants.moon_moser

Solved: stated here without proof.

For graphs, Spencer [Sp71] constructed a graph which contains cliques of at least \(n-\log_2n+O(1)\) different sizes, which Moon and Moser [MoMo65] showed to be best possible.

theorem erdos_775.variants.moon_moser :
    ∃ C : ℝ, ∀ n : ℕ, ∀ G : SimpleGraph (Fin n),
      ((SimpleGraph.cliqueSizes G).ncard : ℝ) ≤ (n : ℝ) - Real.logb 2 (n : ℝ) + C

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

Sources

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

LeanErdos775.erdos_775 · Erdos775.erdos_775.variants.gao · Erdos775.erdos_775.variants.spencer · Erdos775.erdos_775.variants.moon_moser

TheoremErdős Problem 777#

References: - erdosproblems.com/777 - [Gu83] Guy, R. K., A miscellany of Erdős problems. Amer. Math. Monthly (1983), 118-120. - [AlFr85] Alon, N. and Frankl, P., The maximum number of disjoint pairs in a family of subsets. Graphs Combin. (1985), 13-21. - [ADGS15] Alon, N., Das, S., Glebov, R. and Sudakov, B., Comparable pairs in families of sets. J. Combin. Theory Ser. B (2015), 164-185. arXiv

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

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

Erdos777.erdos_777.parts.i

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

If \(\mathcal{F}\) is a family of subsets of \(\{1,\ldots,n\}\) then we write \(G_{\mathcal{F}}\) for the graph on \(\mathcal{F}\) where \(A\sim B\) if \(A\) and \(B\) are comparable - that is, \(A\subseteq B\) or vice versa.

Is it true that, if \(\epsilon>0\) and \(n\) is sufficiently large, whenever \(m\leq (2-\epsilon)2^{n/2}\) the graph \(G_\mathcal{F}\) has \(<2^{n}\) many edges?

A problem of Daykin and Erdős [Gu83]; here \(m=\lvert\mathcal{F}\rvert\). The answer is yes, which follows from Theorem 1.4 and Corollary 1.5 of Alon, Das, Glebov, and Sudakov [ADGS15].

theorem erdos_777.parts.i :
    ∀ ε : ℝ, 0 < ε → ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n → ∀ 𝓕 : Finset (Finset (Fin n)),
      (𝓕.card : ℝ) ≤ (2 - ε) * (2 : ℝ) ^ ((n : ℝ) / 2) → comparableEdges 𝓕 < 2 ^ n

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

Erdos777.erdos_777.parts.ii

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

If \(\mathcal{F}\) is a family of subsets of \(\{1,\ldots,n\}\) then we write \(G_{\mathcal{F}}\) for the graph on \(\mathcal{F}\) where \(A\sim B\) if \(A\) and \(B\) are comparable - that is, \(A\subseteq B\) or vice versa.

Is it true that if \(G_{\mathcal{F}}\) has \(\geq cm^2\) edges then \(m\ll_c 2^{n/2}\)?

The answer is no, by Alon and Frankl [AlFr85, Example 6.1]: for every \(d\geq 1\) there are families with \(m\gg n^d2^{n/2}\) and at least \(2^{-2d-1}\binom{m}{2}\) comparable pairs. Here \(m=\lvert\mathcal{F}\rvert\), and the question is read as: for every \(c>0\) there is \(C=C(c)\) such that \(m\leq C2^{n/2}\) for all \(n\) and all such families, so the answer is the negation.

theorem erdos_777.parts.ii :
    ¬ ∀ c : ℝ, 0 < c → ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, ∀ 𝓕 : Finset (Finset (Fin n)),
      c * (𝓕.card : ℝ) ^ 2 ≤ comparableEdges 𝓕 →
        (𝓕.card : ℝ) ≤ C * (2 : ℝ) ^ ((n : ℝ) / 2)

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

Erdos777.erdos_777.parts.iii

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

If \(\mathcal{F}\) is a family of subsets of \(\{1,\ldots,n\}\) then we write \(G_{\mathcal{F}}\) for the graph on \(\mathcal{F}\) where \(A\sim B\) if \(A\) and \(B\) are comparable - that is, \(A\subseteq B\) or vice versa.

Is it true that, for any \(\epsilon>0\), there exists some \(\delta>0\) such that if there are \(>m^{2-\delta}\) edges then \(m<(2+\epsilon)^{n/2}\)?

The answer is yes, proved by Alon and Frankl [AlFr85, Theorem 1.4, the case \(k=1\)]. Here \(m=\lvert\mathcal{F}\rvert\).

theorem erdos_777.parts.iii :
    ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧ ∀ n : ℕ, ∀ 𝓕 : Finset (Finset (Fin n)),
      (𝓕.card : ℝ) ^ (2 - δ) < comparableEdges 𝓕 →
        (𝓕.card : ℝ) < (2 + ε) ^ ((n : ℝ) / 2)

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

Sources

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

LeanErdos777.erdos_777.parts.i · Erdos777.erdos_777.parts.ii · Erdos777.erdos_777.parts.iii

TheoremErdős Problem 779#

Reference: erdosproblems.com/779

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

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

Erdos779.erdos_779

Open: stated without proof.

A Conjecture of Marian Deaconescu, see p.120 in https://doi.org/10.2307/2975810

[Needed to index shift in order to avoid trivial case \(n = 0\), where the conjecture is trivially false.]

theorem erdos_779 (n : ℕ) (hn : n ≥ 1): let P := ∏ i ∈ range (n + 1), nth Nat.Prime i
    ∃ p, p.Prime ∧ (P + p).Prime ∧ nth Nat.Prime n < p ∧ p < P

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

Sources

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

LeanErdos779.erdos_779

TheoremErdős Problem 780#

References: - erdosproblems.com/780 - [Er76] Erdős, Paul, Problems and results in combinatorial analysis. Colloquio Internazionale sulle Teorie Combinatorie (Roma, 1973), Tomo II (1976), 3-17. - [Lo78] Lovász, L., Kneser's conjecture, chromatic number, and homotopy. J. Combin. Theory Ser. A (1978), 319-324. - [AFL86] Alon, N. and Frankl, P. and Lovász, L., The chromatic number of Kneser hypergraphs. Trans. Amer. Math. Soc. (1986), 359-370.

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

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

Erdos780.erdos_780

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

Suppose \(n\geq kr+(t-1)(k-1)\) and the edges of the complete \(r\)-uniform hypergraph on \(n\) vertices are \(t\)-coloured. Prove that some colour class must contain \(k\) pairwise disjoint edges.

In other words, this problem asks to determine the chromatic number of the Kneser hypergraph. When \(k=2\) this was conjectured by Kneser and proved by Lovász [Lo78]. The general case was proved by Alon, Frankl, and Lovász [AFL86].

theorem erdos_780 (n k r t : ℕ) (hr : 1 ≤ r) (ht : 1 ≤ t)
    (hn : k * r + (t - 1) * (k - 1) ≤ n) (c : {e : Finset (Fin n) // e.card = r} → Fin t) :
    ∃ (i : Fin t) (e : Fin k → {e : Finset (Fin n) // e.card = r}),
      (∀ j, c (e j) = i) ∧ Pairwise fun a b ↦ Disjoint (e a).1 (e b).1

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

Erdos780.erdos_780.variants.sharp

Textbook result, stated without proof.

This would be best possible: if \(n=kr-1+(t-1)(k-1)\) then decomposing \([n]\) as one set \(X_1\) of size \(kr-1\) and \(t-1\) sets \(X_2,\ldots,X_{t}\) of size \(k-1\), a colouring without \(k\) pairwise disjoint edges is given colouring all subsets of \(X_1\) in colour \(1\) and assigning an edge with colour \(2\leq i\leq t\) if \(i\) is minimal such that \(X_i\) intersects the edge.

theorem erdos_780.variants.sharp (k r t : ℕ) (hk : 1 ≤ k) (hr : 1 ≤ r) (ht : 1 ≤ t) :
    ∃ c : {e : Finset (Fin (k * r - 1 + (t - 1) * (k - 1))) // e.card = r} → Fin t,
      ¬ ∃ (i : Fin t) (e : Fin k → {e : Finset (Fin (k * r - 1 + (t - 1) * (k - 1))) //
          e.card = r}), (∀ j, c (e j) = i) ∧ Pairwise fun a b ↦ Disjoint (e a).1 (e b).1

Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/780.lean, line 61.

Sources

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

LeanErdos780.erdos_780 · Erdos780.erdos_780.variants.sharp

TheoremErdős Problem 781#

References: - erdosproblems.com/781 - [BEF90] Brown, T. C. and Erdős, P. and Freedman, A. R., Quasi-progressions and descending waves. J. Combin. Theory Ser. A (1990), 81-95. - [AlSp89] Alon, N. and Spencer, Joel, Ascending waves. J. Combin. Theory Ser. A (1989), 275-287.

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

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

Erdos781.erdos_781.parts.i

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

Let \(f(k)\) be the minimal \(n\) such that any \(2\)-colouring of \(\{1,\ldots,n\}\) contains a monochromatic \(k\)-term descending wave: a sequence \(x_1\lt \cdots \lt x_k\) such that, for \(1\lt j\lt k\),

\[x_j \geq \frac{x_{j+1}+x_{j-1}}{2}.\]

Estimate \(f(k)\).

Brown, Erdős, and Freedman [BEF90] proved \(k^2-k+1\leq f(k) \leq \frac{k^3-4k+9}{3}\). Resolved by Alon and Spencer [AlSp89] who proved that in fact \(f(k) \gg k^3\), so that \(f(k)\asymp k^3\).

theorem erdos_781.parts.i : (fun k ↦ (f k : ℝ)) =Θ[atTop] fun k ↦ (k : ℝ) ^ 3

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

Erdos781.erdos_781.parts.ii

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

Is it true that \(f(k)=k^2-k+1\) for all \(k\)?

The answer is no, since \(f(k)\gg k^3\) by Alon and Spencer [AlSp89].

theorem erdos_781.parts.ii : ¬ ∀ k ≥ 1, f k = k ^ 2 - k + 1

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

Erdos781.erdos_781.variants.brown_erdos_freedman

Solved: stated here without proof.

Brown, Erdős, and Freedman [BEF90] proved \(k^2-k+1\leq f(k) \leq \frac{k^3-4k+9}{3}\).

theorem erdos_781.variants.brown_erdos_freedman (k : ℕ) (hk : 1 ≤ k) :
    k ^ 2 - k + 1 ≤ f k ∧ (f k : ℚ) ≤ (k ^ 3 - 4 * k + 9) / 3

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

Sources

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

LeanErdos781.erdos_781.parts.i · Erdos781.erdos_781.parts.ii · Erdos781.erdos_781.variants.brown_erdos_freedman

TheoremErdős Problem 782#

References: - erdosproblems.com/782 - [BEF90] Brown, T. C. and Erdős, P. and Freedman, A. R., Quasi-progressions and descending waves. J. Combin. Theory Ser. A 53 (1990), 81-95. - [BFS03] Brown, T. C., Freedman, A. R. and Shiue, P. J.-S., Progressions of squares. Australas. J. Combin. 27 (2003), 187-192. - [BEU26] Bremner, A., Elsholtz, C. and Ulas, M., There are infinitely many Hilbert cubes of dimension 3 in the set of squares. arXiv:2604.05459 (2026). - [CiGr07] Cilleruelo, J. and Granville, A., Lattice points on circles, squares in arithmetic progressions and sumsets of squares. Additive combinatorics (2007), 241-262. - [DiEl12] Dietmann, R. and Elsholtz, C., Hilbert cubes in progression-free sets and in the set of squares II. arXiv:1207.1461 (2012). - [So07] Solymosi, J., Elementary additive combinatorics. Additive combinatorics (2007), 29-38.

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

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

Erdos782.erdos_782.parts.i

Open: stated without proof.

Do the squares contain arbitrarily long quasi-progressions? That is, does there exist some constant \(C>0\) such that, for any \(k\), the squares contain a sequence \(x_1,\ldots,x_k\) where, for some \(d\) and all \(1\leq i\lt k\),

\[x_i+d\leq x_{i+1}\leq x_i+d+C.\]

A question of Brown, Erdős, and Freedman [BEF90]. This is the first question. Here \(C\) and \(d\) are positive integers; \(d\geq 1\) excludes constant sequences.

theorem erdos_782.parts.i :
    ∃ C : ℕ, 0 < C ∧ ∀ k : ℕ, ContainsQuasiProgression {n : ℕ | IsSquare n} C k

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

Erdos782.erdos_782.parts.ii

Open: stated without proof.

Do the squares contain arbitrarily large cubes

\[a+\left\{ \sum_i \epsilon_ib_i : \epsilon_i\in \{0,1\}\right\}?\]

A question of Brown, Erdős, and Freedman [BEF90]. This is the second question. The generators \(b_i\) are nonzero integers, as in [BEU26]. Solymosi [So07] conjectured that the answer is no, and Cilleruelo and Granville [CiGr07] observed that the answer is no conditional on the Bombieri-Lang conjecture.

theorem erdos_782.parts.ii :
    ∀ d : ℕ, ∃ (a : ℤ) (b : Fin d → ℤ),
      (∀ i, b i ≠ 0) ∧ hilbertCube a b ⊆ {n : ℤ | IsSquare n}

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

Erdos782.erdos_782.variants.no_four_term_ap

Solved: stated here without proof.

It is a classical fact that the squares do not contain arithmetic progressions of length \(4\).

theorem erdos_782.variants.no_four_term_ap :
    Set.IsAPOfLengthFree {n : ℕ | IsSquare n} 4

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

Erdos782.erdos_782.variants.dietmann_elsholtz

Solved: stated here without proof.

Dietmann and Elsholtz [DiEl12, Theorem 1] proved that, for all sufficiently large \(N\), if \(a_0\geq 0\) and \(b_1,\ldots,b_d\) are distinct positive integers such that the Hilbert cube \(a_0+\{0,b_1\}+\cdots+\{0,b_d\}\) consists of squares in \([1,N]\), then \(d\leq 7\log\log N\).

theorem erdos_782.variants.dietmann_elsholtz :
    ∃ N₀ : ℕ, ∀ N ≥ N₀, ∀ (d : ℕ) (a₀ : ℤ) (b : Fin d → ℤ),
      0 ≤ a₀ → Function.Injective b → (∀ i, 0 < b i) →
      hilbertCube a₀ b ⊆ {n : ℤ | IsSquare n ∧ 1 ≤ n ∧ n ≤ N} →
        (d : ℝ) ≤ 7 * Real.log (Real.log N)

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

Sources

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

LeanErdos782.erdos_782.parts.i · Erdos782.erdos_782.parts.ii · Erdos782.erdos_782.variants.no_four_term_ap · Erdos782.erdos_782.variants.dietmann_elsholtz

TheoremErdős Problem 785#

References: - erdosproblems.com/785 - [ChFa10] Fang, Jin-Hui and Chen, Yong-Gao, On additive complements. Proc. Amer. Math. Soc. (2010), 1923-1927. - [ChFa11] Chen, Yong-Gao and Fang, Jin-Hui, On additive complements. II. Proc. Amer. Math. Soc. (2011), 881-883. - [ChFa14] Fang, Jin-Hui and Chen, Yong-Gao, On additive complements. III. J. Number Theory (2014), 83-91. - [ChFa15] Chen, Yong-Gao and Fang, Jin-Hui, On a conjecture of Sárközy and Szemerédi. Acta Arith. (2015), 47-58. - [Da64] Danzer, L., Über eine Frage von G. Hanani aus der additiven Zahlentheorie. J. Reine Angew. Math. (1964), 392-394. - [Er57] Erdős, Paul, Some unsolved problems. Michigan Math. J. (1957), 291-300. - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Na59] Narkiewicz, Władysław, Remarks on a conjecture of Hanani in additive number theory. Colloq. Math. (1959/60), 161-165. - [Ru17] Ruzsa, Imre Z., Exact additive complements. Q. J. Math. (2017), 227-235. - [SaSz94] Sárközy, A. and Szemerédi, E., On a problem in additive number theory. Acta Math. Hungar. (1994), 237-245.

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

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

Erdos785.erdos_785

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

Let \(A,B\subseteq \mathbb{N}\) be infinite sets of positive integers such that \(A+B\) contains all large integers. Let \(A(x)=\lvert A\cap [1,x]\rvert\) and similarly for \(B(x)\). Is it true that if \(A(x)B(x)\sim x\) then

\[A(x)B(x)-x\to \infty\]

as \(x\to \infty\)?

A conjecture of Erdős and Danzer. The answer is yes, proved by Sárközy and Szemerédi [SaSz94], who actually proved that it is impossible for

\[A(x)B(x)-x=o(A(x)).\]

This was formalized in Lean by van Doorn using Aristotle.

theorem erdos_785 :
    ∀ A B : Set ℕ, A.Infinite → B.Infinite → 0 ∉ A → 0 ∉ B → IsExactAdditiveComplement A B →
      Tendsto (fun x : ℕ => (counting A x * counting B x : ℝ) - (x : ℝ)) atTop atTop

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

Erdos785.erdos_785.variants.danzer

Solved: stated here without proof.

Danzer [Da64] proved that exact additive complements exist (Hanani had earlier conjectured they do not exist, as reported in [Er57] and [Er61]).

theorem erdos_785.variants.danzer :
    ∃ A B : Set ℕ, A.Infinite ∧ B.Infinite ∧ 0 ∉ A ∧ 0 ∉ B ∧ IsExactAdditiveComplement A B

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

Erdos785.erdos_785.variants.sarkozy_szemeredi

Solved: stated here without proof.

Sárközy and Szemerédi [SaSz94] proved that it is impossible for

\[A(x)B(x)-x=o(A(x)).\]

theorem erdos_785.variants.sarkozy_szemeredi (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite)
    (hA₀ : 0 ∉ A) (hB₀ : 0 ∉ B) (h : IsExactAdditiveComplement A B) :
    ¬ (fun x : ℕ => (counting A x * counting B x : ℝ) - (x : ℝ)) =o[atTop]
      (fun x : ℕ => (counting A x : ℝ))

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

Erdos785.erdos_785.variants.chen_fang

Solved: stated here without proof.

Chen and Fang [ChFa15] proved \(A(x)B(x)-x\ll \min(A(x),B(x))^c\) cannot hold for any constant \(c>0\). In particular \(A(x)B(x)-x\ll A(x)^c\) cannot hold when \(A\) is the sparser of the two sets.

theorem erdos_785.variants.chen_fang (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite)
    (hA₀ : 0 ∉ A) (hB₀ : 0 ∉ B) (h : IsExactAdditiveComplement A B) (c : ℝ) (hc : 0 < c) :
    ¬ (fun x : ℕ => (counting A x * counting B x : ℝ) - (x : ℝ)) =O[atTop]
      (fun x : ℕ => (min (counting A x) (counting B x) : ℝ) ^ c)

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

Erdos785.erdos_785.variants.narkiewicz

Solved: stated here without proof.

Narkiewicz [Na59] proved that, under the given assumptions (and perhaps swapping \(A\) and \(B\)) we must have \(A(2x)/A(x)\to 1\) and \(B(2x)/B(x)\to 2\).

theorem erdos_785.variants.narkiewicz (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite)
    (hA₀ : 0 ∉ A) (hB₀ : 0 ∉ B) (h : IsExactAdditiveComplement A B) :
    (Tendsto (fun x : ℕ => (counting A (2 * x) : ℝ) / (counting A x : ℝ)) atTop (𝓝 1) ∧
      Tendsto (fun x : ℕ => (counting B (2 * x) : ℝ) / (counting B x : ℝ)) atTop (𝓝 2)) ∨
    (Tendsto (fun x : ℕ => (counting B (2 * x) : ℝ) / (counting B x : ℝ)) atTop (𝓝 1) ∧
      Tendsto (fun x : ℕ => (counting A (2 * x) : ℝ) / (counting A x : ℝ))
        atTop (𝓝 2))

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

Erdos785.erdos_785.variants.ruzsa_upper_bound

Solved: stated here without proof.

Ruzsa [Ru17] has constructed, for any function \(w(x)\to \infty\), such a pair of sets with

\[A(x)B(x)-x\lt w(x)\]

for infinitely many \(x\).

theorem erdos_785.variants.ruzsa_upper_bound (w : ℕ → ℝ) (hw : Tendsto w atTop atTop) :
    ∃ A B : Set ℕ, A.Infinite ∧ B.Infinite ∧ 0 ∉ A ∧ 0 ∉ B ∧ IsExactAdditiveComplement A B ∧
      ∃ᶠ x : ℕ in atTop, (counting A x * counting B x : ℝ) - (x : ℝ) < w x

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

Erdos785.erdos_785.variants.ruzsa_lower_bound

Solved: stated here without proof.

Ruzsa [Ru17] proves that, if \(a^*(x)=\max A \cap [1,x]\) and \(A\) and \(B\) satisfy the conditions in the problem then (after possibly changing the roles of \(A\) and \(B\))

\[A(x)B(x)-x > (1-o(1))\frac{a^*(x)}{A(x)}.\]

theorem erdos_785.variants.ruzsa_lower_bound (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite)
    (hA₀ : 0 ∉ A) (hB₀ : 0 ∉ B) (h : IsExactAdditiveComplement A B) :
    (∀ ε > (0 : ℝ), ∀ᶠ x : ℕ in atTop,
        (1 - ε) * (aStar A x : ℝ) / (counting A x : ℝ)
          < (counting A x * counting B x : ℝ) - (x : ℝ)) ∨
    (∀ ε > (0 : ℝ), ∀ᶠ x : ℕ in atTop,
        (1 - ε) * (aStar B x : ℝ) / (counting B x : ℝ)
          < (counting A x * counting B x : ℝ) - (x : ℝ))

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

Erdos785.erdos_785.variants.chen_fang_limsup

Solved: stated here without proof.

Chen and Fang [ChFa10] proved the stronger statement that \(A(x)B(x)-x\to \infty\) if \(A\) and \(B\) are infinite sets such that \(A+B\) contains all large integers and

\[\limsup_{x\to \infty}\frac{A(x)B(x)}{x}\lt \frac{5}{4}.\]

They later [ChFa14] improved \(5/4\) to \(3-\sqrt{3}\approx 1.268\).

theorem erdos_785.variants.chen_fang_limsup (A B : Set ℕ) (hA : A.Infinite) (hB : B.Infinite)
    (hA₀ : 0 ∉ A) (hB₀ : 0 ∉ B) (h : IsAdditiveComplement A B)
    (hlim : limsup (fun x : ℕ => ((counting A x * counting B x : ℝ) / (x : ℝ) : EReal)) atTop
      < ((3 - Real.sqrt 3 : ℝ) : EReal)) :
    Tendsto (fun x : ℕ => (counting A x * counting B x : ℝ) - (x : ℝ)) atTop atTop

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

Erdos785.erdos_785.variants.chen_conjecture

Open: stated without proof.

Chen conjectures that this should be true with \(3/2\).

theorem erdos_785.variants.chen_conjecture :
    ∀ A B : Set ℕ, A.Infinite → B.Infinite → 0 ∉ A → 0 ∉ B → IsAdditiveComplement A B →
      limsup (fun x : ℕ => ((counting A x * counting B x : ℝ) / (x : ℝ) : EReal)) atTop
          < ((3 / 2 : ℝ) : EReal) →
        Tendsto (fun x : ℕ => (counting A x * counting B x : ℝ) - (x : ℝ)) atTop atTop

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

Erdos785.erdos_785.variants.chen_fang_sharp

Solved: stated here without proof.

This is sharp, as Chen and Fang [ChFa11] also proved that there exist such \(A\) and \(B\) with

\[\limsup_{x\to \infty}\frac{A(x)B(x)}{x}=\frac{3}{2}\]

for which \(A(x)B(x)-x=1\) for infinitely many \(x\).

theorem erdos_785.variants.chen_fang_sharp :
    ∃ A B : Set ℕ, A.Infinite ∧ B.Infinite ∧ 0 ∉ A ∧ 0 ∉ B ∧ IsAdditiveComplement A B ∧
      limsup (fun x : ℕ => ((counting A x * counting B x : ℝ) / (x : ℝ) : EReal)) atTop
          = ((3 / 2 : ℝ) : EReal) ∧
      ∃ᶠ x : ℕ in atTop, (counting A x * counting B x : ℝ) - (x : ℝ) = 1

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

Sources

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

LeanErdos785.erdos_785 · Erdos785.erdos_785.variants.danzer · Erdos785.erdos_785.variants.sarkozy_szemeredi · Erdos785.erdos_785.variants.chen_fang · Erdos785.erdos_785.variants.narkiewicz · Erdos785.erdos_785.variants.ruzsa_upper_bound · Erdos785.erdos_785.variants.ruzsa_lower_bound · Erdos785.erdos_785.variants.chen_fang_limsup · Erdos785.erdos_785.variants.chen_conjecture · Erdos785.erdos_785.variants.chen_fang_sharp

TheoremErdős Problem 786#

Reference: erdosproblems.com/786

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

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

Erdos786.erdos_786.parts.i

Open: stated without proof.

Let \(\epsilon > 0\). Is there some set \(A\subset\mathbb{N}\) of density \(> 1 - \epsilon\) such that \(a_1\cdots a_r = b_1\cdots b_s\) with \(a_i, b_j\in A\) can only hold when \(r = s\)?

theorem erdos_786.parts.i : ∀ ε > 0, ε ≤ 1 →
    ∃ (A : Set ℕ) (δ : ℝ), 0 ∉ A ∧ 1 - ε < δ ∧ A.HasDensity δ ∧ A.IsMulCardSet

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

Erdos786.erdos_786.parts.ii

Open: stated without proof.

Is there some set \(A\subset\{1, ..., N\}\) of size \(\geq (1 - o(1))N\) such that \(a_1\cdots a_r = b_1\cdots b_s\) with \(a_i, b_j\in A\) can only hold when \(r = s\)?

theorem erdos_786.parts.ii :
    ∃ (A : ℕ → Set ℕ) (f : ℕ → ℝ) (_ : f =o[atTop] (1 : ℕ → ℝ)),
    ∀ N, A N ⊆ Set.Icc 1 (N + 1) ∧ (1 - f N) * N ≤ (A N).ncard ∧ (A N).IsMulCardSet

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

Erdos786.erdos_786.parts.i.example

Textbook result, proved here.

An example of such a set with density \(\frac 1 4\) is given by the integers \(\equiv 2\pmod{4}\)

theorem erdos_786.parts.i.example (A : Set ℕ) (hA : A = { n | n % 4 = 2 }) :
    A.HasDensity (1 / 4) ∧ A.IsMulCardSet

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

Erdos786.erdos_786.parts.i.selfridge

Solved: stated here without proof.

Let \(\epsilon > 0\) be given. Then, for a sufficiently large prime p, take the sequence of consecutive primes \(p_1 < \cdots < p_k\) such that

\[ \sum_{i=1}^k \frac{1}{p_i} < 1 < \sum_{i=1}^{k + 1} \frac{1}{p_i}, \]

and let \(A\) be the set of all naturals divisible by exactly one of \(p_1, ..., p_k\) (with multiplicity \(1\)). Then \(A\) has density \(> \frac{1}{e} - \epsilon\) and has the property that \(a_1\cdots a_r = b_1\cdots b_s\) with \(a_i, b_j\in A\) can only hold when \(r = s\).

theorem erdos_786.parts.i.selfridge (ε : ℝ) (hε : 0 < ε ∧ ε < 1 / rexp 1) :
    ∀ᶠ (p : ℕ) in atTop, p.Prime → ∃ k,
      ∑ q ∈ consecutivePrimesFrom p k, (1 : ℝ) / q < 1 ∧
        1 < ∑ q ∈ consecutivePrimesFrom p (k + 1), (1 : ℝ) / q ∧
          letI A := { n | ∑ q ∈ consecutivePrimesFrom p k, (n : ℕ).factorization q = 1 }
          ∃ δ, 1 / rexp 1 - ε < δ ∧ A.HasDensity δ ∧ A.IsMulCardSet

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

Sources

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

LeanErdos786.erdos_786.parts.i · Erdos786.erdos_786.parts.ii · Erdos786.erdos_786.parts.i.example · Erdos786.erdos_786.parts.i.selfridge

TheoremErdős Problem 787#

References: - erdosproblems.com/787 - [Be25] Beker, A., The Erdős-Moser sum-free set problem via improved bounds for \(k\)-configurations. arXiv:2501.10203 (2025). - [Ch71] Choi, S. L. G., On a combinatorial problem in number theory. Proc. London Math. Soc. (3) (1971), 629-642. - [Er65] Erdős, P., Extremal problems in number theory. Proc. Sympos. Pure Math., Vol. VIII (1965), 181-189. PDF - [Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138. PDF - [Ru05] Ruzsa, Imre Z., Sum-avoiding subsets. Ramanujan J. (2005), 77-82. - [Sa21] Sanders, Tom, The Erdős-Moser sum-free set problem. Canad. J. Math. (2021), 63-107.

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

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

Erdos787.erdos_787

Open: stated without proof.

Let \(g(n)\) be maximal such that given any set \(A\subset \mathbb{R}\) with \(\lvert A\rvert=n\) there exists some \(B\subseteq A\) of size \(\lvert B\rvert\geq g(n)\) such that \(b_1+b_2\not\in A\) for all \(b_1\neq b_2\in B\).

Estimate \(g(n)\).

theorem erdos_787 : (fun n ↦ (g ℝ n : ℝ)) =Θ[atTop] erdos_787.answer

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

Erdos787.erdos_787.variants.integers

Solved: stated here without proof.

This function was considered by Erdős and Moser. Choi observed that, without loss of generality, one can assume that \(A\subset \mathbb{Z}\).

Here this means that sets of integers give the same value \(g(n)\) as sets of reals.

theorem erdos_787.variants.integers (n : ℕ) : g ℤ n = g ℝ n

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

Erdos787.erdos_787.variants.klarner

Solved: stated here without proof.

Klarner proved \(g(n) \gg \log n\) (indeed, a greedy construction suffices).

theorem erdos_787.variants.klarner :
    ∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, c * Real.log n ≤ (g ℝ n : ℝ)

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

Erdos787.erdos_787.variants.choi

Solved: stated here without proof.

Choi [Ch71] proved \(g(n) \ll n^{2/5+o(1)}\).

Here this means that \(g(n) \leq n^{2/5+\varepsilon}\) for every \(\varepsilon > 0\) and all large \(n\), as in [Er73, p. 130].

theorem erdos_787.variants.choi :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (g ℝ n : ℝ) ≤ (n : ℝ) ^ (2 / 5 + ε)

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

Erdos787.erdos_787.variants.sanders

Solved: stated here without proof.

The current best bounds known are

\[(\log n)^{1+c} \ll g(n) \ll \exp(\sqrt{\log n})\]

for some constant \(c>0\), the lower bound due to Sanders [Sa21] and the upper bound due to Ruzsa [Ru05].

This is the lower bound.

theorem erdos_787.variants.sanders :
    ∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, Real.log n ^ (1 + c) ≤ (g ℝ n : ℝ)

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

Erdos787.erdos_787.variants.ruzsa

Solved: stated here without proof.

The current best bounds known are

\[(\log n)^{1+c} \ll g(n) \ll \exp(\sqrt{\log n})\]

for some constant \(c>0\), the lower bound due to Sanders [Sa21] and the upper bound due to Ruzsa [Ru05].

This is the upper bound. [Ru05] proves it in the form \(\exp(O(\sqrt{\log n}))\), which is the form stated here.

theorem erdos_787.variants.ruzsa :
    ∃ C > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (g ℝ n : ℝ) ≤ Real.exp (C * Real.sqrt (Real.log n))

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

Erdos787.erdos_787.variants.beker

Solved: stated here without proof.

Beker [Be25] has proved

\[(\log n)^{1+\tfrac{1}{68}+o(1)} \ll g(n).\]

Here this means that \(g(n) \geq (\log n)^{1+c}\) for every \(c < 1/68\) and all large \(n\) [Be25, Theorem 1.2].

theorem erdos_787.variants.beker :
    ∀ c : ℝ, 0 < c → c < 1 / 68 → ∀ᶠ n : ℕ in atTop, Real.log n ^ (1 + c) ≤ (g ℝ n : ℝ)

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

Sources

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

LeanErdos787.erdos_787 · Erdos787.erdos_787.variants.integers · Erdos787.erdos_787.variants.klarner · Erdos787.erdos_787.variants.choi · Erdos787.erdos_787.variants.sanders · Erdos787.erdos_787.variants.ruzsa · Erdos787.erdos_787.variants.beker

TheoremErdős Problem 789#

In this problem, a function \(h : \mathbb{N} \to\mathbb{N}\) is defined maximally by some counting property.

The problem asks to estimate \(h(n)\). This has been interpreted here as asking for \(\Theta(h(n))\). The principal version includes the unknown function erdos_789.answer.

Straus [Str66] proved that \(h(n) \ll \sqrt{n}\). Erdős [Er62c] and Choi [Ch74b] proved that \((n\log(n))^{1/3} \ll h(n)\). Korsky [Ko26] improved this to \(h(n) \gg \sqrt{n\log\log n/\log n}\). The variants record these bounds and the open question whether \(h(n) = \Theta(\sqrt{n})\). The file proves Korsky's bound, following [Ko26], and derives from it the Erdős–Choi bound and \(h(n) \neq O((n\log(n))^{1/3})\).

References: - erdosproblems.com/789 - [Str66] Straus, E. G., On a problem in combinatorial number theory. J. Math. Sci. (1966), 77--80. - [Er62c] Erdős, Pál, Some remarks on number theory. {III}. Mat. Lapok (1962), 28--38. - [Ch74b] Choi, S. L. G., On an extremal problem in number theory. J. Number Theory (1974), 105--111. - [Ko26] Korsky, S., A near-square-root bound for an additive problem of Erdős and Straus (2026). Proof claim.

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

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

Erdos789.erdos_789

Open: stated without proof.

Let \(h(n)\) be maximal such that if \(A\subseteq \mathbb{Z}\) with \(\lvert A\rvert=n\) then there is \(B\subseteq A\) with \(\lvert B\rvert \geq h(n)\) such that if \(a_1+\cdots+a_r=b_1+\cdots+b_s\) with \(a_i,b_i\in B\) then \(r=s\).

Estimate \(h(n)\).

theorem erdos_789 :
    (fun n ↦ (subsetSumThreshold n : ℝ)) =Θ[atTop] erdos_789.answer

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

Erdos789.erdos_789.variants.sq

Open: stated without proof.

Let \(h(n)\) be maximal such that if \(A\subseteq \mathbb{Z}\) with \(\lvert A\rvert=n\) then there is \(B\subseteq A\) with \(\lvert B\rvert \geq h(n)\) such that if \(a_1+\cdots+a_r=b_1+\cdots+b_s\) with \(a_i,b_i\in B\) then \(r=s\).

Is \(h(n) = \Theta(\sqrt{n})\)?

theorem erdos_789.variants.sq :
    (fun n ↦ (subsetSumThreshold n : ℝ)) =Θ[atTop] fun n ↦ √n

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

Erdos789.erdos_789.variants.isBigO_sq

Solved: stated here without proof.

Straus [Str66] proved that \(h(n) \ll \sqrt{n}\).

theorem erdos_789.variants.isBigO_sq :
    (fun n ↦ (subsetSumThreshold n : ℝ)) =O[atTop] fun n ↦ √n

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

Erdos789.erdos_789.variants.sq_isBigO

Open: stated without proof.

By the solved variant erdos_789.variants.isBigO_sq, in order to prove erdos_789.variants.sq it suffices to show \(\sqrt{n}=O(h(n))\).

theorem erdos_789.variants.sq_isBigO :
    (fun n : ℕ ↦ √n) =O[atTop] fun n ↦ (subsetSumThreshold n : ℝ)

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

Erdos789.erdos_789.variants.sqrt_loglog_div_log_isBigO

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/57a0dc60e2cc245b69870647d122fb851f72d8e4/FormalConjectures/ErdosProblems/789.lean#L907.

Korsky [Ko26] proved that \(h(n) \gg \sqrt{n\log\log n/\log n}\).

theorem erdos_789.variants.sqrt_loglog_div_log_isBigO :
    (fun n : ℕ ↦ √(n * Real.log (Real.log n) / Real.log n)) =O[atTop]
      fun n ↦ (subsetSumThreshold n : ℝ)

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

Erdos789.erdos_789.variants.cube_root_linearithmic_isBigO

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/57a0dc60e2cc245b69870647d122fb851f72d8e4/FormalConjectures/ErdosProblems/789.lean#L973.

Erdős [Er62c] and Choi [Ch74b] proved that \((n\log(n))^{1/3}\ll h(n)\). This also follows from erdos_789.variants.sqrt_loglog_div_log_isBigO.

theorem erdos_789.variants.cube_root_linearithmic_isBigO :
    (fun n : ℕ ↦ (n * Real.log n) ^ ((1 : ℝ) / 3)) =O[atTop]
      fun n ↦ (subsetSumThreshold n : ℝ)

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

Erdos789.erdos_789.variants.isBigO_cube_root_linearithmic

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/57a0dc60e2cc245b69870647d122fb851f72d8e4/FormalConjectures/ErdosProblems/789.lean#L981.

It is not true that \(h(n) = O((n\log(n))^{1/3})\). This follows from erdos_789.variants.sqrt_loglog_div_log_isBigO [Ko26].

theorem erdos_789.variants.isBigO_cube_root_linearithmic :
    ¬ (fun n ↦ (subsetSumThreshold n : ℝ)) =O[atTop]
      fun n ↦ (n * Real.log n) ^ ((1 : ℝ) / 3)

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

Erdos789.erdos_789.variants.cube_root_linearithmic

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/57a0dc60e2cc245b69870647d122fb851f72d8e4/FormalConjectures/ErdosProblems/789.lean#L994.

It is not true that \(h(n) = \Theta((n\log(n))^{1/3})\). This follows from erdos_789.variants.isBigO_cube_root_linearithmic.

theorem erdos_789.variants.cube_root_linearithmic :
    ¬ (fun n ↦ (subsetSumThreshold n : ℝ)) =Θ[atTop]
      fun n ↦ (n * Real.log n) ^ ((1 : ℝ) / 3)

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

Sources

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

LeanErdos789.erdos_789 · Erdos789.erdos_789.variants.sq · Erdos789.erdos_789.variants.isBigO_sq · Erdos789.erdos_789.variants.sq_isBigO · Erdos789.erdos_789.variants.sqrt_loglog_div_log_isBigO · Erdos789.erdos_789.variants.cube_root_linearithmic_isBigO · Erdos789.erdos_789.variants.isBigO_cube_root_linearithmic · Erdos789.erdos_789.variants.cube_root_linearithmic

TheoremErdős Problem 793#

References: - erdosproblems.com/793 - [Er38] Erdős, P., On sequences of integers no one of which divides the product of two others and on related problems. Tomsk. Gos. Univ. Ucen Zap. (1938), 74-82. - [Er69] Erdős, Paul, Some applications of graph theory to number theory. The Many Facets of Graph Theory (Proc. Conf., Western Mich. Univ., Kalamazoo, Mich., 1968) (1969), 77-82. - [Er70b] Erdős, P., Some applications of graph theory to number theory. Proc. Second Chapel Hill Conf. on Combinatorial Mathematics and its Applications (Univ. North Carolina, Chapel Hill, N.C., 1970) (1970), 136-145.

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

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

Erdos793.erdos_793

Solved: stated here without proof.

Let \(F(n)\) be the maximum possible size of a subset \(A \subseteq \{1, \ldots, n\}\) such that \(a \nmid bc\) whenever \(a, b, c \in A\) with \(a \neq b\) and \(a \neq c\). Is there a constant \(c\) such that

\[F(n) = \pi(n) + (c + o(1)) n^{2/3} (\log n)^{-2}?\]

A problem of Erdős [Er69, Er70b], who proved in [Er38] that \(F(n) = \pi(n) + O(n^{2/3} (\log n)^{-2})\). The answer is yes, with \(c = 27/2\): this was proved by GPT-5.6 Sol (prompted by Chojecki), refining the argument of [Er38]; see erdos_793.variants.constant.

theorem erdos_793 :
    ∃ c : ℝ, Tendsto (fun n : ℕ ↦ ((F n : ℝ) - Nat.primeCounting n) /
      ((n : ℝ) ^ ((2 : ℝ) / 3) / (log n) ^ 2)) atTop (𝓝 c)

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

Erdos793.erdos_793.variants.constant

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

The constant in Problem 793 is \(c = 27/2\), i.e.

\[F(n) = \pi(n) + \left(\frac{27}{2} + o(1)\right) \frac{n^{2/3}}{(\log n)^2}.\]

Formalised by van Doorn and Aristotle, following the proof of GPT-5.6 Sol.

theorem erdos_793.variants.constant :
    Tendsto (fun n : ℕ ↦ ((F n : ℝ) - Nat.primeCounting n) /
      ((n : ℝ) ^ ((2 : ℝ) / 3) / (log n) ^ 2)) atTop (𝓝 (27 / 2))

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

Sources

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

LeanErdos793.erdos_793 · Erdos793.erdos_793.variants.constant

TheoremErdős Problem 794#

References: - erdosproblems.com/794 - [Er69] Erdős, Paul, Some applications of graph theory to number theory. The Many Facets of Graph Theory (Proc. Conf., Western Mich. Univ., Kalamazoo, Mich., 1968) (1969), 77-82. - [FrFu84] Frankl, P. and Füredi, Z., An exact result for \(3\)-graphs. Discrete Math. (1984), 323-328.

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

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

Erdos794.erdos_794

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

Is it true that every \(3\)-uniform hypergraph on \(3n\) vertices with at least \(n^3+1\) edges must contain either a subgraph on \(4\) vertices with \(3\) edges or a subgraph on \(5\) vertices with \(7\) edges?

Harris has provided the following simple counterexample to the problem as stated: the \(3\)-uniform graph on \(\{1,\ldots,9\}\) with \(28\) edges, formed by taking \(27\) edges by choosing one element each from \(\{1,2,3\},\{4,5,6\},\{7,8,9\}\), and then adding the edge \(\{1,2,3\}\).

theorem erdos_794 :
    ¬ ∀ n : ℕ, ∀ H : Finset (Finset (Fin (3 * n))), H.IsUniform 3 →
      n ^ 3 + 1 ≤ H.card → H.ContainsSubgraph 4 3 ∨ H.ContainsSubgraph 5 7

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

Erdos794.erdos_794.variants.balogh

Proved here.

Balogh has observed that this problem is probably misstated by Erdős - indeed, every graph with \(5\) vertices spanning \(7\) edges contains a graph on \(4\) vertices spanning \(3\) edges, so the second condition can be dropped.

theorem erdos_794.variants.balogh {V : Type*} [DecidableEq V] (H : Finset (Finset V))
    (hH : H.IsUniform 3) (h : H.ContainsSubgraph 5 7) : H.ContainsSubgraph 4 3

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

Erdos794.erdos_794.variants.harris

Proved here.

Harris has provided the following simple counterexample to the problem as stated: the \(3\)-uniform graph on \(\{1,\ldots,9\}\) with \(28\) edges, formed by taking \(27\) edges by choosing one element each from \(\{1,2,3\},\{4,5,6\},\{7,8,9\}\), and then adding the edge \(\{1,2,3\}\).

theorem erdos_794.variants.harris :
    harrisHypergraph.IsUniform 3 ∧ harrisHypergraph.card = 28 ∧
      ¬ harrisHypergraph.ContainsSubgraph 4 3 ∧ ¬ harrisHypergraph.ContainsSubgraph 5 7

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

Erdos794.erdos_794.variants.frankl_furedi

Solved: stated here without proof.

This problem is then now asking how many edges a \(3\)-uniform hypergraph can have before it contains \(K_4\) minus an edge, and whether the critical edge density is \(2/9\). In fact there is a construction of Frankl and Füredi [FrFu84] showing it must be at least \(2/7\), which is the conjectured truth (although Turán conjectured before [Er69] that the edge density was \(1/4\), and so likely there is simply a typo in this problem's statement).

theorem erdos_794.variants.frankl_furedi (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ n : ℕ in atTop, ∃ H : Finset (Finset (Fin n)), H.IsUniform 3 ∧
      ¬ H.ContainsSubgraph 4 3 ∧ (2 / 7 - ε) * (n.choose 3 : ℝ) ≤ (H.card : ℝ)

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

Sources

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

LeanErdos794.erdos_794 · Erdos794.erdos_794.variants.balogh · Erdos794.erdos_794.variants.harris · Erdos794.erdos_794.variants.frankl_furedi

TheoremErdős Problem 796#

Reference: erdosproblems.com/796

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

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

Erdos796.erdos_796

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

Let \(k\geq 2\) and let \(g_k(n)\) be the largest possible size of \(A\subseteq \{1,\ldots,n\}\) such that every \(m\) has \(\lt k\) solutions to \(m=a_1a_2\) with \(a_1\lt a_2\in A\). Is it true that

\[g_3(n)=\frac{\log\log n}{\log n}n+(c+o(1))\frac{n}{\log n}\]

for some constant \(c\)?

The answer is yes: the rescaled error normalizedError converges.

theorem erdos_796 :
    ∃ c : ℝ, Tendsto normalizedError atTop (𝓝 c)

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

Sources

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

LeanErdos796.erdos_796

TheoremErdős Problem 798#

References: - erdosproblems.com/798 - [Al91] Alon, N., Economical coverings of sets of lattice points. Geom. Funct. Anal. (1991), 224-230.

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

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

Erdos798.erdos_798

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

Let \(t(n)\) be the minimum number of points in \(\{1,\ldots,n\}^2\) such that the \(\binom{t}{2}\) lines determined by these points cover all points in \(\{1,\ldots,n\}^2\).

Estimate \(t(n)\). In particular, is it true that \(t(n)=o(n)\)?

A problem of Erdős and Purdy, who proved \(t(n) \gg n^{2/3}\).

Resolved by Alon [Al91] who proved \(t(n) \ll n^{2/3}\log n\).

theorem erdos_798 :
    (fun n : ℕ => (t n : ℝ)) =o[atTop] (fun n : ℕ => (n : ℝ))

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

Erdos798.erdos_798.variants.lower_bound

Solved: stated here without proof.

A problem of Erdős and Purdy, who proved \(t(n) \gg n^{2/3}\).

theorem erdos_798.variants.lower_bound :
    (fun n : ℕ => (n : ℝ) ^ (2 / 3 : ℝ)) =O[atTop] (fun n : ℕ => (t n : ℝ))

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

Erdos798.erdos_798.variants.upper_bound

Solved: stated here without proof.

Resolved by Alon [Al91] who proved \(t(n) \ll n^{2/3}\log n\).

theorem erdos_798.variants.upper_bound :
    (fun n : ℕ => (t n : ℝ)) =O[atTop]
      (fun n : ℕ => (n : ℝ) ^ (2 / 3 : ℝ) * Real.log n)

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

Sources

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

LeanErdos798.erdos_798 · Erdos798.erdos_798.variants.lower_bound · Erdos798.erdos_798.variants.upper_bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.