Erdős Problem 800 to Erdős Problem 823

TheoremErdős Problem 800#

References: - erdosproblems.com/800 - [Al94] Alon, N., Subdivided graphs have linear Ramsey numbers. J. Graph Theory (1994), 343-347.

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

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

Erdos800.erdos_800

Solved: stated here without proof.

If \(G\) is a graph on \(n\) vertices which has no two adjacent vertices of degree \(\geq 3\) then

\[R(G)\ll n,\]

where the implied constant is absolute.

A problem of Burr and Erdős. Solved in the affirmative by Alon [Al94].

theorem erdos_800 :
    ∃ C > (0 : ℝ), ∀ (n : ℕ) (V : Type) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj],
      Fintype.card V = n →
      (∀ u v, G.Adj u v → ¬(3 ≤ G.degree u ∧ 3 ≤ G.degree v)) →
      (SimpleGraph.diagonalGraphRamsey G : ℝ) ≤ C * n

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

Sources

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

LeanErdos800.erdos_800

TheoremErdős Problem 801#

References: - erdosproblems.com/801 - [Er79g] Erdős, Paul, Some old and new problems in various branches of combinatorics. Proceedings of the Tenth Southeastern Conference on Combinatorics, Graph Theory and Computing (Florida Atlantic Univ., Boca Raton, Fla., 1979) (1979), 19-37. - [Al96b] Alon, Noga, Independence numbers of locally sparse graphs and a Ramsey type problem. Random Structures Algorithms (1996), 271-278.

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

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

Erdos801.erdos_801

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

If \(G\) is a graph on \(n\) vertices containing no independent set on \(>n^{1/2}\) vertices then there is a set of \(\leq n^{1/2}\) vertices containing \(\gg n^{1/2}\log n\) edges.

Proved by Alon [Al96b].

theorem erdos_801 : ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
    ∀ G : SimpleGraph (Fin n), (G.indepNum : ℝ) ≤ √n →
      ∃ S : Finset (Fin n), (S.card : ℝ) ≤ √n ∧
        c * √n * Real.log n ≤ (G.induce (S : Set (Fin n))).edgeSet.ncard

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

Sources

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

LeanErdos801.erdos_801

TheoremErdős Problem 802#

References: - erdosproblems.com/802 - [AEKS81] Ajtai, M. and Erdős, P. and Komlós, J. and Szemerédi, E., On Turán's theorem for sparse graphs. Combinatorica (1981), 313-317. - [AKS80] Ajtai, Miklós and Komlós, János and Szemerédi, Endre, A note on Ramsey numbers. J. Combin. Theory Ser. A (1980), 354-360. - [Al96b] Alon, Noga, Independence numbers of locally sparse graphs and a Ramsey type problem. Random Structures Algorithms (1996), 271-278. - [Sh95] Shearer, James B., On the independence number of sparse graphs. Random Structures Algorithms (1995), 269-271.

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

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

Erdos802.erdos_802

Open: stated without proof.

Is it true that any \(K_r\)-free graph on \(n\) vertices with average degree \(t\) contains an independent set on

\[\gg_r \frac{\log t}{t}n\]

many vertices?

A conjecture of Ajtai, Erdős, Komlós, and Szemerédi [AEKS81].

theorem erdos_802 : ∀ r : ℕ, ∃ c > (0 : ℝ), ∀ n : ℕ, ∀ G : SimpleGraph (Fin n),
    G.CliqueFree r →
      c * (log G.averageDegree / G.averageDegree) * n ≤ G.indepNum

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

Erdos802.erdos_802.variants.aeks

Solved: stated here without proof.

Ajtai, Erdős, Komlós, and Szemerédi [AEKS81] proved that any \(K_r\)-free graph on \(n\) vertices with average degree \(t\) contains an independent set on

\[\gg_r \frac{\log\log(t+1)}{t}n\]

many vertices.

theorem erdos_802.variants.aeks : ∀ r : ℕ, ∃ c > (0 : ℝ), ∀ n : ℕ, ∀ G : SimpleGraph (Fin n),
    G.CliqueFree r →
      c * (log (log (G.averageDegree + 1)) / G.averageDegree) * n ≤ G.indepNum

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

Erdos802.erdos_802.variants.shearer

Solved: stated here without proof.

Shearer [Sh95] proved that any \(K_r\)-free graph on \(n\) vertices with average degree \(t\) contains an independent set on

\[\gg_r \frac{\log t}{\log\log(t+1)t}n\]

many vertices.

We assume \(t \geq 2\). For \(t + 1\) slightly larger than \(e\) the factor \(\log\log(t+1)\) is close to \(0\), so the bound blows up and the statement is false without such a restriction.

theorem erdos_802.variants.shearer : ∀ r : ℕ, ∃ c > (0 : ℝ), ∀ n : ℕ, ∀ G : SimpleGraph (Fin n),
    G.CliqueFree r → 2 ≤ G.averageDegree →
      c * (log G.averageDegree / (log (log (G.averageDegree + 1)) * G.averageDegree)) * n ≤
        G.indepNum

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

Erdos802.erdos_802.variants.r_eq_three

Solved: stated here without proof.

Ajtai, Komlós, and Szemerédi [AKS80] proved the conjectured bound when \(r = 3\): any triangle-free graph on \(n\) vertices with average degree \(t\) contains an independent set on

\[\gg \frac{\log t}{t}n\]

many vertices.

theorem erdos_802.variants.r_eq_three : ∃ c > (0 : ℝ), ∀ n : ℕ, ∀ G : SimpleGraph (Fin n),
    G.CliqueFree 3 →
      c * (log G.averageDegree / G.averageDegree) * n ≤ G.indepNum

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

Erdos802.erdos_802.variants.alon

Solved: stated here without proof.

Alon [Al96b] proved the conjectured bound under the stronger assumption that the induced graph on every vertex neighbourhood has chromatic number \(\leq r - 2\).

theorem erdos_802.variants.alon : ∀ r : ℕ, ∃ c > (0 : ℝ), ∀ n : ℕ, ∀ G : SimpleGraph (Fin n),
    (∀ v, (G.induce (G.neighborSet v)).Colorable (r - 2)) →
      c * (log G.averageDegree / G.averageDegree) * n ≤ G.indepNum

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

Sources

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

LeanErdos802.erdos_802 · Erdos802.erdos_802.variants.aeks · Erdos802.erdos_802.variants.shearer · Erdos802.erdos_802.variants.r_eq_three · Erdos802.erdos_802.variants.alon

TheoremErdős Problem 803#

References: - erdosproblems.com/803 - [ErSi70] Erdős, P. and Simonovits, M., Some extremal problems in graph theory. Combinatorial theory and its applications, I-III (Proc. Colloq., Balatonfüred, 1969) (1970), 377-390. - [Al08] Alon, Noga, Problems and results in extremal combinatorics. II. Discrete Math. (2008), 4460-4472. - [JaSu23] Janzer, Oliver and Sudakov, Benny, Resolution of the Erdős-Sauer problem on regular subgraphs. Forum Math. Pi (2023), Paper No. e19, 13.

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

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

