Erdős Problem 748 to Erdős Problem 772

TheoremErdős Problem 748#

References: - erdosproblems.com/748 - [CaEr90] Cameron, P. J. and Erdős, P., On the number of sets of integers with various properties. (1990), 61-79. - [Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269. - [Er98] Erdős, Paul, Some of my new and almost new problems and results in combinatorial number theory. Number theory (Eger, 1996) (1998), 169-180. - [Gr04] Green, Ben, The Cameron-Erdős conjecture. Bull. London Math. Soc. (2004), 769-778. - [Sa03] Sapozhenko, A. A., The Cameron-Erdős conjecture. Dokl. Akad. Nauk (2003), 749-752.

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

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

Erdos748.erdos_748

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

Let \(f(n)\) count the number of sum-free \(A\subseteq \{1,\ldots,n\}\), i.e. \(A\) contains no solutions to \(a=b+c\) with \(a,b,c\in A\). Is it true that

\[f(n)=2^{(1+o(1))\frac{n}{2}}?\]

The Cameron–Erdős conjecture. This is true, and in fact \(f(n) \ll 2^{n/2}\), which was proved independently by Green [Gr04] and Sapozhenko [Sa03].

The statement \(f(n)=2^{(1+o(1))n/2}\) is formalised as \(\log_2 f(n)/n\to 1/2\).

theorem erdos_748 :
    Tendsto (fun n : ℕ ↦ logb 2 (f n) / n) atTop (nhds (1 / 2))

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

Erdos748.erdos_748.variants.lower_bound

Textbook result, stated without proof.

It is trivial to see that \(f(n) \geq 2^{\frac{n}{2}}\), considering all subsets of \((n/2,n]\). The source writes \([n/2,n]\), but for even \(n\) that interval is not sum-free, since \(n/2 + n/2 = n\).

theorem erdos_748.variants.lower_bound (n : ℕ) :
    (2 : ℝ) ^ ((n : ℝ) / 2) ≤ (f n : ℝ)

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

Erdos748.erdos_748.variants.green_sapozhenko

Solved: stated here without proof.

Green [Gr04] and Sapozhenko [Sa03] proved that \(f(n) \ll 2^{n/2}\).

theorem erdos_748.variants.green_sapozhenko :
    ∃ C : ℝ, ∀ n : ℕ, (f n : ℝ) ≤ C * 2 ^ ((n : ℝ) / 2)

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

Erdos748.erdos_748.variants.asymptotic

Solved: stated here without proof.

In fact, both Green [Gr04] and Sapozhenko [Sa03] prove the stronger asymptotic \(f(n) \sim c_n 2^{n/2}\), where \(c_n\) takes on one of two values depending on the parity of \(n\).

theorem erdos_748.variants.asymptotic :
    ∃ c₀ c₁ : ℝ, 0 < c₀ ∧ 0 < c₁ ∧
      Tendsto (fun m : ℕ ↦ (f (2 * m) : ℝ) / 2 ^ m) atTop (nhds c₀) ∧
      Tendsto (fun m : ℕ ↦ (f (2 * m + 1) : ℝ) / 2 ^ ((2 * m + 1 : ℝ) / 2)) atTop
        (nhds c₁)

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

Sources

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

LeanErdos748.erdos_748 · Erdos748.erdos_748.variants.lower_bound · Erdos748.erdos_748.variants.green_sapozhenko · Erdos748.erdos_748.variants.asymptotic

TheoremErdős Problem 749#

Reference: erdosproblems.com/749

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

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

Erdos749.erdos_749

Open: stated without proof.

Let \(\epsilon>0\). Does there exist \(A\subseteq \mathbb{N}\) such that the lower density of \(A+A\) is at least \(1-\epsilon\) and yet \(1_A\ast 1_A(n) \ll_\epsilon 1\) for all \(n\)?

theorem erdos_749 : ∀ ε > (0 : ℝ),
    ∃ A : Set ℕ, 1 - ε ≤ lowerDensity (A + A) ∧
    ((Nat.cast (R := ℝ) ∘ sumRep A) ≪ (fun n => (1: ℝ)))

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

Sources

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

LeanErdos749.erdos_749

TheoremErdős Problem 750#

References: - erdosproblems.com/750 - [EHS82] Erdős, P. and Hajnal, A. and Szemerédi, E., On almost bipartite large chromatic graphs. Theory and practice of combinatorics (1982), 117-123. - [Er69b] Erdős, P., Problems and results in chromatic graph theory. Proof Techniques in Graph Theory (1969), 27-35. - [Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269. - [Er95d] Erdős, Paul, On some problems in combinatorial set theory. Publ. Inst. Math. (Beograd) (N.S.) (1995), 61-65. - [ErHa67b] Erdős, P. and Hajnal, András, On chromatic graphs. Mat. Lapok (1967), 1--4. - UlamErdos750 - [St85] Stiebitz, M., Beiträge zur Theorie der färbungskritischen Graphen. Habilitation, TH Ilmenau (1985). - [SaSt89] Sachs, H. and Stiebitz, M., On constructive methods in the theory of colour-critical graphs. Discrete Math. (1989), 287-296. - [MuSt19] Müller, T. and Stehlík, M., Generalised Mycielski graphs and the Borsuk-Ulam theorem. Electron. J. Combin. (2019), P4.8.

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

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

Erdos750.erdos_750.variants.stiebitz

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

Stiebitz's theorem [St85]: every graph in \(M_r\) has chromatic number at least \(r\). The matching upper bound follows from the construction, so the chromatic number is exactly \(r\).

See also [SaSt89] and [MuSt19].

The linked formal proof (Alexeev and Codex, via signed-biclique chains and a ℤ_p-Tucker lemma) uses the same IsRecursivelyBuiltMr, except that its genMyc s G has MycAdj s G directly as adjacency relation instead of SimpleGraph.fromRel (MycAdj s G); the two graphs are equal since MycAdj is symmetric and irreflexive.

theorem erdos_750.variants.stiebitz {V : Type u} (G : SimpleGraph V) (r : ℕ)
    (h : IsRecursivelyBuiltMr r G) : (r : ℕ∞) ≤ G.chromaticNumber

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

Erdos750.erdos_750

Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/main/problems/750/Erdos750.lean; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos750.lean#L50.

Let \(f(m)\) be some function such that \(f(m)\to \infty\) as \(m\to \infty\). Does there exist a graph \(G\) of infinite chromatic number such that every subgraph on \(m\) vertices contains an independent set of size at least \(\frac{m}{2}-f(m)\)?

Note that in [Er94b] the function \(f\) generalises a (proven) result for \(f(m) = \epsilon m\), where \(\epsilon > 0\). Hence we should assume it is non-negative valued.

The existence of such a graph was proved [UlamErdos750] by GPT 5.5 Pro (prompted by Chojecki). Indeed, this constructs a graph with infinite chromatic number such that every subgraph on \(m\) vertices can be made bipartite after deleting at most \(f(m)\) many vertices.

The proof in plby/lean-proofs uses the proof of erdos_750.variants.stiebitz linked above. It produces a graph on a V : Type, which gives the statement below in any universe by lifting V.

theorem erdos_750 :
    ∀ (f : ℕ → ℝ≥0) (hf : atTop.Tendsto f atTop),
      ∃ (V : Type*) (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧
        ∀ (m : ℕ) (S : Set V), 0 < m → S.ncard = m →
          ∃ I ⊆ S, G.IsIndepSet I ∧ m / 2 - f m ≤ I.ncard

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

Erdos750.erdos_750.variants.epsilon

Solved: stated here without proof.

In [Er69b] Erdős conjectures this for \(f(m)=\epsilon m\) for any fixed \(\epsilon>0\). This follows from a result of Erdős, Hajnal, and Szemerédi [EHS82], as described by Sellke in the comments.

theorem erdos_750.variants.epsilon :
    ∀ (ε : ℝ≥0), ε > 0 →
      ∃ (V : Type*) (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧
        ∀ (m : ℕ) (S : Set V), 0 < m → S.ncard = m →
          ∃ I ⊆ S, G.IsIndepSet I ∧ m / 2 - ε * m ≤ I.ncard

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

Erdos750.erdos_750.variants.c_gt_quarter

Solved: stated here without proof.

In [ErHa67b] Erdős and Hajnal prove this for \(f(m)\geq cm\) for all \(c>1/4\).

theorem erdos_750.variants.c_gt_quarter :
    ∀ (c : ℝ≥0), c > 1 / 4 →
      ∃ (V : Type*) (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧
        ∀ (m : ℕ) (S : Set V), 0 < m → S.ncard = m →
          ∃ I ⊆ S, G.IsIndepSet I ∧ m / 2 - c * m ≤ I.ncard

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

Sources

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

LeanErdos750.erdos_750.variants.stiebitz · Erdos750.erdos_750 · Erdos750.erdos_750.variants.epsilon · Erdos750.erdos_750.variants.c_gt_quarter

TheoremErdős Problem 751#

References: - erdosproblems.com/751 - [Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261--269. - [BoVi98] Bondy, J. A. and Vince, A., Cycles in a graph whose lengths differ by one or two. J. Graph Theory (1998), 11--15.

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

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

Erdos751.erdos_751.parts.i

Solved: stated here without proof.

Let \(G\) be a graph with chromatic number \(\chi(G)=4\). If \(m_1\lt m_2\lt \cdots\) are the lengths of the cycles in \(G\) then can \(\min(m_{i+1}-m_i)\) be arbitrarily large?

The answer is no: Bondy and Vince [BoVi98] proved that every graph with minimum degree at least \(3\) has two cycles whose lengths differ by at most \(2\), and hence the same is true for every graph with chromatic number \(4\).

erdos_751.variants.finite below carries the Lean proof. It assumes a finite vertex type, where this quantifies over any V : Type, and the two are joined by de Bruijn-Erdős: a graph that is not \(3\)-colourable has a finite subgraph that is not \(3\)-colourable, and cycles of that subgraph are cycles of the whole. Mathlib does not have de Bruijn-Erdős, so that step is not formalised here.

theorem erdos_751.parts.i :
    ¬ ∀ k : ℕ, ∃ (V : Type) (G : SimpleGraph V), G.chromaticNumber = 4 ∧
      ∀ m ∈ G.cycleLengths, ∀ m' ∈ G.cycleLengths, m < m' → m + k ≤ m'

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

Erdos751.erdos_751.parts.ii

Solved: stated here without proof.

Let \(G\) be a graph with chromatic number \(\chi(G)=4\). If \(m_1\lt m_2\lt \cdots\) are the lengths of the cycles in \(G\) then can \(\min(m_{i+1}-m_i)\) be arbitrarily large? Can this happen if the girth of \(G\) is large?

The answer is no: Bondy and Vince [BoVi98] proved that every graph with minimum degree at least \(3\) has two cycles whose lengths differ by at most \(2\), and hence the same is true for every graph with chromatic number \(4\).

theorem erdos_751.parts.ii :
    ¬ ∀ k g : ℕ, ∃ (V : Type) (G : SimpleGraph V), G.chromaticNumber = 4 ∧ g ≤ G.girth ∧
      ∀ m ∈ G.cycleLengths, ∀ m' ∈ G.cycleLengths, m < m' → m + k ≤ m'

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

Erdos751.erdos_751.variants.bondy_vince

Solved: stated here without proof.

Bondy and Vince [BoVi98] proved that every graph with minimum degree at least \(3\) has two cycles whose lengths differ by at most \(2\).

theorem erdos_751.variants.bondy_vince {V : Type*} [Fintype V] (G : SimpleGraph V)
    [DecidableRel G.Adj] (hG : 3 ≤ G.minDegree) :
    ∃ m ∈ G.cycleLengths, ∃ m' ∈ G.cycleLengths, m < m' ∧ m' ≤ m + 2

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

Erdos751.erdos_751.variants.finite

Solved: stated here; a Lean proof is at https://github.com/SpringSense-Innovation-Institute/ai-for-math-lean/blob/ae3ead960a494cf81b28541c477e50997cb03999/erdos-problems/erdos751/Erdos751/Main.lean#L40-L69.

The finite case of erdos_751.parts.i, which is what the Lean proof establishes: a finite graph with chromatic number at least \(4\) has two cycles whose lengths differ by \(1\) or \(2\).

The proof reaches this through a \(4\)-critical subgraph, which supplies the \(2\)-connectivity and the vertex count its Bondy-Vince step needs on top of minimum degree \(3\). Those extra hypotheses are why it does not also settle erdos_751.variants.bondy_vince, which asks for minimum degree \(3\) alone.

This was formalized in Lean by SpringSense Innovation Institute using ChatGPT.

theorem erdos_751.variants.finite {V : Type*} [Fintype V] (G : SimpleGraph V)
    [DecidableRel G.Adj] (hG : (4 : ℕ∞) ≤ G.chromaticNumber) :
    ∃ m ∈ G.cycleLengths, ∃ m' ∈ G.cycleLengths, m < m' ∧ m' ≤ m + 2

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

Sources

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

LeanErdos751.erdos_751.parts.i · Erdos751.erdos_751.parts.ii · Erdos751.erdos_751.variants.bondy_vince · Erdos751.erdos_751.variants.finite

TheoremErdős Problem 753#

References: - erdosproblems.com/753 - [Al92] Alon, Noga, Choice numbers of graphs: a probabilistic approach. Combin. Probab. Comput. (1992), 107-114.

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

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

Erdos753.erdos_753

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

The list chromatic number \(\chi_L(G)\) is defined to be the minimal \(k\) such that for any assignment of a list of \(k\) colours to each vertex of \(G\) (perhaps different lists for different vertices) a colouring of each vertex by a colour on its list can be chosen such that adjacent vertices receive distinct colours.

Does there exist some constant \(c>0\) such that

\[\chi_L(G)+\chi_L(G^c)> n^{1/2+c}\]

for every graph \(G\) on \(n\) vertices (where \(G^c\) is the complement of \(G\))?

A problem of Erdős, Rubin, and Taylor.

The answer is no: Alon [Al92] proved that, for every \(n\), there exists a graph \(G\) on \(n\) vertices such that

\[\chi_L(G)+\chi_L(G^c)\ll (n\log n)^{1/2},\]

where the implied constant is absolute.

theorem erdos_753 :
    ¬ ∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 0 < n → ∀ G : SimpleGraph (Fin n),
      (n : ℝ) ^ ((1 : ℝ) / 2 + c) <
        (listChromaticNumber G : ℝ) + (listChromaticNumber Gᶜ : ℝ)

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

Erdos753.erdos_753.variants.alon

Solved: stated here without proof.

Alon [Al92] proved that, for every \(n\), there exists a graph \(G\) on \(n\) vertices such that

\[\chi_L(G)+\chi_L(G^c)\ll (n\log n)^{1/2},\]

where the implied constant is absolute.

theorem erdos_753.variants.alon :
    ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 2 ≤ n → ∃ G : SimpleGraph (Fin n),
      (listChromaticNumber G : ℝ) + (listChromaticNumber Gᶜ : ℝ) ≤
        C * ((n : ℝ) * Real.log (n : ℝ)) ^ ((1 : ℝ) / 2)

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

Sources

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

LeanErdos753.erdos_753 · Erdos753.erdos_753.variants.alon

TheoremErdős Problem 755#

References: - erdosproblems.com/755 - [ErPu75] Erdős, Paul and Purdy, George, Some extremal problems in geometry. III. (1975), 291--308. - [Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261--269. - [CDL25b] Clemen, Felix Christian, Dumitrescu, Adrian, and Liu, Dingyuan, The number of regular simplices in higher dimensions. arXiv:2507.19841 (2025).

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

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

Erdos755.erdos_755

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

Erdős asked whether every \(n\)-point set in \(\mathbb{R}^6\) spans at most \((1/27 + o(1)) n^3\) unit equilateral triangles.

Clemen, Dumitrescu, and Liu [CDL25b] proved the stronger any-size statement \(T_6(n) = (1/27 + o(1)) n^3\). The unit-triangle upper bound follows as a corollary, since unit equilateral triangles are a subset of equilateral triangles of any positive side length: \(T_\mathrm{unit} \leq T_\mathrm{anysize}\).

theorem erdos_755 :
    ∃ o : ℕ → ℝ,
      o =o[atTop] (fun _ : ℕ => (1 : ℝ)) ∧
        ∀ᶠ n in atTop,
          (TUnit 6 n : ℝ) ≤ ((1 / 27 : ℝ) + o n) * (n : ℝ) ^ 3

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/755.lean, line 94.

Erdos755.erdos_755.variants.any_size_cdl

Solved: stated here without proof.

Clemen, Dumitrescu, and Liu [CDL25b] proved the stronger version where equilateral triangles of all positive side lengths are counted.

theorem erdos_755.variants.any_size_cdl :
    (fun n : ℕ => (TAnySize 6 n : ℝ)) ~[atTop]
      (fun n : ℕ => (1 / 27 : ℝ) * (n : ℝ) ^ 3)

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/755.lean, line 106.

Sources

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

LeanErdos755.erdos_755 · Erdos755.erdos_755.variants.any_size_cdl

TheoremErdős Problem 756#

References: - erdosproblems.com/756 - [Bh24] Bhowmick, K., A problem of Erdős about rich distances. arXiv:2407.01174 (2024). - [CDL25] Clemen, F., Dumitrescu, A. and Liu, D., On multiplicities of interpoint distances. arXiv:2505.04283 (2025). - [Er97b] Erdős, Paul, Some old and new problems in various branches of combinatorics. Discrete Math. (1997), 227-231. - [ErPa90] Erdős, P. and Pach, J., Variations on the theme of repeated distances. Combinatorica (1990), 261-269. - [HoPa34] Hopf, H. and Pannwitz, E., Aufgabe 167. Jber. Deutsch. Math. Verein. (1934), 114.

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

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

Erdos756.erdos_756

Solved: stated here without proof.

Let \(A\subset \mathbb{R}^2\) be a set of \(n\) points. Can there be \(\gg n\) many distinct distances each of which occurs for more than \(n\) many pairs from \(A\)?

The answer is yes: Bhowmick [Bh24] constructs a set of \(n\) points in \(\mathbb{R}^2\) such that \(\lfloor\frac{n}{4}\rfloor\) distances occur at least \(n+1\) times.

theorem erdos_756 :
    (fun n : ℕ => (n : ℝ)) =O[atTop] (fun n : ℕ => (maxRichDistances n : ℝ))

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/756.lean, line 59.

Erdos756.erdos_756.variants.bhowmick

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

Bhowmick [Bh24] constructs a set of \(n\) points in \(\mathbb{R}^2\) such that \(\lfloor\frac{n}{4}\rfloor\) distances occur at least \(n+1\) times.

theorem erdos_756.variants.bhowmick (n : ℕ) :
    ∃ A : Finset ℝ², A.card = n ∧ n / 4 ≤ (richDistances A (n + 1)).card

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/756.lean, line 69.

Erdos756.erdos_756.variants.bhowmick_general

Solved: stated here without proof.

More generally, they construct, for any positive integer \(m\) and large \(n\), a set of \(n\) points such that \(\lfloor \frac{n}{2(m+1)}\rfloor\) distances occur at least \(n+m\) times.

theorem erdos_756.variants.bhowmick_general (m : ℕ) (hm : 1 ≤ m) :
    ∀ᶠ n : ℕ in atTop, ∃ A : Finset ℝ², A.card = n ∧
      n / (2 * (m + 1)) ≤ (richDistances A (n + m)).card

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/756.lean, line 79.

Sources

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

LeanErdos756.erdos_756 · Erdos756.erdos_756.variants.bhowmick · Erdos756.erdos_756.variants.bhowmick_general

TheoremErdős Problem 757#

References: - erdosproblems.com/757 - [GyLe95] Gyárfás, András and Lehel, Jenő, Linear sets with five distinct differences among any four elements. J. Combin. Theory Ser. B (1995), 108-118.

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

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

Erdos757.erdos_757

Open: stated without proof.

What is the supremum of the set of admissible numbers?

theorem erdos_757 {A : Set ℝ} :
    erdos_757.answer = sSup {c | IsAdmissible c}

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

Erdos757.erdos_757.variants.lowerBound

Solved: stated here without proof.

The supremum is strictly larger than 1 / 2, which is proved in [GyLe95].

theorem erdos_757.variants.lowerBound {A : Set ℝ} : 1 / (2 : ℝ) < sSup {c | IsAdmissible c}

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

Erdos757.erdos_757.variants.upperBound

Solved: stated here without proof.

In [GyLe95], the authors also prove that the supremum is smaller than 3 / 5.

theorem erdos_757.variants.upperBound {A : Set ℝ} : sSup {c | IsAdmissible c} < 3 / (5 : ℝ)

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

Sources

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

LeanErdos757.erdos_757 · Erdos757.erdos_757.variants.lowerBound · Erdos757.erdos_757.variants.upperBound

TheoremErdős Problem 760#

References: - erdosproblems.com/760 - [AKS97] Alon, Noga and Krivelevich, Michael and Sudakov, Benny, Subgraphs with a large cochromatic number. J. Graph Theory (1997), 295-297.

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

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

Erdos760.erdos_760

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

The cochromatic number of \(G\), denoted by \(\zeta(G)\), is the minimum number of colours needed to colour the vertices of \(G\) such that each colour class induces either a complete graph or independent set.

If \(G\) is a graph with chromatic number \(\chi(G)=m\) then must \(G\) contain a subgraph \(H\) with

\[ \zeta(H) \gg \frac{m}{\log m}? \]

A problem of Erdős and Gimbel, who proved that there must exist a subgraph \(H\) with

\[ \zeta(H) \gg \left(\frac{m}{\log m}\right)^{1/2}. \]

The proposed bound would be best possible, as shown by taking \(G\) to be a complete graph.

The answer is yes, proved by Alon, Krivelevich, and Sudakov.

theorem erdos_760 :
    ∃ c > (0 : ℝ), ∀ (V : Type*) [Finite V] (G : SimpleGraph V) (m : ℕ),
      G.chromaticNumber = (m : ℕ∞) →
        ∃ H : G.Subgraph, ∃ k : ℕ, ((k : ℕ∞) ≤ H.coe.cochromaticNumber) ∧
          (c * (m : ℝ) / Real.log (m : ℝ) ≤ (k : ℝ))

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

Erdos760.erdos_760.variants.erdos_gimbel

Solved: stated here without proof.

A problem of Erdős and Gimbel, who proved that there must exist a subgraph \(H\) with

\[ \zeta(H) \gg \left(\frac{m}{\log m}\right)^{1/2}. \]

theorem erdos_760.variants.erdos_gimbel :
    ∃ c > (0 : ℝ), ∀ (V : Type*) [Finite V] (G : SimpleGraph V) (m : ℕ),
      G.chromaticNumber = (m : ℕ∞) →
        ∃ H : G.Subgraph, ∃ k : ℕ, ((k : ℕ∞) ≤ H.coe.cochromaticNumber) ∧
          (c * Real.sqrt ((m : ℝ) / Real.log (m : ℝ)) ≤ (k : ℝ))

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

Sources

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

LeanErdos760.erdos_760 · Erdos760.erdos_760.variants.erdos_gimbel

TheoremErdős Problem 761#

References: - erdosproblems.com/761 - [ErGi93] Erdős, P. and Gimbel, J., Some problems and results in cochromatic theory. Quo vadis, graph theory? (1993), 261-264.

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

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

Erdos761.erdos_761.parts.i

Open: stated without proof.

The dichromatic number of \(G\), denoted by \(\delta(G)\), is the minimum number \(k\) of colours required such that, in any orientation of the edges of \(G\), there is a \(k\)-colouring of the vertices of \(G\) such that there are no monochromatic oriented cycles.

Must a graph with large chromatic number have large dichromatic number?

This question is due to Erdős and Neumann-Lara. We read it for finite graphs: for every \(k\) there is \(m\) such that every finite graph with \(\chi(G)\geq m\) has \(\delta(G)\geq k\).

theorem erdos_761.parts.i :
    ∀ k : ℕ, ∃ m : ℕ, ∀ (V : Type*) [Finite V] (G : SimpleGraph V),
      (m : ℕ∞) ≤ G.chromaticNumber → (k : ℕ∞) ≤ dichromaticNumber G

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

Erdos761.erdos_761.parts.ii

Open: stated without proof.

The cochromatic number of \(G\), denoted by \(\zeta(G)\), is the minimum number of colours needed to colour the vertices of \(G\) such that each colour class induces either a complete graph or empty graph.

Must a graph with large cochromatic number contain a graph with large dichromatic number?

This question is due to Erdős and Gimbel. We read it for finite graphs and subgraphs: for every \(k\) there is \(m\) such that every finite graph with \(\zeta(G)\geq m\) has a subgraph \(H\) with \(\delta(H)\geq k\).

theorem erdos_761.parts.ii :
    ∀ k : ℕ, ∃ m : ℕ, ∀ (V : Type*) [Finite V] (G : SimpleGraph V),
      (m : ℕ∞) ≤ G.cochromaticNumber →
        ∃ H : G.Subgraph, (k : ℕ∞) ≤ dichromaticNumber H.coe

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

Erdos761.erdos_761.variants.parts_ii_imp_i

Solved: stated here without proof.

A positive answer to the second question implies a positive answer to the first via the bound mentioned in [760].

theorem erdos_761.variants.parts_ii_imp_i :
    (∀ k : ℕ, ∃ m : ℕ, ∀ (V : Type u) [Finite V] (G : SimpleGraph V),
      (m : ℕ∞) ≤ G.cochromaticNumber →
        ∃ H : G.Subgraph, (k : ℕ∞) ≤ dichromaticNumber H.coe) →
    ∀ k : ℕ, ∃ m : ℕ, ∀ (V : Type u) [Finite V] (G : SimpleGraph V),
      (m : ℕ∞) ≤ G.chromaticNumber → (k : ℕ∞) ≤ dichromaticNumber G

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

Sources

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

LeanErdos761.erdos_761.parts.i · Erdos761.erdos_761.parts.ii · Erdos761.erdos_761.variants.parts_ii_imp_i

TheoremErdős Problem 762#

References: - erdosproblems.com/762 - [EGS90] Erdős, Paul and Gimbel, John and Straight, H. Joseph, Chromatic number versus cochromatic number in graphs with bounded clique number. European J. Combin. (1990), 235-240. - [St24b] R. Steiner, On the difference between the chromatic and cochromatic number. arXiv:2408.02400 (2024).

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

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

Erdos762.erdos_762

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

The cochromatic number of \(G\), denoted by \(\zeta(G)\), is the minimum number of colours needed to colour the vertices of \(G\) such that each colour class induces either a complete graph or empty graph.

Is it true that if \(G\) has no \(K_5\) and \(\zeta(G)\geq 4\) then \(\chi(G) \leq \zeta(G)+2\)?

This has been disproved by Steiner [St24b], who constructed a graph \(G\) with \(\omega(G)=4\), \(\zeta(G)=4\), and \(\chi(G)=7\).

theorem erdos_762 :
    ¬ ∀ (V : Type*) [Fintype V] (G : SimpleGraph V),
      G.CliqueFree 5 → 4 ≤ G.cochromaticNumber →
        G.chromaticNumber ≤ G.cochromaticNumber + 2

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

Erdos762.erdos_762.variants.bounded_clique_number

Solved: stated here without proof.

A conjecture of Erdős, Gimbel, and Straight [EGS90], who proved that for every \(n>2\) there exists some \(f(n)\) such that if \(G\) contains no clique on \(n\) vertices then \(\chi(G)\leq \zeta(G)+f(n)\).

theorem erdos_762.variants.bounded_clique_number (n : ℕ) (hn : 2 < n) :
    ∃ f : ℕ, ∀ (V : Type*) [Fintype V] (G : SimpleGraph V),
      G.CliqueFree n → G.chromaticNumber ≤ G.cochromaticNumber + f

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

Erdos762.erdos_762.variants.steiner

Solved: stated here without proof.

This has been disproved by Steiner [St24b], who constructed a graph \(G\) with \(\omega(G)=4\), \(\zeta(G)=4\), and \(\chi(G)=7\).

theorem erdos_762.variants.steiner :
    ∃ (n : ℕ) (G : SimpleGraph (Fin n)),
      G.cliqueNum = 4 ∧ G.cochromaticNumber = 4 ∧ G.chromaticNumber = 7

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

Sources

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

LeanErdos762.erdos_762 · Erdos762.erdos_762.variants.bounded_clique_number · Erdos762.erdos_762.variants.steiner

TheoremErdős Problem 763#

References: - erdosproblems.com/763 - [Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244. - [Er70c] Erdős, P., Some problems in additive number theory. Amer. Math. Monthly (1970), 619-621. - [ErFu56] Erdős, P. and Fuchs, W. H. J., On a problem of additive number theory. J. London Math. Soc. (1956), 67-73. - [MoVa90] Montgomery, H. L. and Vaughan, R. C., On the Erdős-Fuchs theorems. (1990), 331-338.

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

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

Erdos763.erdos_763

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

Let \(A\subseteq \mathbb{N}\). Can there exist some constant \(c>0\) such that

\[\sum_{n\leq N} 1_A\ast 1_A(n) = cN+O(1)?\]

A conjecture of Erdős and Turán. Erdős and Fuchs [ErFu56] proved that the answer is no in a strong form: in fact even

\[\sum_{n\leq N} 1_A\ast 1_A(n) = cN+o\left(\frac{N^{1/4}}{(\log N)^{1/2}}\right)\]

is impossible. The error term here was improved to \(o(N^{1/4})\) by Jurkat (unpublished) and Montgomery and Vaughan [MoVa90].

See also 764 for a generalisation to more summands.

theorem erdos_763 : ¬ ∃ (A : Set ℕ) (c : ℝ), 0 < c ∧
    (fun N : ℕ ↦ (∑ n ∈ Finset.range (N + 1), sumRep A n : ℝ) - c * N) =O[atTop]
      fun _ ↦ (1 : ℝ)

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

Erdos763.erdos_763.variants.erdos_fuchs

Solved: stated here without proof.

Erdős and Fuchs [ErFu56] proved that \(\sum_{n\leq N} 1_A\ast 1_A(n) = cN+o\left(\frac{N^{1/4}}{(\log N)^{1/2}}\right)\) is impossible.

theorem erdos_763.variants.erdos_fuchs : ¬ ∃ (A : Set ℕ) (c : ℝ), 0 < c ∧
    (fun N : ℕ ↦ (∑ n ∈ Finset.range (N + 1), sumRep A n : ℝ) - c * N) =o[atTop]
      fun N ↦ (N : ℝ) ^ (1 / 4 : ℝ) / √(Real.log N)

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

Erdos763.erdos_763.variants.montgomery_vaughan

Solved: stated here without proof.

Jurkat (unpublished) and Montgomery and Vaughan [MoVa90] proved that even \(\sum_{n\leq N} 1_A\ast 1_A(n) = cN+o(N^{1/4})\) is impossible.

theorem erdos_763.variants.montgomery_vaughan : ¬ ∃ (A : Set ℕ) (c : ℝ), 0 < c ∧
    (fun N : ℕ ↦ (∑ n ∈ Finset.range (N + 1), sumRep A n : ℝ) - c * N) =o[atTop]
      fun N ↦ (N : ℝ) ^ (1 / 4 : ℝ)

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

Sources

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

LeanErdos763.erdos_763 · Erdos763.erdos_763.variants.erdos_fuchs · Erdos763.erdos_763.variants.montgomery_vaughan

TheoremErdős Problem 764#

References: - erdosproblems.com/764 - [Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244. - [Er70c] Erdős, P., Some problems in additive number theory. Amer. Math. Monthly (1970), 619-621. - [Va72] Vaughan, R. C., On the addition of sequences of integers. J. Number Theory (1972), 1-16.

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

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

Erdos764.erdos_764

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

Let \(A\subseteq \mathbb{N}\). Can there exist some constant \(c>0\) such that

\[\sum_{n\leq N} 1_A\ast 1_A\ast 1_A(n) = cN+O(1)?\]

The case of \(1_A\ast 1_A(n)\) is the subject of 763.

The answer is no, proved in a strong form by Vaughan [Va72], who showed that in fact

\[\sum_{n\leq N} 1_A\ast 1_A\ast 1_A(n) = cN+o\left(\frac{N^{1/4}}{(\log N)^{1/2}}\right)\]

is impossible. Vaughan proves a more general result that applies to any \(h\)-fold convolution, with different main terms permitted.

theorem erdos_764 : ¬ ∃ (A : Set ℕ) (c : ℝ), 0 < c ∧
    (fun N : ℕ ↦ (∑ n ∈ Finset.range (N + 1), tripleRep A n : ℝ) - c * N) =O[atTop]
      fun _ ↦ (1 : ℝ)

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

Erdos764.erdos_764.variants.vaughan

Solved: stated here without proof.

Vaughan [Va72] showed that \(\sum_{n\leq N} 1_A\ast 1_A\ast 1_A(n) = cN+o\left(\frac{N^{1/4}}{(\log N)^{1/2}}\right)\) is impossible.

theorem erdos_764.variants.vaughan : ¬ ∃ (A : Set ℕ) (c : ℝ), 0 < c ∧
    (fun N : ℕ ↦ (∑ n ∈ Finset.range (N + 1), tripleRep A n : ℝ) - c * N) =o[atTop]
      fun N ↦ (N : ℝ) ^ (1 / 4 : ℝ) / √(Real.log N)

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

Sources

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

LeanErdos764.erdos_764 · Erdos764.erdos_764.variants.vaughan

TheoremErdős Problem 765#

References: - erdosproblems.com/765 - [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. - [Re58] Reiman, I., Über ein Problem von K. Zarankiewicz. Acta Math. Acad. Sci. Hungar. 9 (1958), 269-273. - [ERS66] Erdős, P. and Rényi, A. and Sós, V. T., On a problem of graph theory. Studia Sci. Math. Hungar. (1966), 215--235. - [Br66] Brown, W. G., On graphs that do not contain a Thomsen graph. Canad. Math. Bull. (1966), 281-285. - [Er75] Erdős, P., Some recent progress on extremal problems in graph theory. Congr. Numer. (1975), 3-14. - [Fu83] Füredi, Z., Graphs without quadrilaterals. J. Combin. Theory Ser. B 34 (1983), 187-190. - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350. - [MaYa23] Ma, Jie and Yang, Tianchi, Upper bounds on the extremal number of the 4-cycle. Bull. Lond. Math. Soc. (2023), 1655--1667.

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

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

Erdos765.erdos_765

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

Give an asymptotic formula for \(\mathrm{ex}(n; C_4)\).

Erdős and Klein [Er38] proved \(\mathrm{ex}(n; C_4) \asymp n^{3/2}\), and Reiman [Re58] proved

\[\frac{1}{2\sqrt 2} \le \lim \frac{\mathrm{ex}(n; C_4)}{n^{3/2}} \le \frac12.\]

Erdős and Rényi [ERS66], and independently Brown [Br66], gave a construction showing that if \(n = q^2 + q + 1\) with \(q\) a prime power then \(\mathrm{ex}(n; C_4) \ge \frac12 q (q+1)^2\); together with Reiman's upper bound this gives \(\mathrm{ex}(n; C_4) \sim \frac12 n^{3/2}\). Füredi [Fu83] proved \(\mathrm{ex}(n; C_4) = \frac12 q (q+1)^2\) for \(q > 13\).

theorem erdos_765 :
    (fun n : ℕ ↦ (SimpleGraph.extremalNumber n (SimpleGraph.cycleGraph 4) : ℝ)) ~[atTop]
      fun n : ℕ ↦ (n : ℝ) ^ (3 / 2 : ℝ) / 2

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

Erdos765.erdos_765.variants.second_term

Solved: stated here without proof.

Erdős [Er93] conjectured that \(\mathrm{ex}(n; C_4) = \frac{n^{3/2}}{2} + \frac n4 + O(n^{1/2})\) for all \(n\), having proved the upper bound \(\mathrm{ex}(n; C_4) \le \frac{n^{3/2}}{2} + \frac n4 + O(n^{1/2})\) in [Er75]. This is false: Ma and Yang [MaYa23] proved that, for some absolute constant \(c > 0\) and a positive density set of \(n\), \(\mathrm{ex}(n; C_4) \le \frac{n^{3/2}}{2} + (\frac14 - c) n\).

theorem erdos_765.variants.second_term :
    ¬ (fun n : ℕ ↦ (SimpleGraph.extremalNumber n (SimpleGraph.cycleGraph 4) : ℝ) -
      (n : ℝ) ^ (3 / 2 : ℝ) / 2 - (n : ℝ) / 4) =O[atTop] fun n : ℕ ↦ (n : ℝ) ^ (1 / 2 : ℝ)

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

Sources

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

LeanErdos765.erdos_765 · Erdos765.erdos_765.variants.second_term

TheoremErdős Problem 766#

References: - erdosproblems.com/766 - [Er64c] Erdős, P., Extremal problems in graph theory. Theory of Graphs and its Applications (Proc. Sympos. Smolenice, 1963) (1964), 29-36. PDF

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

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

Erdos766.erdos_766.parts.i

Open: stated without proof.

Let \(f(n;k,l)=\min \mathrm{ex}(n;G)\), where \(G\) ranges over all graphs with \(k\) vertices and \(l\) edges.

Give good estimates for \(f(n;k,l)\) in the range \(k\lt l\leq k^2/4\).

In [Er64c, p. 33] this question is asked for \(f_1(n;k,l)\) (Erdos766.forcingNumber), which forces at least one graph with \(k\) vertices and \(l\) edges rather than one fixed graph; we follow the source. The question for the function of erdosproblems.com is Erdos766.erdos_766.variants.minExtremalNumber_estimate.

theorem erdos_766.parts.i :
    ∀ k l : ℕ, k < l → l ≤ k ^ 2 / 4 →
      (fun n ↦ (forcingNumber n k l : ℝ)) =Θ[atTop] erdos_766.parts.i.answer k l

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

Erdos766.erdos_766.parts.ii

Open: stated without proof.

For fixed \(k\) and large \(n\) is \(f(n;k,l)\) a strictly monotone function of \(l\)?

As in Erdos766.erdos_766.parts.i, \(f\) is \(f_1\) of [Er64c], and we use the range \(k\lt l\leq k^2/4\) in which the question is asked there; here k ^ 2 / 4 is \(\lfloor k^2/4\rfloor\). The question for the function of erdosproblems.com is Erdos766.erdos_766.variants.minExtremalNumber_strictMonoOn.

theorem erdos_766.parts.ii :
    ∀ k : ℕ, ∀ᶠ n : ℕ in atTop,
      StrictMonoOn (forcingNumber n k) (Set.Ioc k (k ^ 2 / 4))

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

Erdos766.erdos_766.variants.dirac_erdos

Solved: stated here without proof.

Dirac and Erdős proved independently that when \(l=\lfloor k^2/4\rfloor+1\)

\[f(n;k,l)\leq \lfloor n^2/4\rfloor+1.\]

[Er64c, p. 34] states this for every \(k \leq n\). We assume \(k \geq 3\), since for \(k \leq 2\) there is no graph with \(k\) vertices and \(\lfloor k^2/4\rfloor+1\) edges.

theorem erdos_766.variants.dirac_erdos (n k : ℕ) (hk : 3 ≤ k) (hkn : k ≤ n) :
    forcingNumber n k (k ^ 2 / 4 + 1) ≤ n ^ 2 / 4 + 1

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

Erdos766.erdos_766.variants.minExtremalNumber_estimate

Open: stated without proof.

The estimate question of Erdos766.erdos_766.parts.i for the function \(\min \mathrm{ex}(n;G)\) of erdosproblems.com (Erdos766.minExtremalNumber).

theorem erdos_766.variants.minExtremalNumber_estimate :
    ∀ k l : ℕ, k < l → l ≤ k ^ 2 / 4 →
      (fun n ↦ ((minExtremalNumber n k l).toNat : ℝ)) =Θ[atTop]
        erdos_766.variants.minExtremalNumber_estimate.answer k l

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

Erdos766.erdos_766.variants.minExtremalNumber_strictMonoOn

Open: stated without proof.

The monotonicity question of Erdos766.erdos_766.parts.ii for the function \(\min \mathrm{ex}(n;G)\) of erdosproblems.com (Erdos766.minExtremalNumber).

theorem erdos_766.variants.minExtremalNumber_strictMonoOn :
    ∀ k : ℕ, ∀ᶠ n : ℕ in atTop,
      StrictMonoOn (minExtremalNumber n k) (Set.Ioc k (k ^ 2 / 4))

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

Sources

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

LeanErdos766.erdos_766.parts.i · Erdos766.erdos_766.parts.ii · Erdos766.erdos_766.variants.dirac_erdos · Erdos766.erdos_766.variants.minExtremalNumber_estimate · Erdos766.erdos_766.variants.minExtremalNumber_strictMonoOn

TheoremErdős Problem 767#

References: - erdosproblems.com/767 - [Er64c] Erdős, P., Extremal problems in graph theory. Theory of Graphs and its Applications (Proc. Sympos. Smolenice, 1963) (1964), 29-36. - [Er69b] Erdős, P., Problems and results in chromatic graph theory. Proof Techniques in Graph Theory (Proc. Second Ann Arbor Graph Theory Conf., Ann Arbor, Mich., 1968) (1969), 27-35. - [Er75] Erdős, P., Some recent progress on extremal problems in graph theory. Congr. Numer. (1975), 3-14. - [Ji04] Jiang, Tao, A note on a conjecture about cycles with many incident chords. J. Graph Theory (2004), 180-182.

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

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

Erdos767.erdos_767

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

Let \(g_k(n)\) be the maximal number of edges possible on a graph with \(n\) vertices which does not contain a cycle with \(k\) chords incident to a vertex on the cycle. Is it true that

\[g_k(n)=(k+1)n-(k+1)^2\]

for \(n\) sufficiently large?

The answer is yes: the conjectured equality was proved for \(n\geq 3k+3\) by Jiang [Ji04].

theorem erdos_767 :
    ∀ k ≥ 1, ∀ n ≥ 3 * k + 3, g k n = (k + 1) * n - (k + 1) ^ 2

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

Erdos767.erdos_767.variants.czipszer

Solved: stated here without proof.

Czipszer proved that \(g_k(n)\leq (k+1)n\).

theorem erdos_767.variants.czipszer (k n : ℕ) : g k n ≤ (k + 1) * n

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

Erdos767.erdos_767.variants.posa

Solved: stated here without proof.

Pósa proved that \(g_1(n)=2n-4\) for \(n\geq 4\).

theorem erdos_767.variants.posa (n : ℕ) (hn : 4 ≤ n) : g 1 n = 2 * n - 4

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

Sources

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

LeanErdos767.erdos_767 · Erdos767.erdos_767.variants.czipszer · Erdos767.erdos_767.variants.posa

TheoremErdős Problem 769#

Reference: erdosproblems.com/769

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

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

Erdos769.erdos_769

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

Let \(c(n)\) be minimal such that if \(k\geq c(n)\) then the \(n\)-dimensional unit cube can be decomposed into \(k\) homothetic \(n\)-dimensional cubes. Give good bounds for \(c(n)\) — in particular, is it true that \(c(n)\gg n^n\)?

The c(n) \gg n^n conjecture is false: for odd n, one can tile the unit n-cube into k homothetic cubes for every k ≥ U(n) with U(n)/n^n → 0, so c(n)/n^n → 0 along odd dimensions and no absolute constant lower-bounds it.

Determining good bounds for c(n) in general remains open.

theorem erdos_769 : ¬ Erdos769LowerBound

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/769.lean, line 85.

Erdos769.erdos_769.variants.growth_rate

Open: stated without proof.

What refuting \(c(n)\gg n^n\) leaves open: give good bounds for \(c(n)\). Asked here on the scale the problem itself sets, \(n^n\): does \(c\) have a well-defined order

\[\lim_{n\to\infty}\frac{\log c(n)}{n\log n}?\]

The refuted conjecture would have forced this limit to be at least \(1\). The cutoff condition is restricted to positive dimensions: in dimension zero, exact coverage permits only one tile, so no cutoff exists.

theorem erdos_769.variants.growth_rate :
    ∃ c : ℕ → ℕ, (∀ n, 0 < n → IsCutoff n (c n)) ∧
      ∃ γ : ℝ, Tendsto (fun n : ℕ => Real.log (c n) / (n * Real.log n)) atTop (𝓝 γ)

Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/769.lean, line 97.

Sources

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

LeanErdos769.erdos_769 · Erdos769.erdos_769.variants.growth_rate

TheoremErdős Problem 770#

References: - erdosproblems.com/770 - [Er49d] Erdös, P. "On the strong law of large numbers." Transactions of the American Mathematical Society 67.1 (1949): 51-56. - [Ma66] Matsuyama, Noboru. "On the strong law of large numbers." Tohoku Mathematical Journal, Second Series 18.3 (1966): 259-269.

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

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

Erdos770.Nat.Prime.h_eq_add_one

Textbook result, stated without proof.

n + 1 is prime iff h n = n + 1. This is described as 'easy to see' in [Er74b].

theorem Nat.Prime.h_eq_add_one {n : ℕ} (hn : 2 < n) : h n = n + 1 ↔ (n + 1).Prime

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

Erdos770.erdos_770.variants.odd_h_unbounded

Textbook result, stated without proof.

For odd n, the values of h n form an unbounded set. This is described as 'easy to see' in [Er74b].

theorem erdos_770.variants.odd_h_unbounded : Unbounded (· ≤ ·) (ENat.toNat '' (h '' Odd))

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

Erdos770.erdos_770.parts.i

Open: stated without proof.

For every prime p, does the density of integers with h n = p exist?

theorem erdos_770.parts.i : ∀ p : ℕ, p.Prime → ∃ a, HasDensity {n | h n = p} a

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

Erdos770.erdos_770.parts.ii

Open: stated without proof.

Does liminf h n = ∞?

theorem erdos_770.parts.ii : liminf h atTop = ⊤

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

Erdos770.erdos_770.parts.iii

Open: stated without proof.

Is it true that if p is the greatest prime such that p - 1 ∣ n and p > n ^ ε, then h n = p?

theorem erdos_770.parts.iii : ∀ ε > 0, ∀ᶠ n in atTop,
    let p := sSup {m : ℕ | m.Prime ∧ m - 1 ∣ n}
    p > (n : ℝ) ^ (ε : ℝ) → h n = p

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

Erdos770.erdos_770.variants.three

Open: stated without proof.

It is probably true that h n = 3 for infinitely many n.

theorem erdos_770.variants.three : {n | h n = 3}.Infinite

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

Sources

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

LeanErdos770.Nat.Prime.h_eq_add_one · Erdos770.erdos_770.variants.odd_h_unbounded · Erdos770.erdos_770.parts.i · Erdos770.erdos_770.parts.ii · Erdos770.erdos_770.parts.iii · Erdos770.erdos_770.variants.three

TheoremErdős Problem 771#

References: - erdosproblems.com/771 - [Er89] Erdős, P., Some problems and results on combinatorial number theory. Graph theory and its applications: East and West (Jinan, 1986), Ann. New York Acad. Sci. 576 (1989), 132-145. - [AlFr88] Alon, N. and Freiman, G., On sums of subsets of a set of integers. Combinatorica 8 (1988), 297-306.

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

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

Erdos771.erdos_771

Solved: stated here without proof.

Let \(f(n)\) be maximal such that, for every \(m\geq 1\), there exists some \(S\subseteq \{1,\ldots,n\}\) with \(\lvert S\rvert=f(n)\) such that \(m\neq \sum_{a\in A}a\) for all \(A\subseteq S\).

Is it true that

\[f(n) = \left(\frac{1}{2}+o(1)\right)\frac{n}{\log n}?\]

The answer is yes: the lower bound is due to Erdős and Graham and the upper bound to Alon and Freiman [AlFr88].

theorem erdos_771 :
    (fun n : ℕ ↦ (f n : ℝ)) ~[atTop] fun n : ℕ ↦ (n : ℝ) / (2 * Real.log n)

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

Erdos771.erdos_771.variants.erdos_graham_lower

Solved: stated here without proof.

Erdős and Graham proved the lower bound

\[f(n)\geq \left(\frac{1}{2}+o(1)\right)\frac{n}{\log n}.\]

Their proof is to note that we can assume that \(m< \binom{n+1}{2}\) and then, for any \(m\), take \(S=\{ kp : 1\leq k\lt \frac{n}{p}\}\) where \(p\) is the least prime that does not divide \(m\) (so \(p<(2+o(1))\log n\)).

theorem erdos_771.variants.erdos_graham_lower :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop, (1 / 2 - ε) * ((n : ℝ) / Real.log n) ≤ f n

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

Erdos771.erdos_771.variants.alon_freiman_upper

Solved: stated here without proof.

The complementary bound

\[f(n) \leq \left(\frac{1}{2}+o(1)\right)\frac{n}{\log n}\]

was proved by Alon and Freiman [AlFr88], who chose \(m\) as the least common multiple of \(\{1,\ldots,s\}\) where \(s\) is maximal such that \(m\leq \frac{n^2}{20(\log n)^2}\).

theorem erdos_771.variants.alon_freiman_upper :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop, (f n : ℝ) ≤ (1 / 2 + ε) * ((n : ℝ) / Real.log n)

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

Sources

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

LeanErdos771.erdos_771 · Erdos771.erdos_771.variants.erdos_graham_lower · Erdos771.erdos_771.variants.alon_freiman_upper

TheoremErdős Problem 772#

References: - erdosproblems.com/772 - [Er80e] Erdős, P., Some applications of Ramsey's theorem to additive number theory. European J. Combin. (1980), 43-46. - [Er84d] Erdős, P., Extremal problems in number theory, combinatorics and geometry. Proceedings of the International Congress of Mathematicians, Vol. 1, 2 (Warsaw, 1983) (1984), 51-70. - [AlEr85] Alon, Noga and Erdős, P., An application of graph theory to additive number theory. European J. Combin. (1985), 201-203.

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

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

Erdos772.erdos_772.parts.i

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

Let \(k\geq 1\) and \(H_k(n)\) be the maximal \(r\) such that if \(A\subset\mathbb{N}\) has \(\lvert A\rvert=n\) and \(\| 1_A\ast 1_A\|_\infty \leq k\) then \(A\) contains a Sidon set of size at least \(r\).

Is it true that \(H_k(n)/n^{1/2}\to \infty\)?

The answer is yes, and in fact \(H_k(n) \gg_k n^{2/3}\), proved by Alon and Erdős [AlEr85].

theorem erdos_772.parts.i :
    ∀ k ≥ 1, Tendsto (fun n : ℕ ↦ (H k n : ℝ) / √n) atTop atTop

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

Erdos772.erdos_772.parts.ii

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

Is it true that \(H_k(n) > n^{1/2+c}\) for some constant \(c>0\)?

The answer is yes, and in fact \(H_k(n) \gg_k n^{2/3}\), proved by Alon and Erdős [AlEr85].

theorem erdos_772.parts.ii :
    ∀ k ≥ 1, ∃ c > 0, ∀ᶠ n : ℕ in atTop, (n : ℝ) ^ (1 / 2 + c : ℝ) < H k n

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

Erdos772.erdos_772.variants.alon_erdos

Solved: stated here without proof.

Alon and Erdős [AlEr85] proved that \(H_k(n) \gg_k n^{2/3}\).

theorem erdos_772.variants.alon_erdos (k : ℕ) (hk : 1 ≤ k) :
    ∃ c > 0, ∀ᶠ n : ℕ in atTop, c * (n : ℝ) ^ (2 / 3 : ℝ) ≤ H k n

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

Erdos772.erdos_772.variants.upper_bound

Solved: stated here without proof.

Erdős [Er84d] proved that \(H_k(n) \ll n^{2/3}\), where the implied constant is absolute.

Since \(1_A\ast 1_A\) counts ordered pairs, the bound needs \(k\geq 4\): the construction of Erdős has at most two unordered representations of each sum, hence at most four ordered ones, while \(k\leq 2\) forces \(A\) itself to be Sidon and so \(H_k(n)=n\). For \(k=3\) the only collisions are \(a+b=2c\), so the Sidon subsets of \(A\) are its \(3\)-term-progression-free subsets, which have size \(n^{1-o(1)}\), and the bound fails there too.

theorem erdos_772.variants.upper_bound :
    ∃ C : ℝ, ∀ k ≥ 4, ∀ᶠ n : ℕ in atTop,
      (H k n : ℝ) ≤ C * (n : ℝ) ^ (2 / 3 : ℝ)

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

Sources

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

LeanErdos772.erdos_772.parts.i · Erdos772.erdos_772.parts.ii · Erdos772.erdos_772.variants.alon_erdos · Erdos772.erdos_772.variants.upper_bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.