Erdős Problem 67 to Erdős Problem 88
TheoremErdős Problem 67#
References: - erdosproblems.com/67 - [Ta16] Tao, Terence, The Erdős discrepancy problem. Discrete Anal. (2016), Paper No. 1, 29.
Quoted from FormalConjectures/ErdosProblems/67.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/67.
The file states 2 research or textbook statements: 2 solved.
Erdos67.erdos_67
Solved: stated here without proof.
The Erdős discrepancy problem
If \(f\colon \mathbb N \rightarrow \{-1, +1\}\) then is it true that for every \(C>0\) there exist \(d, m \ge 1\) such that
\[\left\lvert \sum_{1\leq k\leq m}f(kd)\right\rvert > C?\]This is true, and was proved by Tao [Ta16]
theorem erdos_67 (f : ℕ → ({-1, 1} : Finset ℝ)) (C : ℝ) (hC : 0 < C) : ∃ᵉ (d ≥ 1) (m ≥ 1),
C < |∑ k ∈ Finset.Icc 1 m, (f (k * d)).1|
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/67.lean, line 42.
Erdos67.erdos_67.variants.complex
Solved: stated here without proof.
The Erdős discrepancy problem (complex variant)
If \(f\colon \mathbb N \rightarrow S^1 ⊆ ℂ\) then is it true that for every \(C>0\) there exist \(d, m \ge 1\) such that
\[\left\lvert \sum_{1\leq k\leq m}f(kd)\right\rvert > C?\]This is true, and was proved by Tao [Ta16]
theorem erdos_67.variants.complex (f : ℕ → Metric.sphere (0 : ℂ) 1) (C : ℝ) (hC : 0 < C) :
∃ᵉ (d ≥ 1) (m ≥ 1), C < ‖∑ k ∈ Finset.Icc 1 m, (f (k * d)).1‖
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/67.lean, line 54.
Sources
TheoremErdős Problem 68#
Reference: erdosproblems.com/68
Quoted from FormalConjectures/ErdosProblems/68.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/68.
The file states 2 research or textbook statements: 1 open and 1 textbook result.
Erdos68.erdos_68
Open: stated without proof.
Is
\[\sum_{n=2}^\infty \frac{1}{n!-1}\]irrational?
theorem erdos_68 :
Irrational (∑' n : ℕ, 1 / ((n + 2).factorial - 1 : ℝ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/68.lean, line 36.
Erdos68.sum_factorial_inv_eq_geometric
Textbook result, proved here.
\[\sum_{n=2}^\infty \frac{1}{n!-1} = \sum_{n=2}^\infty \sum_{k=1}^\infty \frac{1}{(n!)^k}\]
theorem sum_factorial_inv_eq_geometric :
let f (n k : ℕ) : ℝ := 1 / ((n + 2).factorial : ℝ) ^ (k + 1)
∑' n : ℕ, (1 : ℝ) / ((n + 2).factorial - 1) = ∑' n : ℕ, ∑' k : ℕ, f n k
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/68.lean, line 44.
Sources
TheoremErdős Problem 69#
Reference: erdosproblems.com/69
Quoted from FormalConjectures/ErdosProblems/69.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/69.
The file states 2 research or textbook statements: 1 solved and 1 textbook result.
Erdos69.erdos_69
Textbook result, stated without proof.
Is
\[ \sum_{n\geq 2}\frac{\omega(n)}{2^n} \]irrational? (Here \(\omega(n)\) counts the number of distinct prime divisors of \(n\).)
theorem erdos_69 : Irrational <| ∑' n, ω (n + 2) / 2 ^ (n + 2)
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/69.lean, line 40.
Erdos69.erdos_69.variants.specialisation_of_erdos_257
Proved here.
Tao observed that
erdos_69is a special case oferdos_257, since\[ \sum_{n\geq 2}\frac{\omega(n)}{2^n} = \sum_p \frac{1}{2^p - 1}. \]
theorem erdos_69.variants.specialisation_of_erdos_257 :
let A := { n : ℕ | n.Prime }
∑' n, ω (n + 2) / (2 ^ (n + 2) : ℝ) = ∑' p : A, 1 / (2 ^ p.1 - 1)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/69.lean, line 50.
Sources
TheoremErdős Problem 70#
References: - erdosproblems.com/70 - [ErRa56] Erdős, P. and Rado, R., A partition calculus in set theory, Bull. Amer. Math. Soc. 62 (1956), 427–489, Theorem 31. - [Er87] Erdős, P., Some problems on finite and infinite graphs, Logic and combinatorics (Arcata, Calif., 1985), Contemp. Math. 65 (1987), 223–228.
The 3-uniform (triple) partition relation \(\mathfrak{c} \to (\beta, n)^3_2\), where \(\mathfrak{c}\) denotes the order type of the real numbers with their usual order (written \(\lambda\) in [ErRa56]). This is the triple analogue of
OrdinalCardinalRamseyused in Problems 590–592; the file also contains the analogous relation for an ordinal in place of the real line.
Quoted from FormalConjectures/ErdosProblems/70.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/70.
The file states 5 research or textbook statements: 3 open and 2 solved. It also has 1 test statement, counted here but not shown.
Erdos70.erdos_70
Open: stated without proof.
Erdős Problem 70: Let \(\mathfrak{c}\) be the order type of the real numbers, let \(\beta\) be a countable ordinal, and let \(2 \le n < \omega\). Is it true that \(\mathfrak{c} \to (\beta, n)^3_2\)?
Note: The cases \(n \le 3\) are trivially true (compare
omega_three), so the genuine content of the conjecture begins at \(n = 4\).
theorem erdos_70 :
∀ᵉ (β : Ordinal.{0}) (n : ℕ) (_ : β.card ≤ ℵ₀) (_ : 2 ≤ n),
RealCardinalRamsey3 β n
Category research open; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/70.lean, line 113.
Erdos70.erdos_70.variants.erdos_rado
Solved: stated here without proof.
Erdős–Rado partial result: \(\mathfrak{c} \to (\omega + n, 4)^3_2\) for any \(2 \le n < \omega\), where \(\mathfrak{c}\) is the order type of the real numbers. Positive partial answer to Problem 70 with \(\beta = \omega + n\) and the blue side fixed at \(4\) [ErRa56, Theorem 31].
theorem erdos_rado (n : ℕ) (hn : 2 ≤ n) :
RealCardinalRamsey3 (ω + n) 4
Category research solved; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/70.lean, line 129.
Erdos70.erdos_70.variants.omega_times_two_four
Open: stated without proof.
First open case beyond Erdős–Rado: \(\mathfrak{c} \to (\omega \cdot 2, 4)^3_2\), where \(\mathfrak{c}\) is the order type of the real numbers.
Erdős and Rado proved \(\mathfrak{c} \to (\omega + n, 4)^3_2\) for every finite \(n \ge 2\) (see
erdos_rado), which covers all red ordinals below \(\omega \cdot 2 = \omega + \omega\). This variant asks whether the result extends to \(\beta = \omega \cdot 2\), the simplest countable ordinal not covered by their theorem.
theorem omega_times_two_four :
RealCardinalRamsey3 (ω * 2) 4
Category research open; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/70.lean, line 143.
Erdos70.erdos_70.variants.omega_three
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/c024db0fa3ac32c6dddcd6c28d7b0cd994dad580/FormalConjectures/ErdosProblems/70.lean#L126.
Trivial boundary case: \(\mathfrak{c} \to (\omega, 3)^3_2\), stated for the initial ordinal \(\mathfrak{c}.\mathrm{ord}\) of the cardinality of the continuum.
This is trivially true because in a 3-uniform hypergraph, a \"blue clique of size 3\" consists of a single 3-element subset (\(\binom{3}{3} = 1\)), so the blue alternative merely asks for one blue triple to exist. The proof splits into two cases: - If any blue triple exists, it is itself a blue-monochromatic set of cardinality 3. - If no blue triple exists, all triples are red, and since \(\omega \le \mathfrak{c}\), any subset of order type \(\omega\) is red-monochromatic.
The problem becomes non-trivial only for \(n \ge 4\); see
omega_times_two_fourfor the simplest genuinely open case.
theorem omega_three :
OrdinalCardinalRamsey3 (𝔠).ord ω 3
Category research solved; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/70.lean, line 164.
Erdos70.erdos_70.variants.omega_one
Open: stated without proof.
The relation at \(\omega_1\): \(\mathfrak{c} \to (\omega_1, n)^3_2\) for finite \(n \ge 2\), where \(\omega_1 = \aleph_1\) is the first uncountable ordinal.
Note that \(\omega_1\) is not a countable ordinal, so this is not directly an instance of the main Erdős problem (which asks for countable \(\beta\)). Under CH, \(\omega_1 = \mathfrak{c}.\mathrm{ord}\), making this a self-referential question about \(\mathfrak{c}.\mathrm{ord} \to (\mathfrak{c}.\mathrm{ord}, n)^3_2\).
theorem omega_one :
∀ᵉ (n : ℕ) (_ : 2 ≤ n),
OrdinalCardinalRamsey3 (𝔠).ord (Cardinal.aleph 1).ord n
Category research open; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/70.lean, line 178.
Sources
TheoremErdős Problem 71#
References: - erdosproblems.com/71 - [Bo77] Bollobás, Béla, Cycles modulo \(k\). Bull. London Math. Soc. (1977), 97-98. - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79. - [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186. - [Er97b] Erdős, Paul, Some old and new problems in various branches of combinatorics. Discrete Math. (1997), 227-231.
Quoted from FormalConjectures/ErdosProblems/71.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/71.
The file states 1 research or textbook statement: 1 solved.
Erdos71.erdos_71
Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/110d489ed5c07e5b216453e092e9113127c98c9a/problems/71/Erdos71.lean.
Is it true that for every infinite arithmetic progression \(P\) which contains even numbers there is some constant \(c=c(P)\) such that every graph with average degree at least \(c\) contains a cycle whose length is in \(P\)?
In [Er82e] Erdős credits this conjecture to himself and Burr. This has been proved by Bollobás [Bo77]. The best dependence of the constant \(c(P)\) is unknown.
The infinite arithmetic progression is encoded as a set \(P \subseteq \mathbb{N}\) satisfying
P.IsAPOfLength ⊤(which forces a positive common difference), and "contains even numbers" as the existence of an even element. The average degree of a finite simple graph isSimpleGraph.averageDegree, i.e. \((\sum_v \deg v)/|V| \in \mathbb{Q}\), and a cycle whose length is in \(P\) is a cycle walkwwithw.length ∈ P.
theorem erdos_71 :
∀ P : Set ℕ, P.IsAPOfLength ⊤ → (∃ n ∈ P, Even n) →
∃ c : ℚ, ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V)
[DecidableRel G.Adj], c ≤ G.averageDegree →
∃ (v : V) (w : G.Walk v v), w.IsCycle ∧ w.length ∈ P
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/71.lean, line 54.
Sources
TheoremErdős Problem 72#
References: - erdosproblems.com/72 - [Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269. - [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186. - [Er97b] Erdős, Paul, Some old and new problems in various branches of combinatorics. Discrete Math. (1997), 227-231. - [Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67. - [Bo77] Bollobás, Béla, Cycles modulo \(k\). Bull. London Math. Soc. (1977), 97-98. - [Ve05] Verstraete, Jacques, Unavoidable cycle lengths in graphs. J. Graph Theory (2005), 151-167. - [LiMo20] Liu, Hong and Montgomery, Richard, A solution to Erdős and Hajnal's odd cycle problem. arXiv:2010.15802 (2020).
Quoted from FormalConjectures/ErdosProblems/72.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/72.
The file states 2 research or textbook statements: 2 solved.
Erdos72.erdos_72
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos72.lean#L184.
Is there a set \(A\subset \mathbb{N}\) of density \(0\) and a constant \(c>0\) such that every graph on sufficiently many vertices with average degree \(\geq c\) contains a cycle whose length is in \(A\)?
Bollobás [Bo77] proved that such a \(c\) does exist if \(A\) is an infinite arithmetic progression containing even numbers (see 71).
Erdős was 'almost certain' that if \(A\) is the set of powers of \(2\) then no such \(c\) exists (although he conjectured that \(n\) vertices and average degree \(\gg (\log n)^{C}\) suffices for some \(C=O(1)\)). If \(A\) is the set of squares (or the set of \(p\pm 1\) for \(p\) prime) then he had no guess.
Solved by Verstraëte [Ve05], who gave a non-constructive proof that such a set \(A\) exists.
Liu and Montgomery [LiMo20] proved that in fact this is true when \(A\) is the set of powers of \(2\) (more generally any set of even numbers which doesn't grow too quickly) - in particular this contradicts the previous belief of Erdős.
theorem erdos_72 : ∃ A : Set ℕ, A.HasDensity 0 ∧ ∃ c : ℚ, 0 < c ∧
∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph (Fin n), c ≤ G.averageDegree →
∃ (v : Fin n) (w : G.Walk v v), w.IsCycle ∧ w.length ∈ A
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/72.lean, line 68.
Erdos72.erdos_72.variants.powers_of_two
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos72.lean#L157.
Liu and Montgomery [LiMo20] proved that there is a constant \(c > 0\) such that every graph on sufficiently many vertices with average degree \(\geq c\) contains a cycle whose length is a power of \(2\).
theorem erdos_72.variants.powers_of_two : ∃ c : ℚ, 0 < c ∧
∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph (Fin n), c ≤ G.averageDegree →
∃ (v : Fin n) (w : G.Walk v v), w.IsCycle ∧ ∃ k : ℕ, w.length = 2 ^ k
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/72.lean, line 82.
Sources
TheoremErdős Problem 73#
References: - erdosproblems.com/73 - [Re99] Reed, B., Mangoes and Blueberries. Combinatorica (1999), 267-296.
Quoted from FormalConjectures/ErdosProblems/73.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/73.
The file states 1 research or textbook statement: 1 solved.
Erdos73.erdos_73
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos73.lean#L122.
Let \(k\ge 0\). Let \(G\) be a graph such that every subgraph \(H\) contains an independent set of size \(\ge (n-k)/2\), where \(n\) is the number of vertices of \(H\). Must \(G\) be the union of a bipartite graph and \(O_k(1)\) many vertices?
Proved by Reed [Re99].
The linked formal proof (Alexeev and Codex, following Reed's mangoes-and-blueberries argument) states the hypothesis as
∀ H : G.Subgraph, H.verts.ncard ≤ 2 * H.coe.indepNum + kand the conclusion as(G.induce Dᶜ).IsBipartite, for graphs onFin n(and, equivalently, on any finite vertex type); this implies the statement below.
theorem erdos_73 :
∀ (k : ℕ), ∃ (C : ℕ),
∀ (V : Type) [Fintype V] (G : SimpleGraph V),
(∀ (S : Finset V), ∃ (I : Finset V), I ⊆ S ∧ (G.induce (I : Set V)).edgeSet = ∅ ∧
(I.card : ℝ) ≥ (S.card - k : ℝ) / 2) →
∃ (D : Finset V), D.card ≤ C ∧
(G.induce (D : Set V)ᶜ).Colorable 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/73.lean, line 47.
Sources
TheoremErdős Problem 74#
Reference: erdosproblems.com/74
Quoted from FormalConjectures/ErdosProblems/74.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/74.
The file states 2 research or textbook statements: 1 open and 1 solved. It also has 2 test statements, counted here but not shown.
Erdos74.erdos_74
Solved: stated here; a Lean proof is at https://github.com/tadamcz/erdos74/blob/e127ee587c7c91267eecdb3569443d2b0ad64b52/Erdos74/Resolutions/Erdos74_118usd_22h.lean#L2511.
Let \(f(n)\to \infty\) possibly very slowly. Is there a graph of infinite chromatic number such that every finite subgraph on \(n\) vertices can be made bipartite by deleting at most \(f(n)\) edges?
The answer is no. A machine-checked disproof constructs a function \(f(n) \to \infty\) for which every graph satisfying this local deletion bound has finite chromatic number.
theorem erdos_74 : ¬ ∀ f : ℕ → ℕ, Tendsto f atTop atTop →
(∃ (V : Type u) (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧
∀ n, G.maxSubgraphEdgeDistToBipartite n ≤ f n)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/74.lean, line 132.
Erdos74.erdos_74.variants.sqrt
Open: stated without proof.
Is there a graph of infinite chromatic number such that every finite subgraph on \(n\) vertices can be made bipartite by deleting at most \(\sqrt{n}\) edges?
theorem erdos_74.variants.sqrt :
∃ (V : Type u) (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧
∀ n, G.maxSubgraphEdgeDistToBipartite n ≤ (n : ℝ).sqrt
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/74.lean, line 142.
Sources
TheoremErdős Problem 75#
Reference: * [erdosproblems.com/75] (https://www.erdosproblems.com/75)
Quoted from FormalConjectures/ErdosProblems/75.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/75.
The file states 1 research or textbook statement: 1 open.
Erdos75.erdos_75
Open: stated without proof.
Is there a graph of chromatic number
ℵ_ 1withℵ_ 1vertices such that for allε > 0, ifnis sufficiently large andHis a subgraph onnvertices, thenHcontains an independent set of size> n ^ (1 - ε)?
theorem erdos_75 :
∃ (V : Type) (G : SimpleGraph V),
G.chromaticCardinal = ℵ_ 1 ∧
#V = ℵ_ 1 ∧
∀ ε > (0 : ℝ),
∀ᶠ (n : ℕ) in Filter.atTop, ∀ (H : G.Subgraph),
H.verts.ncard = n →
∃ (I : Finset V),
(I : Set V) ⊆ H.verts ∧
G.IsIndepSet (I : Set V) ∧
(I.card : ℝ) > (n : ℝ) ^ (1 - ε)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/75.lean, line 39.
Sources
TheoremErdős Problem 77#
References: - erdosproblems.com/77 - [BBCGHMST24] Balister, P. and Bollobás, B. and Campos, M. and Griffiths, S. and Hurley, E. and Morris, R. and Sahasrabudhe, J. and Tiba, M., Upper bounds for multicolour Ramsey numbers. arXiv:2410.17197 (2024). - [CGMS23] Campos, Marcelo and Griffiths, Simon and Morris, Robert and Sahasrabudhe, Julian, An exponential improvement for diagonal Ramsey. arXiv:2303.09521 (2023). - [Er88] Erdős, P, Problems and results in combinatorial analysis and graph theory. Discrete Math. (1988), 81-92. - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350. - [GNNW24] Gupta, P. and Ndiaye, N. and Norin, S. and Wei, L., Optimizing the CGMS upper bound on Ramsey numbers. arXiv:2407.19026 (2024).
Quoted from FormalConjectures/ErdosProblems/77.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/77.
The file states 1 research or textbook statement: 1 open.
Erdos77.erdos_77
Open: stated without proof.
If \(R(k)\) is the Ramsey number for \(K_k\), the minimal \(n\) such that every \(2\)-colouring of the edges of \(K_n\) contains a monochromatic copy of \(K_k\), then find the value of
\[\lim_{k\to \infty}R(k)^{1/k}.\]This problem is #3 in Ramsey Theory in the graphs problem collection.
theorem erdos_77 :
Filter.Tendsto (fun k : ℕ ↦ (SimpleGraph.diagonalRamsey k : ℝ) ^ (1 / (k : ℝ)))
Filter.atTop (𝓝 erdos_77.answer)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/77.lean, line 54.
Sources
TheoremErdős Problem 78#
References: - erdosproblems.com/78 - [Co15] Cohen, Gil, Two-source dispersers for polylogarithmic entropy and improved Ramsey graphs. arXiv:1506.04428 (2015). - [Er47] Erdős, P., Some remarks on the theory of graphs. Bull. Amer. Math. Soc. (1947), 292-294. - [Er71] Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109. - [Er88] Erdős, P, Problems and results in combinatorial analysis and graph theory. Discrete Math. (1988), 81-92. - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350. - [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186. - [Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67. - [Li23b] Li, Xin, Two source extractors for asymptotically optimal entropy, and (many) more. arXiv:2303.06802 (2023). - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999).
Quoted from FormalConjectures/ErdosProblems/78.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/78.
The file states 7 research or textbook statements: 2 open and 5 solved.
Erdos78.erdos_78
Open: stated without proof.
Let \(R(k)\) be the Ramsey number for \(K_k\). Give a constructive proof that \(R(k) > C^k\) for some constant \(C > 1\).
Equivalently, give an explicit construction of graphs on \(n\) vertices which contain no clique and no independent set of size \(\geq c \log n\), for some constant \(c > 0\).
We formalise "explicit" as: the adjacency relation of the graph on \(n\) vertices is decided by a single algorithm that runs in time polynomial in \(n\) (see
explicitGraph). This is the weakest reasonable notion ("weakly explicit"); even this is open. The strongly explicit version, with time polynomial in \(\log n\), iserdos_78.variants.strongly_explicit.This problem is #4 in Ramsey Theory in the graphs problem collection.
theorem erdos_78 :
∃ c > (0 : ℝ), ∃ adj : List Bool × ℕ × ℕ → Bool, IsPolyTime adj ∧
∀ᶠ n in atTop, NoHomogeneousSet (explicitGraph adj n) ⌈c * log n⌉₊
Category research open; AMS 05 Combinatorics, 68 Computer science. Declared in FormalConjectures/ErdosProblems/78.lean, line 96.
Erdos78.erdos_78.variants.nonconstructive
Solved: stated here without proof.
Erdős [Er47] gave a simple probabilistic, non-constructive proof that \(R(k) > C^k\) for some constant \(C > 1\). In fact \(R(k) > 2^{k/2}\) for all \(k \geq 3\).
theorem erdos_78.variants.nonconstructive :
∃ C > (1 : ℝ), ∀ᶠ k in atTop, C ^ k < (SimpleGraph.diagonalRamsey k : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/78.lean, line 106.
Erdos78.erdos_78.variants.little_o_sqrt
Solved: stated here without proof.
Erdős also asked for an explicit construction of graphs on \(n\) vertices whose largest clique and independent set have size \(o(n^{1/2})\). Such constructions are now known; see [Co15] for the history.
theorem erdos_78.variants.little_o_sqrt :
∃ f : ℕ → ℝ, f =o[atTop] (fun n ↦ √(n : ℝ)) ∧
∃ adj : List Bool × ℕ × ℕ → Bool, IsPolyTime adj ∧
∀ᶠ n in atTop, NoHomogeneousSet (explicitGraph adj n) ⌈f n⌉₊
Category research solved; AMS 05 Combinatorics, 68 Computer science. Declared in FormalConjectures/ErdosProblems/78.lean, line 116.
Erdos78.erdos_78.variants.cohen
Solved: stated here without proof.
Cohen [Co15] constructed explicit graphs on \(n\) vertices with no clique and no independent set of size \(2^{(\log \log n)^C}\), for some constant \(C > 0\).
theorem erdos_78.variants.cohen :
∃ C > (0 : ℝ), ∃ adj : List Bool × ℕ × ℕ → Bool, IsPolyTime adj ∧
∀ᶠ n in atTop,
NoHomogeneousSet (explicitGraph adj n) ⌈(2 : ℝ) ^ (log (log n)) ^ C⌉₊
Category research solved; AMS 05 Combinatorics, 68 Computer science. Declared in FormalConjectures/ErdosProblems/78.lean, line 127.
Erdos78.erdos_78.variants.li
Solved: stated here without proof.
Li [Li23b] improved this to explicit graphs on \(n\) vertices with no clique and no independent set of size \((\log n)^C\), for some constant \(C > 0\).
theorem erdos_78.variants.li :
∃ C > (0 : ℝ), ∃ adj : List Bool × ℕ × ℕ → Bool, IsPolyTime adj ∧
∀ᶠ n in atTop, NoHomogeneousSet (explicitGraph adj n) ⌈(log n) ^ C⌉₊
Category research solved; AMS 05 Combinatorics, 68 Computer science. Declared in FormalConjectures/ErdosProblems/78.lean, line 138.
Erdos78.erdos_78.variants.strongly_explicit
Open: stated without proof.
The strongly explicit version of
erdos_78: an explicit family of graphs on \(n\) vertices with no clique and no independent set of size \(\geq c \log n\), where each adjacency query is answered in time polynomial in \(\log n\) (seestronglyExplicitGraph).
theorem erdos_78.variants.strongly_explicit :
∃ c > (0 : ℝ), ∃ adj : ℕ × ℕ × ℕ → Bool, IsPolyTime adj ∧
∀ᶠ n in atTop, NoHomogeneousSet (stronglyExplicitGraph adj n) ⌈c * log n⌉₊
Category research open; AMS 05 Combinatorics, 68 Computer science. Declared in FormalConjectures/ErdosProblems/78.lean, line 149.
Erdos78.erdos_78.variants.li_strongly_explicit
Solved: stated here without proof.
The construction of Li [Li23b] is strongly explicit: there are graphs on \(n\) vertices with no clique and no independent set of size \((\log n)^C\), for some constant \(C > 0\), whose adjacency queries are answered in time polynomial in \(\log n\).
theorem erdos_78.variants.li_strongly_explicit :
∃ C > (0 : ℝ), ∃ adj : ℕ × ℕ × ℕ → Bool, IsPolyTime adj ∧
∀ᶠ n in atTop, NoHomogeneousSet (stronglyExplicitGraph adj n) ⌈(log n) ^ C⌉₊
Category research solved; AMS 05 Combinatorics, 68 Computer science. Declared in FormalConjectures/ErdosProblems/78.lean, line 160.
Sources
TheoremErdős Problem 79#
References: - erdosproblems.com/79 - [EFRS93] Erdős, P., Faudree, R. J., Rousseau, C. C. and Schelp, R. H., Ramsey size linear graphs. Combin. Probab. Comput. (1993), 389-399. - [Wi24] Wigderson, Y., Infinitely many minimally non-Ramsey size linear graphs. arXiv:2409.05931 (2024).
Quoted from FormalConjectures/ErdosProblems/79.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/79.
The file states 1 research or textbook statement: 1 solved.
Erdos79.erdos_79
Solved: stated here without proof.
We say \(G\) is Ramsey size linear if \(R(G,H)\ll m\) for all graphs \(H\) with \(m\) edges and no isolated vertices.
Are there infinitely many graphs \(G\) which are not Ramsey size linear but such that all of its proper subgraphs are?
Asked by Erdős, Faudree, Rousseau, and Schelp [EFRS93]. \(K_4\) was long the only known example. Wigderson [Wi24] proved that there are infinitely many such graphs.
theorem erdos_79 :
∀ (N : ℕ), ∃ (n : ℕ) (_ : N ≤ n) (G : SimpleGraph (Fin n)),
¬ G.IsRamseySizeLinear ∧
∀ H : G.Subgraph, H < ⊤ → H.coe.IsRamseySizeLinear
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/79.lean, line 47.
Sources
TheoremErdős Problem 80#
References: - erdosproblems.com/80 - erdosproblems.com/600, stated in
FormalConjectures/ErdosProblems/600.lean- [FoLo12] Fox, Jacob and Loh, Po-Shen, On a problem of Erdős and Rothschild on edges in triangles. Combinatorica (2012), 619--628.600 asks the same question from the other side.
Erdos600.eFunction n ris the least edge count forcing some edge intortriangles;f c nhere is the largest book forced once the edge count is at least \(cn^2\). Sor ≤ f c nandErdos600.eFunction n r ≤ c * n^2say the same thing, and the two functions are inverse to each other in that sense. Both are built onSimpleGraph.trianglesContaining, which 600 introduced.
Quoted from FormalConjectures/ErdosProblems/80.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/80.
The file states 2 research or textbook statements: 1 open and 1 solved. It also has 1 test statement and 2 API statements, counted here but not shown.
Erdos80.erdos_80.parts.i
Solved: stated here without proof.
Let \(c>0\) and let \(f_c(n)\) be the maximal \(m\) such that every graph \(G\) with \(n\) vertices and at least \(cn^2\) edges, where each edge is contained in at least one triangle, must contain a book of size \(m\), that is, an edge shared by at least \(m\) different triangles. Estimate \(f_c(n)\). In particular, is it true that \(f_c(n)>n^\epsilon\) for some \(\epsilon>0\)?
The answer is no. Fox and Loh [FoLo12] proved that \(f_c(n) \leq n^{O(1/\log\log n)}\) for every fixed \(c < 1/4\), so no \(\epsilon > 0\) works for, say, \(c = 1/8\). For \(c > 1/4\) the situation is different: \(f_c(n) \geq n/6\), see erdosproblems.com/80.
The bound \(c < 1/2\) is what makes the hypothesis satisfiable: a simple graph on \(n\) vertices has at most \(n(n-1)/2\) edges, so no graph has \(cn^2\) of them once \(c \geq 1/2\).
theorem erdos_80.parts.i :
¬ ∀ c : ℝ, 0 < c → c < 1 / 2 →
∃ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (n : ℝ) ^ ε < f c n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/80.lean, line 86.
Erdos80.erdos_80.parts.ii
Open: stated without proof.
The weaker question from the same problem: is \(f_c(n) \gg \log n\)?
Same feasibility bound on
cas above.
theorem erdos_80.parts.ii :
∀ c : ℝ, 0 < c → c < 1 / 2 →
(fun n : ℕ ↦ (f c n : ℝ)) ≫ (fun n : ℕ ↦ Real.log n)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/80.lean, line 97.
Sources
TheoremErdős Problem 81#
References: - erdosproblems.com/81 - [EOZ93] Erdős, Paul and Ordman, Edward T. and Zalcstein, Yechezkel, Clique partitions of chordal graphs. Combin. Probab. Comput. (1993), 409–415. - [CEO94] Chen, Guan-Tao and Erdős, Paul and Ordman, Edward T., Clique partitions of split graphs. Combinatorics, graph theory, algorithms and applications (Beijing, 1993) (1994), 21–30.
Quoted from FormalConjectures/ErdosProblems/81.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/81.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos81.erdos_81
Open: stated without proof.
Let \(G\) be a chordal graph on \(n\) vertices - that is, \(G\) has no induced cycles of length greater than \(3\). Can the edges of \(G\) be partitioned into \(n^2/6+O(n)\) many cliques?
theorem erdos_81 :
∃ C : ℝ, ∀ n : ℕ, ∀ G : SimpleGraph (Fin n), G.IsChordal →
∃ P : Finset (Finset (Fin n)), G.IsCliqueEdgePartition P ∧
(P.card : ℝ) ≤ (n : ℝ) ^ 2 / 6 + C * n
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/81.lean, line 41.
Erdos81.erdos_81.variants.split
Solved: stated here without proof.
Chen, Erdős, and Ordman [CEO94] have shown that any split graph can be partitioned into \(\frac{3}{16}n^2+O(n)\) many cliques.
theorem erdos_81.variants.split :
∃ C : ℝ, ∀ n : ℕ, ∀ G : SimpleGraph (Fin n), G.IsSplitGraph →
∃ P : Finset (Finset (Fin n)), G.IsCliqueEdgePartition P ∧
(P.card : ℝ) ≤ 3 * (n : ℝ) ^ 2 / 16 + C * n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/81.lean, line 50.
Sources
TheoremErdős Problem 82#
Reference: erdosproblems.com/82
Quoted from FormalConjectures/ErdosProblems/82.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/82.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos82.erdos_82
Open: stated without proof.
\(F(n) / \log n \to \infty as n \to \infty\)
theorem erdos_82 : Tendsto (fun n => F n / Real.log n) atTop atTop
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/82.lean, line 53.
Erdos82.erdos_82.variants.F_upper_bound
Solved: stated here without proof.
\(F(n) \le O(n^{1/2} \ln ^ {3/4} n)\)
Theorem 1.4 from [AKS07]
[AKS07] Alon, N. and Krivelevich, M. and Sudakov, B., Large nearly regular induced subgraphs. arXiv:0710.2106 (2007).
theorem erdos_82.variants.F_upper_bound :
(fun n => (F n : ℝ)) =O[atTop] (fun n => Real.sqrt n * (Real.log n) ^ (3 / 4 : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/82.lean, line 64.
Sources
TheoremErdős Problem 83#
References: - erdosproblems.com/83 - [Er71] Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109. - [Er90] Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467-478. - [Er92e] Erdős, Pál, Some Unsolved problems in Geometry, Number Theory and Combinatorics. Eureka (1992), 44-48. - [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186. - [ErKoRa61] Erdős, P. and Ko, Chao and Rado, R., Intersection theorems for systems of finite sets. Quart. J. Math. Oxford Ser. (2) (1961), 313-320. - [AhKh97] Ahlswede, Rudolf and Khachatrian, Levon H., The complete intersection theorem for systems of finite sets. European J. Combin. (1997), 125-136.
Quoted from FormalConjectures/ErdosProblems/83.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/83.
The file states 3 research or textbook statements: 3 solved.
Erdos83.erdos_83
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos83.lean#L36.
Suppose that we have a family \(\mathcal{F}\) of subsets of \([4n]\) such that \(\lvert A\rvert=2n\) for all \(A\in\mathcal{F}\) and for every \(A,B\in \mathcal{F}\) we have \(\lvert A\cap B\rvert \geq 2\). Then
\[\lvert \mathcal{F}\rvert \leq \frac{1}{2}\left(\binom{4n}{2n}-\binom{2n}{n}^2\right).\]Conjectured by Erdős, Ko, and Rado [ErKoRa61]. This inequality would be best possible, as shown by taking \(\mathcal{F}\) to be the collection of all subsets of \([4n]\) of size \(2n\) containing at least \(n+1\) elements from \([2n]\).
Proved by Ahlswede and Khachatrian [AhKh97], who more generally showed the following. Let \(2\leq t\leq k\leq m\) and let \(r\geq 0\) be such that
\[\frac{1}{r+1}\leq \frac{m-2k+2t-2}{(t-1)(k-t+1)}< \frac{1}{r}.\]The largest possible family of subsets of \([m]\) of size \(k\), such that the pairwise intersections have size at least \(t\), is the family of all subsets of \([m]\) of size \(k\) which contain at least \(t+r\) elements from \(\{1,\ldots,t+2r\}\).
The number \(\binom{4n}{2n}-\binom{2n}{n}^2\) is even, so the bound is an integer.
theorem erdos_83 (n : ℕ) (F : Finset (Finset (Fin (4 * n)))) (hF : ∀ A ∈ F, A.card = 2 * n)
(hinter : ∀ A ∈ F, ∀ B ∈ F, 2 ≤ (A ∩ B).card) :
F.card ≤ ((4 * n).choose (2 * n) - (2 * n).choose n ^ 2) / 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/83.lean, line 65.
Erdos83.erdos_83.variants.extremal
Solved: stated here without proof.
The bound in erdős_83 is attained by the family of all subsets of \([4n]\) of size \(2n\) containing at least \(n+1\) elements from \([2n]\).
theorem erdos_83.variants.extremal (n : ℕ) :
∃ F : Finset (Finset (Fin (4 * n))), (∀ A ∈ F, A.card = 2 * n) ∧
(∀ A ∈ F, ∀ B ∈ F, 2 ≤ (A ∩ B).card) ∧
F.card = ((4 * n).choose (2 * n) - (2 * n).choose n ^ 2) / 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/83.lean, line 75.
Erdos83.erdos_83.variants.ahlswede_khachatrian
Solved: stated here without proof.
The complete intersection theorem of Ahlswede and Khachatrian [AhKh97]: for \(2\leq t\leq k\leq m\), every family of \(k\)-subsets of \([m]\) with pairwise intersections of size at least \(t\) is at most as large as one of the families of all \(k\)-subsets of \([m]\) containing at least \(t+r\) elements of \(\{1,\ldots,t+2r\}\), \(r \geq 0\).
theorem erdos_83.variants.ahlswede_khachatrian (m k t : ℕ) (ht : 2 ≤ t) (htk : t ≤ k)
(hkm : k ≤ m) (F : Finset (Finset (Fin m))) (hF : ∀ A ∈ F, A.card = k)
(hinter : ∀ A ∈ F, ∀ B ∈ F, t ≤ (A ∩ B).card) :
∃ r : ℕ, F.card ≤ ({A : Finset (Fin m) | A.card = k ∧
t + r ≤ (A.filter fun i : Fin m => (i : ℕ) < t + 2 * r).card} : Finset _).card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/83.lean, line 88.
Sources
TheoremErdős Problem 85#
Reference: erdosproblems.com/85
Quoted from FormalConjectures/ErdosProblems/85.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/85.
The file states 1 research or textbook statement: 1 open.
Erdos85.erdos_85
Open: stated without proof.
Is it true that, for all large \(n\), \(f(n + 1) \ge f(n)\)?
theorem erdos_85 : ∀ᶠ n in atTop, f n ≤ f (n + 1)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/85.lean, line 44.
Sources
TheoremErdős Problem 86#
References: - erdosproblems.com/86 - [BHLL14] Balogh, József and Hu, Ping and Lidický, Bernard and Liu, Hong, Upper bounds on the size of 4- and 6-cycle-free subgraphs of the hypercube. European J. Combin. (2014), 75-85. - [BHN95] Brass, Peter and Harborth, Heiko and Nienborg, Hauke, On the maximum number of edges in a {\(C_4\)}-free subgraph of {\(Q_n\)}. J. Graph Theory (1995), 17--23. - [Ba12b] R. Baber, Turán densities of hypercubes. arXiv:1201.3587 (2012). - [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.
Quoted from FormalConjectures/ErdosProblems/86.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/86.
The file states 1 research or textbook statement: 1 open.
Erdos86.erdos_86
Open: stated without proof.
Let \(Q_n\) be the \(n\)-dimensional hypercube graph (so that \(Q_n\) has \(2^n\) vertices and \(n2^{n-1}\) edges). Is it true that every subgraph of \(Q_n\) with
\[\geq \left(\frac{1}{2}+o(1)\right)n2^{n-1}\]many edges contains a \(C_4\)?
theorem erdos_86 :
∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop, ∀ H : SimpleGraph (Fin n → Bool),
H ≤ hypercube n →
(1 / 2 + ε) * n * 2 ^ (n - 1 : ℕ) ≤ (H.edgeSet.ncard : ℝ) →
cycleGraph 4 ⊑ H
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/86.lean, line 45.
Sources
TheoremErdős Problem 87#
References: - erdosproblems.com/87 - [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186.
Quoted from FormalConjectures/ErdosProblems/87.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/87.
The file states 2 research or textbook statements: 2 open.
Erdos87.erdos_87.parts.i
Open: stated without proof.
Let \(0 < \epsilon < 1\). Is it true that, if \(k\) is sufficiently large, then
\[R(G) > (1-\epsilon)^k R(k)\]for every graph \(G\) with chromatic number \(\chi(G)=k\)?
The restriction \(\epsilon < 1\) excludes negative bases in \((1-\epsilon)^k\).
This problem is #12 in Ramsey Theory in the graphs problem collection.
theorem erdos_87.parts.i :
∀ ε > (0 : ℝ), ε < 1 → ∀ᶠ k : ℕ in atTop,
∀ (V : Type) [Fintype V] (G : SimpleGraph V), G.chromaticNumber = (k : ℕ∞) →
(SimpleGraph.diagonalGraphRamsey G : ℝ) >
(1 - ε) ^ k * (SimpleGraph.diagonalRamsey k : ℝ)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/87.lean, line 45.
Erdos87.erdos_87.parts.ii
Open: stated without proof.
Even stronger, is there some \(c > 0\) such that, for all large \(k\),
\[R(G) > c R(k)\]for every graph \(G\) with chromatic number \(\chi(G)=k\)?
This problem is #13 in Ramsey Theory in the graphs problem collection.
theorem erdos_87.parts.ii :
∃ c > (0 : ℝ), ∀ᶠ k : ℕ in atTop,
∀ (V : Type) [Fintype V] (G : SimpleGraph V), G.chromaticNumber = (k : ℕ∞) →
(SimpleGraph.diagonalGraphRamsey G : ℝ) > c * (SimpleGraph.diagonalRamsey k : ℝ)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/87.lean, line 60.
Sources
TheoremErdős Problem 88#
References: - erdosproblems.com/88 - [Er92b] Erdős, Paul, Some of my favourite problems in various branches of combinatorics. Matematiche (Catania) (1992), 231-240. - [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186. - [Er97d] Erdős, Paul, Some recent problems and results in graph theory. Discrete Math. (1997), 81-85. - [KSSS22] Kwan, M. and Sah, A. and Sauermann, L. and Sawhney, M., Anticoncentration in Ramsey graphs and a proof of the Erdős-McKay conjecture. Forum Math. Pi 11 (2023), e21. arXiv:2208.02874
Quoted from FormalConjectures/ErdosProblems/88.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/88.
The file states 3 research or textbook statements: 3 solved.
Erdos88.erdos_88
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos88.lean#L127.
For any \(\epsilon>0\) there exists \(\delta=\delta(\epsilon)>0\) such that if \(G\) is a graph on \(n\) vertices with no independent set or clique of size \(\geq \epsilon\log n\) then \(G\) contains an induced subgraph with \(m\) edges for all \(m\leq \delta n^2\).
This was conjectured by Erdős and McKay and proved by Kwan, Sah, Sauermann, and Sawhney [KSSS22]. Erdős' original formulation also assumed that \(G\) has \(\gg n^2\) edges. By an old result of Erdős and Szemerédi this follows from the other condition, so it is omitted here.
theorem erdos_88 :
∀ ε > (0 : ℝ), ∃ δ > (0 : ℝ), ∀ n : ℕ, ∀ G : SimpleGraph (Fin n),
(G.cliqueNum : ℝ) < ε * Real.log n → (G.indepNum : ℝ) < ε * Real.log n →
∀ m : ℕ, (m : ℝ) ≤ δ * n ^ 2 →
∃ S : Finset (Fin n), (G.induce (S : Set (Fin n))).edgeSet.ncard = m
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/88.lean, line 54.
Erdos88.erdos_88.variants.erdos_mckay
Solved: stated here without proof.
Erdős and McKay proved the statement of
erdos_88with \(\delta n^2\) replaced by \(\delta (\log n)^2\). Since \((\log n)^2 \leq n^2\), this weaker bound also follows fromerdos_88.
theorem erdos_88.variants.erdos_mckay :
∀ ε > (0 : ℝ), ∃ δ > (0 : ℝ), ∀ n : ℕ, ∀ G : SimpleGraph (Fin n),
(G.cliqueNum : ℝ) < ε * Real.log n → (G.indepNum : ℝ) < ε * Real.log n →
∀ m : ℕ, (m : ℝ) ≤ δ * Real.log n ^ 2 →
∃ S : Finset (Fin n), (G.induce (S : Set (Fin n))).edgeSet.ncard = m
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/88.lean, line 67.
Erdos88.erdos_88.variants.kwan_sah_sauermann_sawhney
Solved: stated here without proof.
Kwan, Sah, Sauermann, and Sawhney [KSSS22, Theorem 1.1] proved the following stronger statement. Fix \(C > 0\) and \(\eta > 0\), and let \(G\) be a graph on \(n\) vertices with no independent set or clique of size \(\geq C \log_2 n\), where \(n\) is sufficiently large with respect to \(C\) and \(\eta\). Then for every integer \(0 \leq m \leq (1 - \eta) e(G)\) there is an induced subgraph of \(G\) with exactly \(m\) edges.
theorem erdos_88.variants.kwan_sah_sauermann_sawhney :
∀ C > (0 : ℝ), ∀ η > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph (Fin n),
(G.cliqueNum : ℝ) < C * Real.logb 2 n → (G.indepNum : ℝ) < C * Real.logb 2 n →
∀ m : ℕ, (m : ℝ) ≤ (1 - η) * G.edgeSet.ncard →
∃ S : Finset (Fin n), (G.induce (S : Set (Fin n))).edgeSet.ncard = m
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/88.lean, line 82.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.