Erdos803.erdos_803

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

We call a graph \(H\) \(D\)-balanced (or \(D\)-almost-regular) if the maximum degree of \(H\) is at most \(D\) times the minimum degree of \(H\).

Is it true that for every \(m\geq 1\), if \(n\) is sufficiently large, any graph on \(n\) vertices with \(\geq n\log n\) edges contains a \(O(1)\)-balanced subgraph with \(m\) vertices and \(\gg m\log m\) edges (where the implied constants are absolute)?

A problem of Erdős and Simonovits [ErSi70]. Alon [Al08] proved this is false: for every \(D>1\) and large \(n\) there is a graph \(G\) with \(n\) vertices and \(\geq n\log n\) edges such that if \(H\) is a \(D\)-balanced subgraph then \(H\) has \(\ll m\sqrt{\log m}+\log D\) many edges.

See also 1077.

theorem erdos_803 :
    ¬ ∃ (D c : ℝ), 0 < c ∧ ∀ m ≥ 1, ∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph (Fin n),
      (n : ℝ) * log n ≤ G.edgeSet.ncard →
        ∃ H : G.Subgraph, H.verts.ncard = m ∧ IsBalanced H.coe D ∧
          c * m * log m ≤ H.edgeSet.ncard

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

Erdos803.erdos_803.variants.alon

Solved: stated here without proof.

Alon [Al08] proved that for every \(D>1\) and large \(n\) there is a graph \(G\) with \(n\) vertices and \(\geq n\log n\) edges such that if \(H\) is a \(D\)-balanced subgraph on \(m\) vertices then \(H\) has \(\ll m\sqrt{\log m}+\log D\) many edges.

theorem erdos_803.variants.alon :
    ∃ C : ℝ, ∀ D : ℝ, 1 < D → ∀ᶠ n : ℕ in atTop, ∃ G : SimpleGraph (Fin n),
      (n : ℝ) * log n ≤ G.edgeSet.ncard ∧
      ∀ H : G.Subgraph, IsBalanced H.coe D →
        (H.edgeSet.ncard : ℝ) ≤ C * (H.verts.ncard * √(log H.verts.ncard) + log D)

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

Erdos803.erdos_803.variants.janzer_sudakov

Solved: stated here without proof.

Janzer and Sudakov [JaSu23] have proved that, for any \(k\), if \(n\) is sufficiently large then any graph on \(n\) vertices with at least \(n\log n\) edges contains a \(O(1)\)-balanced subgraph on \(m\geq k\) vertices with \(\gg_k \frac{\sqrt{\log m}}{(\log\log m)^{3/2}}m\) many edges.

theorem erdos_803.variants.janzer_sudakov :
    ∃ D : ℝ, ∀ k : ℕ, ∃ c > 0, ∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph (Fin n),
      (n : ℝ) * log n ≤ G.edgeSet.ncard →
        ∃ H : G.Subgraph, k ≤ H.verts.ncard ∧ IsBalanced H.coe D ∧
          c * (√(log H.verts.ncard) / (log (log H.verts.ncard)) ^ (3 / 2 : ℝ)) *
            H.verts.ncard ≤ H.edgeSet.ncard

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

Sources

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

LeanErdos803.erdos_803 · Erdos803.erdos_803.variants.alon · Erdos803.erdos_803.variants.janzer_sudakov

TheoremErdős Problem 804#

References: - erdosproblems.com/804 - [Er91] Erdős, P., Problems and results in combinatorial analysis and combinatorial number theory. Graph theory, combinatorics, and applications, Vol. 1 (Kalamazoo, MI, 1988) (1991), 397-406. - [AlSu07] Alon, Noga and Sudakov, Benny, On graphs with subgraphs having large independence numbers. J. Graph Theory (2007), 149-157.

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

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

Erdos804.erdos_804.parts.i

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

Let \(f(m,n)\) be maximal such that any graph on \(n\) vertices in which every induced subgraph on \(m\) vertices has an independent set of size at least \(\log n\) must contain an independent set of size at least \(f(n)\).

Estimate \(f(n)\). In particular, is it true that \(f((\log n)^2,n) \geq n^{1/2-o(1)}\)?

The answer is no: Alon and Sudakov [AlSu07] proved that in fact

\[\frac{(\log n)^2}{\log\log n}\ll f((\log n)^2,n) \ll (\log n)^2.\]

theorem erdos_804.parts.i :
    ¬ ∀ ε > 0, ∀ᶠ n : ℕ in atTop,
      (n : ℝ) ^ (1 / 2 - ε : ℝ) ≤ f ⌊(log n) ^ 2⌋₊ n

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

Erdos804.erdos_804.parts.ii

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

Is it true that \(f((\log n)^3,n)\gg (\log n)^3\)?

The answer is no: Alon and Sudakov [AlSu07] proved that in fact

\[f((\log n)^3,n)\asymp \frac{(\log n)^2}{\log\log n}.\]

theorem erdos_804.parts.ii :
    ¬ ∃ c > 0, ∀ᶠ n : ℕ in atTop, c * (log n) ^ 3 ≤ f ⌊(log n) ^ 3⌋₊ n

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

Erdos804.erdos_804.variants.alon_sudakov

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

Alon and Sudakov [AlSu07] proved that

\[\frac{(\log n)^2}{\log\log n}\ll f((\log n)^2,n) \ll (\log n)^2\]

and

\[f((\log n)^3,n)\asymp \frac{(\log n)^2}{\log\log n}.\]

theorem erdos_804.variants.alon_sudakov :
    ∃ c₂ C₂ c₃ C₃ : ℝ, 0 < c₂ ∧ 0 < C₂ ∧ 0 < c₃ ∧ 0 < C₃ ∧
    ∀ᶠ n : ℕ in atTop,
      c₂ * ((log n) ^ 2 / log (log n)) ≤ f ⌊(log n) ^ 2⌋₊ n ∧
      (f ⌊(log n) ^ 2⌋₊ n : ℝ) ≤ C₂ * (log n) ^ 2 ∧
      c₃ * ((log n) ^ 2 / log (log n)) ≤ f ⌊(log n) ^ 3⌋₊ n ∧
      (f ⌊(log n) ^ 3⌋₊ n : ℝ) ≤ C₃ * ((log n) ^ 2 / log (log n))

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

Sources

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

LeanErdos804.erdos_804.parts.i · Erdos804.erdos_804.parts.ii · Erdos804.erdos_804.variants.alon_sudakov

TheoremErdős Problem 805#

References: - erdosproblems.com/805 - [Er91] Erdős, P., Problems and results in combinatorial analysis and combinatorial number theory. Graph theory, combinatorics, and applications, Vol. 1 (Kalamazoo, MI, 1988) (1991), 397-406. - [AlSu07] Alon, N. and Sudakov, B., On graphs with subgraphs having large independence numbers. J. Graph Theory 56 (2007), 149-157. arXiv:0706.4099 - [ABS21] Alon, N., Bucić, M. and Sudakov, B., Large cliques and independent sets all over the place. Proc. Amer. Math. Soc. 149 (2021), 3145-3157. arXiv:2004.04718

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

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

Erdos805.erdos_805.parts.i

Open: stated without proof.

For which functions \(g(n)\) with \(n>g(n)\geq (\log n)^2\) is there a graph on \(n\) vertices in which every induced subgraph on \(g(n)\) vertices contains a clique of size \(\geq \log n\) and an independent set of size \(\geq \log n\)?

In particular, is there such a graph for \(g(n)=(\log n)^3\)?

This is the first part. A problem of Erdős and Hajnal [Er91]; see also erdosproblems.com/804. The inequalities on g are required for all large n, and a graph is required for all large n.

theorem erdos_805.parts.i :
    {g : ℕ → ℕ | (∀ᶠ n : ℕ in atTop, Real.log n ^ 2 ≤ g n ∧ g n < n) ∧ HasRamseyGraphs g} =
      erdos_805.parts.i.answer

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

Erdos805.erdos_805.parts.ii

Open: stated without proof.

For which functions \(g(n)\) with \(n>g(n)\geq (\log n)^2\) is there a graph on \(n\) vertices in which every induced subgraph on \(g(n)\) vertices contains a clique of size \(\geq \log n\) and an independent set of size \(\geq \log n\)?

In particular, is there such a graph for \(g(n)=(\log n)^3\)?

This is the second part. Erdős and Hajnal thought that there is no such graph for \(g(n)=(\log n)^3\) [AlSu07]; we state the positive proposition, with \(g(n)=\lfloor(\log n)^3\rfloor\) and a graph required for all large \(n\), as in the first part.

theorem erdos_805.parts.ii : HasRamseyGraphs (fun n ↦ ⌊Real.log n ^ 3⌋₊)

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

Erdos805.erdos_805.variants.alon_sudakov

Solved: stated here without proof.

Alon and Sudakov [AlSu07] proved that there is no such graph with

\[g(n)=\frac{c}{\log\log n}(\log n)^3\]

for some constant \(c>0\).

Here log is the natural logarithm, as in [AlSu07], and the statement is for all large n.

theorem erdos_805.variants.alon_sudakov :
    ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop, ¬ ∃ G : SimpleGraph (Fin n),
      IsLocallyRamsey G ⌊c * Real.log n ^ 3 / Real.log (Real.log n)⌋₊ ⌈Real.log n⌉₊

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

Erdos805.erdos_805.variants.alon_bucic_sudakov

Solved: stated here without proof.

Alon, Bucić, and Sudakov [ABS21] construct such a graph with

\[g(n)\leq 2^{2^{(\log\log n)^{1/2+o(1)}}}.\]

Here all logarithms are to base \(2\), as in [ABS21], so the cliques and independent sets have at least \(\lceil\log_2 n\rceil\) vertices; this implies the natural-logarithm version of the problem. The \(o(1)\) is expressed as: for every \(0\lt \varepsilon<1/2\) and all large \(n\) there is such a graph with \(g(n)=\lceil 2^{2^{(\log_2\log_2 n)^{1/2+\varepsilon}}}\rceil\). This form, with the rounding, follows from [ABS21, Theorem 2].

theorem erdos_805.variants.alon_bucic_sudakov :
    ∀ ε : ℝ, 0 < ε → ε < 1 / 2 → ∀ᶠ n : ℕ in atTop, ∃ G : SimpleGraph (Fin n),
      IsLocallyRamsey G
        ⌈(2 : ℝ) ^ ((2 : ℝ) ^ (Real.logb 2 (Real.logb 2 n) ^ (1 / 2 + ε)))⌉₊
        ⌈Real.logb 2 n⌉₊

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

Sources

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

LeanErdos805.erdos_805.parts.i · Erdos805.erdos_805.parts.ii · Erdos805.erdos_805.variants.alon_sudakov · Erdos805.erdos_805.variants.alon_bucic_sudakov

TheoremErdős Problem 806#

References: - erdosproblems.com/806 - [ErNe77] Erdős, P. and Newman, D. J., Bases for sets of integers. J. Number Theory (1977), 420-425. - [ABS09] Alon, Noga and Bukh, Boris and Sudakov, Benny, Discrete Kakeya-type problems and small bases. Israel J. Math. (2009), 285-301.

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

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

Erdos806.erdos_806

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

Let \(A\subseteq \{1,\ldots,n\}\) with \(\lvert A\rvert \leq n^{1/2}\). Must there exist some \(B\subset\mathbb{Z}\) with \(\lvert B\rvert=o(n^{1/2})\) such that \(A\subseteq B+B\)?

A problem of Erdős and Newman [ErNe77], who proved that there exist \(A\) with \(\lvert A\rvert\asymp n^{1/2}\) such that if \(A\subseteq B+B\) then

\[\lvert B\rvert \gg \frac{\log\log n}{\log n}n^{1/2}.\]

Resolved by Alon, Bukh, and Sudakov [ABS09], who proved that for any \(A\subseteq \{1,\ldots,n\}\) with \(\lvert A\rvert \leq n^{1/2}\) there exists some \(B\) such that \(A\subseteq B+B\) and

\[\lvert B\rvert \ll \frac{\log\log n}{\log n}n^{1/2}.\]

See also 333.

theorem erdos_806 : ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop,
    ∀ A : Finset ℕ, A ⊆ Finset.Icc 1 n → (A.card : ℝ) ≤ √n →
      ∃ B : Finset ℤ, A.map Nat.castEmbedding ⊆ B + B ∧ (B.card : ℝ) ≤ ε * √n

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

Erdos806.erdos_806.variants.alon_bukh_sudakov

Solved: stated here without proof.

Alon, Bukh, and Sudakov [ABS09] proved that for any \(A\subseteq \{1,\ldots,n\}\) with \(\lvert A\rvert \leq n^{1/2}\) there exists some \(B\) such that \(A\subseteq B+B\) and \(\lvert B\rvert \ll \frac{\log\log n}{\log n}n^{1/2}\).

theorem erdos_806.variants.alon_bukh_sudakov : ∃ C : ℝ, ∀ᶠ n : ℕ in atTop,
    ∀ A : Finset ℕ, A ⊆ Finset.Icc 1 n → (A.card : ℝ) ≤ √n →
      ∃ B : Finset ℤ, A.map Nat.castEmbedding ⊆ B + B ∧
        (B.card : ℝ) ≤ C * Real.log (Real.log n) / Real.log n * √n

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

Erdos806.erdos_806.variants.erdos_newman

Solved: stated here without proof.

Erdős and Newman [ErNe77] proved that there exist \(A\subseteq\{1,\ldots,n\}\) with \(\lvert A\rvert\asymp n^{1/2}\) such that if \(A\subseteq B+B\) then \(\lvert B\rvert \gg \frac{\log\log n}{\log n}n^{1/2}\).

theorem erdos_806.variants.erdos_newman : ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
    ∃ A : Finset ℕ, A ⊆ Finset.Icc 1 n ∧ c * √n ≤ A.card ∧ (A.card : ℝ) ≤ √n ∧
      ∀ B : Finset ℤ, A.map Nat.castEmbedding ⊆ B + B →
        c * Real.log (Real.log n) / Real.log n * √n ≤ B.card

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

Sources

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

LeanErdos806.erdos_806 · Erdos806.erdos_806.variants.alon_bukh_sudakov · Erdos806.erdos_806.variants.erdos_newman

TheoremErdős Problem 808#

References: - erdosproblems.com/808 - [ErSz83] Erdős, P. and Szemerédi, E., On sums and products of integers. Studies in pure mathematics (1983), 213-218. PDF - [ARS20] Alon, Noga and Ruzsa, Imre and Solymosi, József, Sums, products and ratios along the edges of a graph. Publ. Mat. (2020), 143-155. arXiv:1802.06405

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

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

Erdos808.erdos_808

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

Let \(c,\epsilon>0\) and \(n\) be sufficiently large. If \(A\subset \mathbb{N}\) has \(\lvert A\rvert=n\) and \(G\) is any graph on \(A\) with at least \(n^{1+c}\) edges then

\[\max(\lvert A+_GA\rvert,\lvert A\cdot_G A\rvert) \geq \lvert A\rvert^{1+c-\epsilon},\]

where

\[A+_GA = \{ a+b : (a,b)\in G\}\]

and similarly for \(A\cdot_GA\).

This strong conjecture of Erdős and Szemerédi [ErSz83] strengthens Erdős Problem 52 (Erdos52.erdos_52, the case of the complete graph). It was disproved by Alon, Ruzsa, and Solymosi [ARS20, Theorem 3]: for arbitrarily large \(m\) there are a set of integers \(A\) with \(\lvert A\rvert=m\) and a graph on \(A\) with \(\gg m^{5/3}/(\log m)^{1/3}\) edges such that \(\lvert A+_GA\rvert+\lvert A\cdot_GA\rvert \ll (m\log m)^{4/3}\). The statement below is the negation of the conjecture.

A set \(A\) with a graph on it is given by a finite type V, a graph G on V and an injection a : V ↪ ℕ (so \(A\) is the image of a and \(n\) is Fintype.card V). Here ℕ contains \(0\); see erdos_808.variants.positive for positive integers.

theorem erdos_808 :
    ¬ ∀ c : ℝ, 0 < c → ∀ ε : ℝ, 0 < ε →
      ∃ n₀ : ℕ, ∀ (V : Type) [Fintype V] (a : V ↪ ℕ) (G : SimpleGraph V) [DecidableRel G.Adj],
        n₀ ≤ Fintype.card V →
        (Fintype.card V : ℝ) ^ (1 + c) ≤ (G.edgeFinset.card : ℝ) →
        (Fintype.card V : ℝ) ^ (1 + c - ε) ≤
          max ((edgeSums a G).card : ℝ) ((edgeProducts a G).card : ℝ)

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

Erdos808.erdos_808.variants.positive

Solved: stated here without proof.

The conjecture already fails for positive integers: the set of integers constructed in [ARS20, Theorem 3] consists of positive integers. This is erdos_808 with the extra hypothesis ∀ v, 0 < a v, so it implies erdos_808.

theorem erdos_808.variants.positive :
    ¬ ∀ c : ℝ, 0 < c → ∀ ε : ℝ, 0 < ε →
      ∃ n₀ : ℕ, ∀ (V : Type) [Fintype V] (a : V ↪ ℕ), (∀ v, 0 < a v) →
        ∀ (G : SimpleGraph V) [DecidableRel G.Adj],
          n₀ ≤ Fintype.card V →
          (Fintype.card V : ℝ) ^ (1 + c) ≤ (G.edgeFinset.card : ℝ) →
          (Fintype.card V : ℝ) ^ (1 + c - ε) ≤
            max ((edgeSums a G).card : ℝ) ((edgeProducts a G).card : ℝ)

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

Erdos808.erdos_808.variants.ars_lower_bound

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

Alon, Ruzsa, and Solymosi do prove, however, that if \(A\) has size \(n\) and \(G\) has \(m\) edges then

\[\max(\lvert A+_GA\rvert,\lvert A\cdot_G A\rvert) \gg m^{3/2}n^{-7/4}.\]

This is [ARS20, Theorem 10]. It holds for any \(n\)-element set of real numbers, and [ARS20] state it for \(\lvert A+_GA\rvert+\lvert A\cdot_GA\rvert\), which is within a factor \(2\) of the maximum. It is written in multiplied-out form, so that \(n=0\) needs no division.

theorem erdos_808.variants.ars_lower_bound :
    ∃ K : ℝ, 0 < K ∧
      ∀ (V : Type) [Fintype V] (a : V ↪ ℝ) (G : SimpleGraph V) [DecidableRel G.Adj],
        (G.edgeFinset.card : ℝ) ^ ((3 : ℝ) / 2) ≤
          K * (Fintype.card V : ℝ) ^ ((7 : ℝ) / 4) *
            max ((edgeSums a G).card : ℝ) ((edgeProducts a G).card : ℝ)

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

Sources

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

LeanErdos808.erdos_808 · Erdos808.erdos_808.variants.positive · Erdos808.erdos_808.variants.ars_lower_bound

TheoremErdős Problem 810#

References: - erdosproblems.com/810 - [BEGS89] Burr, S. A., Erdős, P., Graham, R. L., and Sós, V. T., Maximal anti-Ramsey graphs and the strong chromatic number. J. Graph Theory 13 (1989), no. 3, 263–282. - [Er91] Erdős, P., Problems and results in combinatorial analysis and combinatorial number theory. Graph theory, combinatorics, and applications, Vol. 1 (1991), 397–406.

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

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

Erdos810.erdos_810

Open: stated without proof.

Does there exist some \(\epsilon>0\) such that, for all sufficiently large \(n\), there exists a graph \(G\) on \(n\) vertices with at least \(\epsilon n^2\) edges whose edges can be coloured with \(n\) colours so that every \(C_4\) receives four distinct colours?

theorem erdos_810 : ∃ ε > 0, ∀ᶠ n in atTop,
    ∃ G : SimpleGraph (Fin n), ∃ color : Fin n → Fin n → Fin n,
      ε * (n : ℝ) ^ 2 ≤ (G.edgeSet.ncard : ℝ) ∧ C4RainbowColoring G color

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

Sources

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

LeanErdos810.erdos_810

TheoremErdős Problem 812#

References: - erdosproblems.com/812 - [BEFS89] Burr, S. A. and Erd\H{o}s, P. and Faudree, R. J. and Schelp, R. H., On the difference between consecutive {R}amsey numbers. Utilitas Math. (1989), 115--118.

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

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

Erdos812.erdos_812.parts.i

Open: stated without proof.

Is it true that \(\frac{R(n+1)}{R(n)}\geq 1+c\) for some constant \(c>0\), for all large \(n\)?

theorem erdos_812.parts.i :
    ∃ c > 0, ∀ᶠ n in atTop, (R (n + 1) : ℝ) / (R n : ℝ) ≥ 1 + c

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

Erdos812.erdos_812.parts.ii

Open: stated without proof.

Is it true that \(R(n+1)-R(n) \gg n^2\)?

theorem erdos_812.parts.ii :
    (fun n : ℕ ↦ (R (n + 1) : ℝ) - (R n : ℝ)) ≫ (fun n : ℕ ↦ (n : ℝ) ^ 2)

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

Erdos812.erdos_812.variants.lower_bound

Solved: stated here without proof.

Burr, Erdős, Faudree, and Schelp [BEFS89] proved that \(R(n+1)-R(n) \geq 4n-8\) for all \(n\geq 2\).

theorem erdos_812.variants.lower_bound :
    ∀ n : ℕ, n ≥ 2 → (R (n + 1) : ℤ) - (R n : ℤ) ≥ 4 * (n : ℤ) - 8

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

Sources

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

LeanErdos812.erdos_812.parts.i · Erdos812.erdos_812.parts.ii · Erdos812.erdos_812.variants.lower_bound

TheoremErdős Problem 813#

References: - erdosproblems.com/813 - [Er91] Erdős, P., Problems and results in combinatorial analysis and combinatorial number theory. Graph theory, combinatorics, and applications, Vol. 1 (Kalamazoo, MI, 1988) (1991), 397-406. - [BuSu23] Bucić, M. and Sudakov, B., Large independent sets from local considerations. Combinatorica 43 (2023), 505-546. arXiv:2007.03667

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

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

Erdos813.erdos_813

Open: stated without proof.

Let \(h(n)\) be minimal such that every graph on \(n\) vertices where every set of \(7\) vertices contains a triangle must contain a clique on at least \(h(n)\) vertices. Estimate \(h(n)\). In particular, do there exist constants \(c_1, c_2 > 0\) such that

\[n^{1/3+c_1} \ll h(n) \ll n^{1/2-c_2}?\]

The lower half has a positive answer (Erdos813.erdos_813.variants.lower); the upper half is Erdos813.erdos_813.variants.upper.

theorem erdos_813 :
    ∃ c₁ > (0 : ℝ), ∃ c₂ > (0 : ℝ),
      (fun n : ℕ ↦ (n : ℝ) ^ (1 / 3 + c₁ : ℝ)) =O[atTop] (fun n ↦ (h n : ℝ)) ∧
        (fun n : ℕ ↦ (h n : ℝ)) =O[atTop] (fun n : ℕ ↦ (n : ℝ) ^ (1 / 2 - c₂ : ℝ))

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

Erdos813.erdos_813.variants.erdos_hajnal

Solved: stated here without proof.

Erdős and Hajnal proved (see [Er91]) that

\[n^{1/3} \ll h(n) \ll n^{1/2}.\]

theorem erdos_813.variants.erdos_hajnal :
    (fun n : ℕ ↦ (n : ℝ) ^ (1 / 3 : ℝ)) =O[atTop] (fun n ↦ (h n : ℝ)) ∧
      (fun n : ℕ ↦ (h n : ℝ)) =O[atTop] (fun n : ℕ ↦ (n : ℝ) ^ (1 / 2 : ℝ))

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

Erdos813.erdos_813.variants.bucic_sudakov

Solved: stated here without proof.

Bucić and Sudakov [BuSu23] proved that \(h(n) \gg n^{5/12-o(1)}\). Their result is stated for graphs in which every \(7\) vertices contain an independent set of size \(3\); it applies to \(h\) by taking complements.

theorem erdos_813.variants.bucic_sudakov :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (n : ℝ) ^ (5 / 12 - ε : ℝ) ≤ (h n : ℝ)

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

Erdos813.erdos_813.variants.lower

Solved: stated here without proof.

The lower half of Erdos813.erdos_813 has a positive answer: there is a constant \(c_1 > 0\) with \(n^{1/3+c_1} \ll h(n)\). This follows from the bound \(h(n) \gg n^{5/12-o(1)}\) of Bucić and Sudakov [BuSu23], since \(5/12 > 1/3\).

theorem erdos_813.variants.lower :
    ∃ c₁ > (0 : ℝ), (fun n : ℕ ↦ (n : ℝ) ^ (1 / 3 + c₁ : ℝ)) =O[atTop] (fun n ↦ (h n : ℝ))

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

Erdos813.erdos_813.variants.upper

Open: stated without proof.

The upper half of Erdos813.erdos_813: is there a constant \(c_2 > 0\) with \(h(n) \ll n^{1/2-c_2}\)?

theorem erdos_813.variants.upper :
    ∃ c₂ > (0 : ℝ), (fun n : ℕ ↦ (h n : ℝ)) =O[atTop] (fun n : ℕ ↦ (n : ℝ) ^ (1 / 2 - c₂ : ℝ))

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

Sources

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

LeanErdos813.erdos_813 · Erdos813.erdos_813.variants.erdos_hajnal · Erdos813.erdos_813.variants.bucic_sudakov · Erdos813.erdos_813.variants.lower · Erdos813.erdos_813.variants.upper

TheoremErdős Problem 814#

References: - erdosproblems.com/814 - [EFRS90] Erdős, P. and Faudree, R. J. and Rousseau, C. C. and Schelp, R. H., Subgraphs of minimal degree k. Discrete Math. (1990), 53--58. - [Er91] Erdős, P., Problems and results in combinatorial analysis and combinatorial number theory. Graph theory, combinatorics, and applications, Vol. 1 (Kalamazoo, MI, 1988) (1991), 397-406. - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350. - [MNS17] Mousset, Frank and Noever, Andreas and Škorić, Nemanja, Smaller subgraphs of minimum degree k. Electron. J. Combin. (2017), Paper No. 4.9, 8. - [Sa19] Sauermann, Lisa, A proof of a conjecture of Erdős, Faudree, Rousseau and Schelp on subgraphs of minimum degree k. J. Combin. Theory Ser. B (2019), 36--75.

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

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

Erdos814.erdos_814

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

Let \(k\geq 2\) and \(G\) be a graph with \(n\geq k-1\) vertices and

\[(k-1)(n-k+2)+\binom{k-2}{2}+1\]

edges. Does there exist some \(c_k>0\) such that \(G\) must contain an induced subgraph on at most \((1-c_k)n\) vertices with minimum degree at least \(k\)?

The case \(k=3\) was a problem of Erdős and Hajnal [Er91]. The question for general \(k\) was a conjecture of Erdős, Faudree, Rousseau, and Schelp [EFRS90], who proved that such a subgraph exists with at most \(n-c_k\sqrt{n}\) vertices. Mousset, Noever, and Skorić [MNS17] improved this to \(n-c_k\frac{n}{\log n}\). The full conjecture was proved by Sauermann [Sa19], who proved this with \(c_k \gg 1/k^3\).

theorem erdos_814 :
    ∀ k ≥ 2, ∃ c > 0, ∀ n ≥ k - 1, ∀ G : SimpleGraph (Fin n),
      G.edgeFinset.card = (k - 1) * (n + 2 - k) + (k - 2).choose 2 + 1 →
        ∃ S : Finset (Fin n), S.Nonempty ∧ (S.card : ℝ) ≤ (1 - c) * n ∧
          k ≤ (G.induce (S : Set (Fin n))).minDegree

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

Erdos814.erdos_814.variants.at_least

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

The conclusion holds as soon as \(G\) has at least \((k-1)(n-k+2)+inom{k-2}{2}+1\) edges (Sauermann [Sa19]).

theorem erdos_814.variants.at_least :
    ∀ k ≥ 2, ∃ c > 0, ∀ n ≥ k - 1, ∀ G : SimpleGraph (Fin n),
      (k - 1) * (n + 2 - k) + (k - 2).choose 2 + 1 ≤ G.edgeFinset.card →
        ∃ S : Finset (Fin n), S.Nonempty ∧ (S.card : ℝ) ≤ (1 - c) * n ∧
          k ≤ (G.induce (S : Set (Fin n))).minDegree

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

Erdos814.erdos_814.variants.sauermann

Solved: stated here without proof.

Sauermann [Sa19] proved this with \(c_k \gg 1/k^3\).

theorem erdos_814.variants.sauermann :
    ∃ C > 0, ∀ k ≥ 2, ∀ n ≥ k - 1, ∀ G : SimpleGraph (Fin n),
      (k - 1) * (n + 2 - k) + (k - 2).choose 2 + 1 ≤ G.edgeFinset.card →
        ∃ S : Finset (Fin n), S.Nonempty ∧ (S.card : ℝ) ≤ (1 - C / k ^ 3) * n ∧
          k ≤ (G.induce (S : Set (Fin n))).minDegree

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

Sources

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

LeanErdos814.erdos_814 · Erdos814.erdos_814.variants.at_least · Erdos814.erdos_814.variants.sauermann

TheoremErdős Problem 816#

References: - erdosproblems.com/816 - [Er91] Erdős, P., Problems and results in combinatorial analysis and combinatorial number theory. Graph theory, combinatorics, and applications, Vol. 1 (Kalamazoo, MI, 1988) (1991), 397-406. - [ChMa25] K. Chen and J. Ma, A problem of Erdős and Hajnal on paths with equal-degree endpoints. arXiv:2503.19569 (2025).

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

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

Erdos816.erdos_816

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

Let \(G\) be a graph with \(2n+1\) vertices and \(n^2+n+1\) edges. Must \(G\) contain two vertices of the same degree which are joined by a path of length \(3\)?

A problem of Erdős and Hajnal. The example of \(K_{n,n+1}\) shows that this fails if we only have \(n^2+n\) edges.

This is true, and was proved by Chen and Ma [ChMa25], who prove the stronger statement that, provided \(n\geq 600\), all graphs with \(2n+1\) vertices and at least \(n^2+n\) edges contain two vertices of the same degree joined by a path of length \(3\), except \(K_{n,n+1}\).

For \(n = 1\) the graph is a triangle, which contains no path of length \(3\), so we assume \(n \geq 2\).

theorem erdos_816 : ∀ n : ℕ, 2 ≤ n → ∀ G : SimpleGraph (Fin (2 * n + 1)),
    G.edgeFinset.card = n ^ 2 + n + 1 → HasEqualDegreePathThree G

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

Erdos816.erdos_816.variants.chen_ma

Solved: stated here without proof.

Chen and Ma [ChMa25] proved that, provided \(n\geq 600\), all graphs with \(2n+1\) vertices and at least \(n^2+n\) edges contain two vertices of the same degree joined by a path of length \(3\), except \(K_{n,n+1}\).

theorem erdos_816.variants.chen_ma : ∀ n : ℕ, 600 ≤ n →
    ∀ G : SimpleGraph (Fin (2 * n + 1)), n ^ 2 + n ≤ G.edgeFinset.card →
      ¬ Nonempty (G ≃g completeBipartiteGraph (Fin n) (Fin (n + 1))) →
        HasEqualDegreePathThree G

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

Erdos816.erdos_816.variants.complete_bipartite

Solved: stated here without proof.

The example of \(K_{n,n+1}\) shows that this fails if we only have \(n^2+n\) edges.

theorem erdos_816.variants.complete_bipartite : ∀ n : ℕ,
    (completeBipartiteGraph (Fin n) (Fin (n + 1))).edgeFinset.card = n ^ 2 + n ∧
      ¬ HasEqualDegreePathThree (completeBipartiteGraph (Fin n) (Fin (n + 1)))

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

Sources

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

LeanErdos816.erdos_816 · Erdos816.erdos_816.variants.chen_ma · Erdos816.erdos_816.variants.complete_bipartite

TheoremErdős Problem 817#

References: - erdosproblems.com/817 - [Co26] Costa, S., A negative answer to the Erdős–Sárközy question. arXiv:2609.06303 (2026).

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

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

Erdos817.erdos_817

Solved: stated here; a Lean proof is at https://zenodo.org/records/22638810.

Let \(k \geq 3\). Define \(g_k(n)\) to be the minimal \(N\) such that \(\{1, ..., N\}\) contains some \(A\) of size \(|A| = n\) such that

\[ \langle A\rangle = \left\{\sum_{a \in A} \epsilon_a a : \epsilon_a \in\{0, 1\}\right\} \]

contains no non-trivial \(k\)-term arithmetic progression. Estimate \(g_k(n)\). In particular, is it true that

\[ g_3(n) \gg 3^n \]

The answer is no: Costa [Co26, Corollary 1.2] proved that \(\liminf_{n \to \infty} g_3(n)/3^n = 0\).

theorem erdos_817 :
    ¬ (fun n => (3 ^ n : ℝ)) =O[atTop] fun n => (g 3 n : ℝ)

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

Erdos817.erdos_817.variants.bdd_power

Solved: stated here without proof.

A problem of Erdős and Sárközy who proved

\[ g_3(n) \gg \frac{3^n}{n^{O(1)}}. \]

theorem erdos_817.variants.bdd_power : ∃ O > (0 : ℝ),
    (fun (n : ℕ) => (3 ^ n : ℝ) / n ^ O) =O[atTop] fun n => (g 3 n : ℝ)

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

Sources

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

LeanErdos817.erdos_817 · Erdos817.erdos_817.variants.bdd_power

TheoremErdős Problem 818#

References: - erdosproblems.com/818 - [So09d] Solymosi, József, Bounding multiplicative energy by the sumset. Adv. Math. (2009), 402-408.

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

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

Erdos818.erdos_818

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

Let \(A\) be a finite set of integers such that \(\lvert A+A\rvert \ll \lvert A\rvert\). Is it true that

\[\lvert AA\rvert \gg \frac{\lvert A\rvert^2}{(\log \lvert A\rvert)^C}\]

for some constant \(C>0\)?

This was proved by Solymosi [So09d], in the strong form

\[\lvert AA\rvert \gg \frac{\lvert A\rvert^2}{\log \lvert A\rvert}.\]

See also [52].

theorem erdos_818 :
    ∀ K : ℝ, 0 < K → ∃ C : ℝ, 0 < C ∧ ∃ c : ℝ, 0 < c ∧
      ∀ A : Finset ℤ, 2 ≤ A.card → ((A + A).card : ℝ) ≤ K * (A.card : ℝ) →
        c * (A.card : ℝ) ^ 2 / (Real.log (A.card : ℝ)) ^ C ≤ ((A * A).card : ℝ)

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

Erdos818.erdos_818.variants.solymosi

Solved: stated here without proof.

This was proved by Solymosi [So09d], in the strong form

\[\lvert AA\rvert \gg \frac{\lvert A\rvert^2}{\log \lvert A\rvert}.\]

theorem erdos_818.variants.solymosi :
    ∀ K : ℝ, 0 < K → ∃ c : ℝ, 0 < c ∧
      ∀ A : Finset ℤ, 2 ≤ A.card → ((A + A).card : ℝ) ≤ K * (A.card : ℝ) →
        c * (A.card : ℝ) ^ 2 / Real.log (A.card : ℝ) ≤ ((A * A).card : ℝ)

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

Sources

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

LeanErdos818.erdos_818 · Erdos818.erdos_818.variants.solymosi

TheoremErdős Problem 819#

References: - erdosproblems.com/819 - [Er91] Erdős, P., Problems and results in combinatorial analysis and combinatorial number theory. Graph theory, combinatorics, and applications, Vol. 1 (Kalamazoo, MI, 1988) (1991), 397-406. - [ErFr91] Erdős, P. and Freud, R., On sums of a Sidon-sequence. J. Number Theory 38 (1991), 196-205.

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

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

Erdos819.erdos_819

Open: stated without proof.

Let \(f(N)\) be maximal such that there exists \(A\subseteq \{1,\ldots,N\}\) with \(\lvert A\rvert=\lfloor N^{1/2}\rfloor\) such that \(\lvert (A+A)\cap [1,N]\rvert=f(N)\). Estimate \(f(N)\).

theorem erdos_819 : (fun N ↦ (f N : ℝ)) ~[atTop] erdos_819.answer

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

Erdos819.erdos_819.variants.erdos_freud_lower

Solved: stated here without proof.

Erdős and Freud [ErFr91] proved

\[\left(\frac{3}{8}-o(1)\right)N \leq f(N) \leq \left(\frac{1}{2}+o(1)\right)N.\]

This is the lower bound.

theorem erdos_819.variants.erdos_freud_lower :
    ∀ ε > (0 : ℝ), ∀ᶠ N : ℕ in atTop, (3 / 8 - ε) * N ≤ (f N : ℝ)

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

Erdos819.erdos_819.variants.erdos_freud_upper

Proved here.

Erdős and Freud [ErFr91] proved

\[\left(\frac{3}{8}-o(1)\right)N \leq f(N) \leq \left(\frac{1}{2}+o(1)\right)N.\]

This is the upper bound.

theorem erdos_819.variants.erdos_freud_upper :
    ∀ ε > (0 : ℝ), ∀ᶠ N : ℕ in atTop, (f N : ℝ) ≤ (1 / 2 + ε) * N

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

Sources

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

LeanErdos819.erdos_819 · Erdos819.erdos_819.variants.erdos_freud_lower · Erdos819.erdos_819.variants.erdos_freud_upper

TheoremErdős Problem 820#

References: - erdosproblems.com/820 - [Er74b] Erdős, P., Remarks on some problems in number theory. Math. Balkanica (1974), 197-202. - OEIS A263647: the \(n\) with \((2^n-1, 3^n-1) = 1\).

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

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

Erdos820.erdos_820

Open: stated without proof.

Let \(H(n)\) be the smallest integer \(l\) such that there exists \(k < l\) with \((k^n-1, l^n-1) = 1\). Is it true that \(H(n) = 3\) infinitely often? That is, is \((2^n-1, 3^n-1) = 1\) for infinitely many \(n\) (see Erdos820.H_eq_three_iff)?

The request to estimate \(H(n)\) is open-ended and not formalised; the variants below state the specific questions that are asked. See also Erdős Problem 770.

theorem erdos_820 : {n : ℕ | H n = 3}.Infinite

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

Erdos820.erdos_820.variants.log_log_exponent

Open: stated without proof.

Is it true that there exists some constant \(c > 0\) such that, for all \(\epsilon > 0\),

\[ H(n) > \exp\left(n^{(c-\epsilon)/\log\log n}\right) \]

for infinitely many \(n\) and

\[ H(n) < \exp\left(n^{(c+\epsilon)/\log\log n}\right) \]

for all large enough \(n\)?

theorem erdos_820.variants.log_log_exponent :
    ∃ c > (0 : ℝ), ∀ ε > (0 : ℝ),
      (∃ᶠ n : ℕ in atTop,
        Real.exp ((n : ℝ) ^ ((c - ε) / Real.log (Real.log (n : ℝ)))) < (H n : ℝ)) ∧
      ∀ᶠ n : ℕ in atTop,
        (H n : ℝ) < Real.exp ((n : ℝ) ^ ((c + ε) / Real.log (Real.log (n : ℝ))))

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

Erdos820.erdos_820.variants.two_pow_upper

Open: stated without proof.

Let \(K(n)\) be the smallest \(k\) such that \((k^n-1, 2^n-1) = 1\). Does a similar upper bound hold for \(K(n)\)? That is, is there a constant \(c > 0\) such that, for all \(\epsilon > 0\),

\[ K(n) < \exp\left(n^{(c+\epsilon)/\log\log n}\right) \]

for all large enough \(n\)?

We read "similar" as an upper bound of the same shape, with its own constant \(c\), which need not be the same as in Erdos820.erdos_820.variants.log_log_exponent.

theorem erdos_820.variants.two_pow_upper :
    ∃ c > (0 : ℝ), ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (K n : ℝ) < Real.exp ((n : ℝ) ^ ((c + ε) / Real.log (Real.log (n : ℝ))))

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

Erdos820.erdos_820.variants.erdos_lower

Solved: stated here without proof.

Erdős [Er74b] proved that there exists a constant \(c > 0\) such that

\[ H(n) > \exp\left(n^{c/(\log\log n)^2}\right) \]

for infinitely many \(n\).

theorem erdos_820.variants.erdos_lower :
    ∃ c > (0 : ℝ), ∃ᶠ n : ℕ in atTop,
      Real.exp ((n : ℝ) ^ (c / Real.log (Real.log (n : ℝ)) ^ 2)) < (H n : ℝ)

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

Sources

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

LeanErdos820.erdos_820 · Erdos820.erdos_820.variants.log_log_exponent · Erdos820.erdos_820.variants.two_pow_upper · Erdos820.erdos_820.variants.erdos_lower

TheoremErdős Problem 821#

References: - erdosproblems.com/821 - [BaHa98] Baker, R. C. and Harman, G., Shifted primes without large prime factors. Acta Arith. (1998), 331--361. - [Er35b] Erdős, P., On the normal number of prime factors of \(p-1\) and some related problems concerning Euler's \(\varphi\)-function. Quart. J. Math. (1935), 205-213. - [Er74b] Erdős, P., Remarks on some problems in number theory. Math. Balkanica (1974), 197-202. - [Li22] J. D. Lichtman, Primes in arithmetic progressions to large moduli and shifted primes without large prime factors. arXiv:2211.09641 (2022). - [LuPo11] Luca, Florian and Pollack, Paul, An arithmetic function arising from {C}armichael's conjecture. J. Théor. Nombres Bordeaux (2011), 697--714. - [OpenAI26] OpenAI, Weighted dilation graphs, smooth shifted primes and totient fibers. OpenAI Math Release preprint (September 2026). github.com/openai/math

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

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

Erdos821.erdos_821

Solved: stated here; a Lean proof is at https://github.com/cadamcat/totient-fibers-lean4/blob/dfce35707a67fce7362cb2bd95af8b80a0b0373e/Erdos821/Theorem.lean#L18.

Is it true that, for every \(\epsilon>0\), there exist infinitely many \(n\) such that \(g(n) > n^{1-\epsilon}\)?

This was proved in [OpenAI26]; see the linked formal proof for more explanations.

theorem erdos_821 :
    ∀ ε > (0 : ℝ), { n : ℕ | (g n : ℝ) > (n : ℝ) ^ (1 - ε) }.Infinite

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

Erdos821.erdos_821.variants.pillai

Solved: stated here without proof.

Pillai proved that \(\limsup g(n)=\infty\).

theorem erdos_821.variants.pillai :
    atTop.limsup (fun n : ℕ ↦ (g n : EReal)) = ⊤

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

Erdos821.erdos_821.variants.erdos

Solved: stated here without proof.

Erdős [Er35b] proved that there exists some constant \(c>0\) such that \(g(n) > n^c\) for infinitely many \(n\).

theorem erdos_821.variants.erdos :
    ∃ c > (0 : ℝ), { n : ℕ | (n : ℝ) ^ c < (g n : ℝ) }.Infinite

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

Erdos821.erdos_821.variants.lichtman

Solved: stated here without proof.

The best known bound is that there are infinitely many \(n\) such that \(g(n) > n^{0.71568\cdots}\), obtained by Lichtman [Li22] as a consequence of proving that there are \(\geq \frac{x}{(\log x)^{O(1)}}\) many primes \(p\leq x\) such that all prime factors of \(p-1\) are \(\leq x^{0.2843\cdots}\) (which improves a number of previous exponents, most recently Baker and Harman [BaHa98]).

theorem erdos_821.variants.lichtman :
    ∃ c > (0.71568 : ℝ), { n : ℕ | (n : ℝ) ^ c < (g n : ℝ) }.Infinite

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

Sources

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

LeanErdos821.erdos_821 · Erdos821.erdos_821.variants.pillai · Erdos821.erdos_821.variants.erdos · Erdos821.erdos_821.variants.lichtman

TheoremErdős Problem 822#

References: - erdosproblems.com/822 - [GIL24] Gabdullin, Mikhail R. and Iudelevich, Vitalii V. and Luca, Florian, Numbers of the form {\(k+f(k)\)}. J. Number Theory (2024), 58--85.

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

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

Erdos822.erdos_822

Solved: stated here without proof.

Does the set of integers of the form \(n + \varphi(n)\) have positive (lower) density?

[GIL24] proved this was true.

theorem erdos_822 :
    0 < (Set.range fun n => n + Nat.totient n).lowerDensity

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

Sources

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

LeanErdos822.erdos_822

TheoremErdős Problem 823#

References: - erdosproblems.com/823 - [Er59c] Erdős, P., Remarks on number theory. II. Some problems on the \(\sigma\) function. Acta Arith. (1959), 171--177. - [Er74b] Erdős, P., Remarks on some problems in number theory. Math. Balkanica (1974), 197-202. - [Po15b] Pollack, Paul, Remarks on fibers of the sum-of-divisors function. Analytic number theory, Springer, Cham (2015), 305-320.

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

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

Erdos823.erdos_823

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

Let \(\alpha\geq 1\). Is there a sequence of integers \(n_k,m_k\) such that \(n_k/m_k\to \alpha\) and \(\sigma(n_k)=\sigma(m_k)\) for all \(k\geq 1\), where \(\sigma\) is the sum of divisors function?

The answer is yes, proved by Pollack [Po15b].

We take \(n_k\) and \(m_k\) to be positive integers.

theorem erdos_823 : ∀ α : ℝ, 1 ≤ α →
    ∃ n m : ℕ → ℕ, (∀ k, 0 < n k) ∧ (∀ k, 0 < m k) ∧ (∀ k, σ 1 (n k) = σ 1 (m k)) ∧
      Tendsto (fun k ↦ (n k : ℝ) / m k) atTop (𝓝 α)

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

Erdos823.erdos_823.variants.totient

Solved: stated here without proof.

For every \(\alpha\geq 1\) there are sequences of integers \(n_k,m_k\) such that \(n_k/m_k\to \alpha\) and \(\phi(n_k)=\phi(m_k)\) for all \(k\geq 1\). Erdős [Er74b] writes it is 'easy to prove the analogous result for \(\phi(n)\)'.

theorem erdos_823.variants.totient : ∀ α : ℝ, 1 ≤ α →
    ∃ n m : ℕ → ℕ, (∀ k, 0 < n k) ∧ (∀ k, 0 < m k) ∧ (∀ k, φ (n k) = φ (m k)) ∧
      Tendsto (fun k ↦ (n k : ℝ) / m k) atTop (𝓝 α)

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

Sources

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

LeanErdos823.erdos_823 · Erdos823.erdos_823.variants.totient

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.