Erdős Problem 900 to Erdős Problem 923
TheoremErdős Problem 900#
References: - erdosproblems.com/900 - [AKS81] Ajtai, Miklós and Komlós, János and Szemerédi, Endre, The longest path in a random graph. Combinatorica 1 (1981), 1--12. - [Er78] Erdős, Paul, Problems and results in combinatorial analysis and combinatorial number theory. Proceedings of the Ninth Southeastern Conference on Combinatorics, Graph Theory, and Computing (1978), 29-40. PDF
Quoted from FormalConjectures/ErdosProblems/900.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/900.
The file states 1 research or textbook statement: 1 solved. It also has 1 API statement, counted here but not shown.
Erdos900.erdos_900
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos900.lean#L950.
There is a function \(f:(1/2,\infty)\to \mathbb{R}\) such that \(f(c)\to 0\) as \(c\to 1/2\) and \(f(c)\to 1\) as \(c\to \infty\) and every random graph with \(n\) vertices and \(cn\) edges has (with high probability) a path of length at least \(f(c)n\).
Conjectured by Erdős [Er78, p. 32] and proved by Ajtai, Komlós, and Szemerédi [AKS81]. We take the uniform random graph with \(\lfloor cn\rfloor\) edges, count the length of a path in edges, read "with high probability" as probability tending to \(1\) as \(n\to\infty\), and require \(f(c)>0\) for every \(c>1/2\) (a path of linear length). The linked formal proof uses the same uniform model, written as uniformly random \(0/1\) vectors of weight \(\lfloor cn\rfloor\) indexed by the pairs of vertices.
theorem erdos_900 :
∃ f : ℝ → ℝ, (∀ c : ℝ, 1 / 2 < c → 0 < f c) ∧
Tendsto f (𝓝[>] (1 / 2)) (𝓝 0) ∧ Tendsto f atTop (𝓝 1) ∧
∀ c : ℝ, 1 / 2 < c → Tendsto (fun n : ℕ ↦
uniformEdgeProbability n ⌊c * n⌋₊ (HasLongPath n (f c))) atTop (𝓝 1)
Category research solved; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/900.lean, line 72.
Sources
TheoremErdős Problem 901#
References: - erdosproblems.com/901 - [Be77] Beck, J., On a combinatorial problem of {P}. {E}rdős and {L}. {L}ovász. Discrete Math. (1977), 127--131. - [Be78] Beck, J., On {\(3\)}-chromatic hypergraphs. Discrete Math. (1978), 127--137. - [Er63b] Erdős, P., On a combinatorial problem. Nordisk Mat. Tidskr. (1963), 5--10, 40. - [Er64e] Erdős, P., On a combinatorial problem. {II}. Acta Math. Acad. Sci. Hungar. (1964), 445--447. - [ErLo75] Erdős, P. and Lovász, L., Problems and results on {\(3\)}-chromatic hypergraphs and some related questions. (1975), 609--627. - [Pl09] Pluhár, András, Greedy colorings of uniform hypergraphs. Random Structures Algorithms (2009), 216--221. - [RaSr00] Radhakrishnan, Jaikumar and Srinivasan, Aravind, Improved bounds and algorithms for hypergraph {\(2\)}-coloring. Random Structures Algorithms (2000), 4--32.
Quoted from FormalConjectures/ErdosProblems/901.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/901.
The file states 1 research or textbook statement: 1 open.
Erdos901.erdos_901
Open: stated without proof.
Let \(m(n)\) be minimal such that there is an \(n\)-uniform hypergraph with \(m(n)\) edges which is \(3\)-chromatic. Estimate \(m(n)\).
theorem erdos_901 :
(fun n ↦ ((Hypergraph.minChromaticEdges n 3).toNat : ℝ)) =Θ[atTop]
erdos_901.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/901.lean, line 52.
Sources
TheoremErdős Problem 902#
References: - erdosproblems.com/902 - [Er63c] Erdős, P., On a problem in graph theory. Math. Gaz. 47 (1963), 220-223. PDF - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59-79. - [SzSz65] Szekeres, E. and Szekeres, G., On a problem of Schütte and Erdős. Math. Gaz. 49 (1965), 290-293.
Quoted from FormalConjectures/ErdosProblems/902.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/902.
The file states 7 research or textbook statements: 1 open and 6 solved. It also has 2 test statements, counted here but not shown.
Erdos902.erdos_902
Open: stated without proof.
Let \(f(n)\) be minimal such that there is a tournament (a complete directed graph) on \(f(n)\) vertices such that every set of \(n\) vertices is dominated by at least one other vertex. Estimate \(f(n)\).
theorem erdos_902 : (fun n ↦ (f n : ℝ)) =Θ[atTop] erdos_902.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/902.lean, line 90.
Erdos902.erdos_902.variants.f_one
Proved here.
It is easy to check that \(f(1)=3\) and \(f(2)=7\).
This is the statement for \(f(1)\).
theorem erdos_902.variants.f_one : f 1 = 3
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/902.lean, line 99.
Erdos902.erdos_902.variants.f_two
Solved: stated here without proof.
It is easy to check that \(f(1)=3\) and \(f(2)=7\).
This is the statement for \(f(2)\).
theorem erdos_902.variants.f_two : f 2 = 7
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/902.lean, line 130.
Erdos902.erdos_902.variants.erdos_lower
Solved: stated here without proof.
Erdős [Er63c] proved
\[2^{n+1}-1 \leq f(n) \ll n^22^n.\]This is the lower bound.
theorem erdos_902.variants.erdos_lower (n : ℕ) : 2 ^ (n + 1) - 1 ≤ f n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/902.lean, line 140.
Erdos902.erdos_902.variants.erdos_upper
Solved: stated here without proof.
Erdős [Er63c] proved
\[2^{n+1}-1 \leq f(n) \ll n^22^n.\]This is the upper bound, in the form proved in [Er63c, (2)]: \(\limsup_n f(n)2^{-n}n^{-2} \leq \log 2\).
theorem erdos_902.variants.erdos_upper :
∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (f n : ℝ) ≤ (Real.log 2 + ε) * n ^ 2 * 2 ^ n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/902.lean, line 151.
Erdos902.erdos_902.variants.szekeres_f_three
Solved: stated here without proof.
Szekeres and Szekeres [SzSz65] proved that \(f(3)=19\) and
\[n2^n \ll f(n).\]This is the statement for \(f(3)\).
theorem erdos_902.variants.szekeres_f_three : f 3 = 19
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/902.lean, line 162.
Erdos902.erdos_902.variants.szekeres_lower
Solved: stated here without proof.
Szekeres and Szekeres [SzSz65] proved that \(f(3)=19\) and
\[n2^n \ll f(n).\]This is the lower bound.
theorem erdos_902.variants.szekeres_lower :
∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, c * n * 2 ^ n ≤ (f n : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/902.lean, line 172.
Sources
TheoremErdős Problem 903#
References: - erdosproblems.com/903 - [EFSW85] Erdős, P. and Fowler, Joel C. and S\'os, Vera T. and Wilson, Richard M., On {\(2\)}-designs. J. Combin. Theory Ser. A (1985), 131--142. - [dBEr48] de Bruijn, N. G. and Erdős, P., On a combinatorial problem. Nederl. Akad. Wetensch., Proc. (1948), 1277--1279 = Indagationes Math. 10, 421--423.
Quoted from FormalConjectures/ErdosProblems/903.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/903.
The file states 1 research or textbook statement: 1 solved.
Erdos903.erdos_903
Solved: stated here without proof.
Let \(n=p^2+p+1\) for some prime power \(p\), and let \(A_1,\ldots,A_t\subseteq \{1,\ldots,n\}\) be a block design (so that every pair \(x,y\in \{1,\ldots,n\}\) is contained in exactly one \(A_i\)). Is it true that if \(t>n\) then \(t\geq n+p\)?
This is true, and was proved by Erdős, Fowler, Sós, and Wilson [EFSW85].
theorem erdos_903 :
∀ p : ℕ, IsPrimePow p →
∀ H : Finset (Finset (Fin (p ^ 2 + p + 1))),
H.IsPairwiseBalancedDesign → p ^ 2 + p + 1 < H.card →
p ^ 2 + p + 1 + p ≤ H.card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/903.lean, line 45.
Sources
TheoremErdős Problem 904#
References: - erdosproblems.com/904 - [BoEr75] Bollobás, B. and Erdős, P., Unsolved Problems. Proc. Fifth British Combinatorial Conf. (1975), 678-680. - [Er75] Erdős, P., Some recent progress on extremal problems in graph theory. Congr. Numer. (1975), 3-14. - [Ed78] Edwards, C. S., Complete subgraphs with largest sum of vertex degrees. (1978), 293-306. - [Fa92] Faudree, Ralph J., Complete subgraphs with large degree sums. J. Graph Theory (1992), 327-334. - [BoNi05] Bollobás, Béla and Nikiforov, Vladimir, The sum of degrees in cliques. Electron. J. Combin. (2005), Note 21, 10.
Quoted from FormalConjectures/ErdosProblems/904.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/904.
The file states 1 research or textbook statement: 1 solved.
Erdos904.erdos_904
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos904.lean.
Let \(r\geq 2\) and let \(t_r(n)\) be the Turán number (the maximal number of edges in a graph on \(n\) vertices with no \(K_{r+1}\)).
If \(G\) is a graph with \(n\) vertices and \(m\geq t_r(n)\) edges there exists a clique on \(r\) vertices, say \(x_1,\ldots,x_r\), such that
\[d(x_1)+\cdots+d(x_r)\geq \frac{2rm}{n}.\]A conjecture of Bollobás and Erdős. This was conjectured in [Er75] only in the special case \(r=3\). Edwards [Ed78] proved the conjecture for \(2\leq r\leq 8\) (under the additional assumption that \(n\geq r^2\)). Faudree [Fa92] proved the conjecture for all \(r\geq 2\) provided \(n>\frac{r-1}{4}r^2\). The full conjecture was proved by Bollobás and Nikiforov [BoNi05].
theorem erdos_904 :
∀ (V : Type*) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]
(r : ℕ) (hr : r ∈ Set.Icc 1 (n V)) (hm : turanNumber (n V) r ≤ #G.edgeFinset),
∃ s, G.IsNClique r s ∧ 2 * r * #G.edgeFinset ≤ n V * ∑ v ∈ s, G.degree v
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/904.lean, line 55.
Sources
TheoremErdős Problem 905#
References: - erdosproblems.com/905 - [KhNi79] Khadzhiivanov, N. G. and Nikiforov, S. V., Solution of a problem of P. Erdős about the maximum number of triangles with a common edge in a graph. C. R. Acad. Bulgare Sci. (1979), 1315-1318.
Quoted from FormalConjectures/ErdosProblems/905.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/905.
The file states 1 research or textbook statement: 1 solved.
Erdos905.erdos_905
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos905.lean.
Every graph with \(n\) vertices and \(>n^2/4\) edges contains an edge which is in at least \(n/6\) triangles.
A conjecture of Bollobás and Erdős. This was proved independently by Edwards (unpublished) and Khadzhiivanov and Nikiforov [KhNi79].
theorem erdos_905 (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
(hG : (n : ℝ) ^ 2 / 4 < (#G.edgeFinset : ℝ)) :
∃ e ∈ G.edgeFinset, (n : ℝ) / 6 ≤ (#(G.trianglesContaining e) : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/905.lean, line 45.
Sources
TheoremErdős Problem 906#
Reference: erdosproblems.com/906
Quoted from FormalConjectures/ErdosProblems/906.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/906.
The file states 1 research or textbook statement: 1 open.
Erdos906.erdos_906
Open: stated without proof.
Does there exists an entire non-zero transcendental function
f : ℂ → ℂsuch that for any sequencen₀ < n₁ < ...,{ z | ∃ k, iteratedDeriv (n k) f z = 0 }is dense.
theorem erdos_906 : ∃ f : ℂ → ℂ, Transcendental (Polynomial ℂ) f ∧
Differentiable ℂ f ∧ ∀ n : ℕ → ℕ, StrictMono n →
Dense { z | ∃ k, iteratedDeriv (n k) f z = 0 }
Category research open; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/906.lean, line 33.
Sources
TheoremErdős Problem 907#
References: - erdosproblems.com/907 - [dB51] de Bruijn, N. G., Functions whose differences belong to a given class. Nieuw Arch. Wiskunde (2) (1951), 194-218.
Quoted from FormalConjectures/ErdosProblems/907.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/907.
The file states 1 research or textbook statement: 1 solved.
Erdos907.erdos_907
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos907.lean.
Let \(f:\mathbb{R}\to \mathbb{R}\) be such that \(f(x+h)-f(x)\) is continuous for every \(h>0\). Is it true that
\[f=g+h\]for some continuous \(g\) and additive \(h\) (i.e. \(h(x+y)=h(x)+h(y)\))?
A conjecture of Erdős from the early 1950s. Answered in the affirmative by de Bruijn [dB51].
theorem erdos_907 :
∀ f : ℝ → ℝ, (∀ h : ℝ, 0 < h → Continuous fun x => f (x + h) - f x) →
∃ g a : ℝ → ℝ, Continuous g ∧ (∀ x y, a (x + y) = a x + a y) ∧ f = g + a
Category research solved; AMS 26 Real functions, 39 Difference and functional equations. Declared in FormalConjectures/ErdosProblems/907.lean, line 43.
Sources
TheoremErdős Problem 910#
References: - erdosproblems.com/910 - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79. PDF - [Er44] Erdős, P., Some remarks on connected sets. Bull. Amer. Math. Soc. 50 (1944), 442-446. PDF - [Ru58] Rudin, M. E., A connected subset of the plane. Fund. Math. 46 (1958), 15-24.
Quoted from FormalConjectures/ErdosProblems/910.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/910.
The file states 3 research or textbook statements: 2 open and 1 solved.
Erdos910.erdos_910.parts.i
Open: stated without proof.
Does every connected set in \(\mathbb{R}^n\) contain a connected subset which is not a point and not homeomorphic to the original set?
Asked by Erdős [Er44, p. 445], see also [Er82e, p. 77]. Following [Er44, pp. 443 and 445], a single point is not a connected set, so \(X\) is required to have more than one point.
Erdős [Er82e, p. 77] reports that Rudin, assuming the continuum hypothesis, found counterexamples to both questions of this problem. The theorem of [Ru58] (
erdos_910.variants.rudin_CH) does not say that Rudin's set is homeomorphic to its connected subsets with more than one point. A counterexample that assumes the continuum hypothesis would not disprove this statement in ZFC.
theorem erdos_910.parts.i :
∀ (n : ℕ) (X : Set (EuclideanSpace ℝ (Fin n))), IsConnected X → X.Nontrivial →
∃ Y ⊆ X, IsConnected Y ∧ Y.Nontrivial ∧ ¬ Nonempty (Y ≃ₜ X)
Category research open; AMS 54 General topology. Declared in FormalConjectures/ErdosProblems/910.lean, line 51.
Erdos910.erdos_910.parts.ii
Open: stated without proof.
If \(n\geq 2\) does every connected set in \(\mathbb{R}^n\) contain more than \(2^{\aleph_0}\) many connected subsets?
Erdős [Er82e, p. 77] asks this for connected sets of dimension greater than one; [Er44, p. 446] asks, for these sets, for \(2^{\mathfrak{c}}\) connected subsets. The condition \(n\geq 2\) alone would make the answer trivially no: a segment in \(\mathbb{R}^2\) has only \(2^{\aleph_0}\) connected subsets, its intervals. So we require
1 < smallInductiveDimension X, which agrees with the covering dimension for subsets of \(\mathbb{R}^n\). As inerdos_910.parts.i, single points are not counted as connected sets [Er44, p. 445].Rudin's set \(M\) [Ru58] has at most \(2^{\aleph_0}\) connected subsets, since each one with more than one point is \(M\) minus a countable set. But \(M\) lies in Rudin's continuum \(I=\bigcap_n\Gamma_n^*\), where each \(\Gamma_n\) is a chain of \(2\)-cells whose links have diameter less than \(1/n\) [Ru58, 1.1-1.2], so \(I\), and hence \(M\), has dimension at most one. Rudin's set therefore does not answer this question as Erdős states it.
theorem erdos_910.parts.ii :
∀ (n : ℕ) (X : Set (EuclideanSpace ℝ (Fin n))), IsConnected X →
1 < smallInductiveDimension X →
𝔠 < Cardinal.mk {Y : Set (EuclideanSpace ℝ (Fin n)) |
Y ⊆ X ∧ IsConnected Y ∧ Y.Nontrivial}
Category research open; AMS 54 General topology. Declared in FormalConjectures/ErdosProblems/910.lean, line 74.
Erdos910.erdos_910.variants.rudin_CH
Solved: stated here without proof.
Assume the continuum hypothesis. Rudin [Ru58, p. 15] constructed a connected subset \(M\) of the plane, with more than one point, such that \(M\setminus N\) is at most countable for every connected subset \(N\subseteq M\) with more than one point.
This disproves a conjecture of Erdős [Er44, p. 443] that every connected set \(C\) contains a connected subset \(C'\) such that \(C\setminus C'\) has cardinality \(2^{\aleph_0}\). Erdős [Er82e, p. 77] reports that Rudin's examples answer both questions of this problem in the negative; see the docstrings of
erdos_910.parts.ianderdos_910.parts.ii.
theorem erdos_910.variants.rudin_CH :
(ℵ₁ = 𝔠) → ∃ M : Set (EuclideanSpace ℝ (Fin 2)), IsConnected M ∧ M.Nontrivial ∧
∀ N ⊆ M, IsConnected N → N.Nontrivial → (M \ N).Countable
Category research solved; AMS 54 General topology. Declared in FormalConjectures/ErdosProblems/910.lean, line 92.
Sources
TheoremErdős Problem 911#
References: - erdosproblems.com/911 - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79.
Quoted from FormalConjectures/ErdosProblems/911.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/911.
The file states 1 research or textbook statement: 1 open.
Erdos911.erdos_911
Open: stated without proof.
Let \(\hat{R}(G)\) denote the size Ramsey number, the minimal number of edges \(m\) such that there is a graph \(H\) with \(m\) edges that is Ramsey for \(G\).
Is there a function \(f\) such that \(f(x)/x\to \infty\) as \(x\to \infty\) such that, for all large \(C\), if \(G\) is a graph with \(n\) vertices and \(e\geq Cn\) edges then
\[\hat{R}(G) > f(C) e?\]Here \(\hat{R}(G)\) is
sizeRamsey G G, and \(G\) has at least one vertex (for \(n = 0\) the inequality fails trivially).
theorem erdos_911 :
∃ f : ℝ → ℝ, Tendsto (fun x ↦ f x / x) atTop atTop ∧
∃ C₀ : ℝ, ∀ C ≥ C₀, ∀ (n : ℕ) (G : SimpleGraph (Fin n)), 0 < n →
C * n ≤ (G.edgeSet.ncard : ℝ) →
f C * G.edgeSet.ncard < (sizeRamsey G G : ℝ)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/911.lean, line 47.
Sources
TheoremErdős Problem 912#
References: - erdosproblems.com/912 - [Er82c] Erdős, P., Miscellaneous problems in number theory. Congr. Numer. (1982), 25-45.
Quoted from FormalConjectures/ErdosProblems/912.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/912.
The file states 3 research or textbook statements: 2 open and 1 solved.
Erdos912.erdos_912.variants.selfridge
Solved: stated here without proof.
Erdős and Selfridge prove in [Er82c] that \(h(n) \asymp \left(\frac{n}{\log n}\right)^{1/2}\).
theorem erdos_912.variants.selfridge :
(fun n => (h n : ℝ)) =Θ[atTop] (fun n => (n / Real.log n) ^ (1 / 2 : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/912.lean, line 41.
Erdos912.erdos_912
Open: stated without proof.
Prove that there exists some \(c>0\) such that
\[h(n) \sim c \left(\frac{n}{\log n}\right)^{1/2}\]as \(n\to \infty\).
theorem erdos_912 : ∃ c > 0,
(fun n => (h n : ℝ)) ~[atTop] (fun n => c * (n / Real.log n) ^ (1 / 2 : ℝ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/912.lean, line 50.
Erdos912.erdos_912.variants.tao
Open: stated without proof.
A heuristic of Tao using the Cramér model for the primes suggests this is true with \(c=\sqrt{2\pi}\).
theorem erdos_912.variants.tao :
(fun n => (h n : ℝ)) ~[atTop] (fun n => √(2 * Real.pi) * (n / Real.log n) ^ (1 / 2 : ℝ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/912.lean, line 57.
Sources
TheoremErdős Problem 913#
Reference: erdosproblems.com/913
Reviewed by @b-mehta on 2025-05-27
Quoted from FormalConjectures/ErdosProblems/913.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/913.
The file states 3 research or textbook statements: 2 open and 1 solved.
Erdos913.erdos_913
Open: stated without proof.
Are there infinitely many \(n\) such that if
\[ n(n + 1) = \prod_i p_i^{k_i} \]is the factorisation into distinct primes then all exponents \(k_i\) are distinct?
theorem erdos_913 :
{ n | Set.InjOn (n * (n + 1)).factorization (n * (n + 1)).primeFactors }.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/913.lean, line 40.
Erdos913.erdos_913.variants.infinite_many_8p_sq_add_one_primes
Open: stated without proof.
It is likely that there are infinitely many primes \(p\) such that \(8p^2 - 1\) is also prime.
theorem erdos_913.variants.infinite_many_8p_sq_add_one_primes :
{ p | p.Prime ∧ (8 * p ^ 2 - 1).Prime }.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/913.lean, line 48.
Erdos913.erdos_913.variants.conditional
Proved here.
If there are infinitely many primes \(p\) such that \(8p^2 - 1\) is prime, then this is true.
theorem erdos_913.variants.conditional (h : { p | p.Prime ∧ (8 * p ^ 2 - 1).Prime }.Infinite) :
{ n | Set.InjOn (n * (n + 1)).factorization (n * (n + 1)).primeFactors }.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/913.lean, line 54.
Sources
TheoremErdős Problem 914#
References: - erdosproblems.com/914 - [CoHa63] Corrádi, K. and Hajnal, A., On the maximal number of independent circuits in a graph. Acta Math. Acad. Sci. Hungar. (1963), 423-439. - [HaSz70] Hajnal, A. and Szemerédi, E., Proof of a conjecture of P. Erdős. (1970), 601-623. - [KiKo08] Kierstead, H. A. and Kostochka, A. V., A short proof of the Hajnal-Szemerédi theorem on equitable colouring. Combin. Probab. Comput. (2008), 265-270.
Quoted from FormalConjectures/ErdosProblems/914.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/914.
The file states 2 research or textbook statements: 2 solved.
Erdos914.erdos_914
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos914.lean.
Let \(r\geq 2\) and \(m\geq 1\). Every graph with \(rm\) vertices and minimum degree at least \(m(r-1)\) contains \(m\) vertex disjoint copies of \(K_r\).
When \(r=2\) this follows from Dirac's theorem. Corrádi and Hajnal [CoHa63] proved this when \(r=3\). Hajnal and Szemerédi [HaSz70] proved this for all \(r\geq 4\).
A shorter proof was given by Kierstead and Kostochka [KiKo08].
theorem erdos_914 {r m : ℕ} (hr : 2 ≤ r) (hm : 1 ≤ m) {V : Type*} [Fintype V]
(G : SimpleGraph V) [DecidableRel G.Adj] (hV : Fintype.card V = r * m)
(hdeg : m * (r - 1) ≤ G.minDegree) :
∃ K : Fin m → Finset V, (∀ i, G.IsNClique r (K i)) ∧
Pairwise fun i j => Disjoint (K i) (K j)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/914.lean, line 47.
Erdos914.erdos_914.variants.equitable_colouring
Solved: stated here without proof.
Equivalently, every graph with \(rm\) vertices and maximum degree at most \(m-1\) has a proper vertex colouring with \(m\) colours in which every colour class has exactly \(r\) vertices (an equitable colouring).
theorem erdos_914.variants.equitable_colouring {r m : ℕ} (hr : 2 ≤ r) (hm : 1 ≤ m) {V : Type*}
[Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hV : Fintype.card V = r * m)
(hdeg : G.maxDegree ≤ m - 1) :
∃ C : G.Coloring (Fin m), ∀ i, (C.colorClass i).ncard = r
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/914.lean, line 60.
Sources
TheoremErdős Problem 915#
References: - erdosproblems.com/915 - [BoEr62] Bollobás, Béla and Erdős, Pál, Extremal problems in graph theory. Mat. Lapok (1962), 143--152. - [Er67b] Erdős, Paul, Extremal problems in graph theory. A Seminar on Graph Theory (1967), 54-59. - [Ba60] P. Bártfai, Solution of a problem posed by P. Erdős. Mat. Lapok (1960), 175-176. - [Bo66] Bollobás, B., On graphs with at most three independent paths connecting any two vertices. Studia Sci. Math. Hungar. (1966), 137--140. - [Le73] Leonard, John L., On a conjecture of Bollobás and Erdős. Period. Math. Hungar. (1973), 281--284. - [Ma73] Mader, W., Ein Extremalproblem des Zusammenhangs von Graphen. Math. Z. (1973), 223--231. - [SoTh74] Sørensen, Bo Aagaard and Thomassen, Carsten, On \(k\)-rails in graphs. J. Combinatorial Theory Ser. B (1974), 143--159.
Quoted from FormalConjectures/ErdosProblems/915.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/915.
The file states 2 research or textbook statements: 2 solved.
Erdos915.erdos_915
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos915.lean#L362.
Let \(G\) be a graph with \(1+n(m-1)\) vertices and \(1+n\binom{m}{2}\) edges. Must \(G\) contain two points which are connected by \(m\) disjoint paths?
A conjecture of Bollobás and Erdős [BoEr62]. This would be the best possible, as demonstrated by \(n\) copies of \(K_m\) which share a single vertex (but are otherwise disjoint). It is unclear whether disjoint here is to mean edge-disjoint or (internally) vertex-disjoint. The above construction is valid for either interpretation.
This is the internally vertex-disjoint reading. It is trivial for \(m = 2\), and was proved for \(m = 3\) by Bártfai [Ba60] and for \(m = 4\) by Bollobás [Bo66]. Leonard [Le73] disproved this conjecture for \(m=5\), giving an explicit counterexample with \(57\) vertices and \(141\) edges, and Mader [Ma73] disproved the conjecture in general for all \(m \geq 6\). Sørensen and Thomassen [SoTh74] proved that the conjectured bound of Bollobás and Erdős holds if the graph is \(3\)-connected.
theorem erdos_915 :
¬ ∀ m n : ℕ, 2 ≤ m → 1 ≤ n → ∀ (V : Type) [Fintype V] (G : SimpleGraph V),
Fintype.card V = 1 + n * (m - 1) → G.edgeSet.ncard = 1 + n * m.choose 2 →
∃ u v : V, u ≠ v ∧ ∃ P : Finset (G.Walk u v), P.card = m ∧ (∀ p ∈ P, p.IsPath) ∧
(P : Set (G.Walk u v)).Pairwise InternallyDisjoint
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/915.lean, line 65.
Erdos915.erdos_915.variants.edge_disjoint
Solved: stated here without proof.
The edge-disjoint reading of erdős_915. Mader [Ma73] proved that if a graph with \(n\) vertices has more than
\[\frac{m}{2}(n-1)-\frac{1}{2}(e_0(G)+\cdots+e_{m-2}(G))\]edges then \(G\) contains two vertices connected by \(m\) edge-disjoint paths (where \(e_r(G)\) counts the number of vertices of degree \(\leq r\)). In particular, this confirms (and is stronger than) the conjecture.
theorem erdos_915.variants.edge_disjoint :
∀ m n : ℕ, 2 ≤ m → 1 ≤ n → ∀ (V : Type) [Fintype V] (G : SimpleGraph V),
Fintype.card V = 1 + n * (m - 1) → G.edgeSet.ncard = 1 + n * m.choose 2 →
∃ u v : V, u ≠ v ∧ ∃ P : Finset (G.Walk u v), P.card = m ∧ (∀ p ∈ P, p.IsPath) ∧
(P : Set (G.Walk u v)).Pairwise fun p q => List.Disjoint p.edges q.edges
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/915.lean, line 81.
Sources
TheoremErdős Problem 917#
References: - erdosproblems.com/917 - [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. PDF - [Er93] Erdős, P., Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. 16 (1993), 333-350. - [Di52] Dirac, G. A., A property of \(4\)-chromatic graphs and some remarks on critical graphs. J. London Math. Soc. 27 (1952), 85-92. - [To70] Toft, B., On the maximal number of edges of critical \(k\)-chromatic graphs. Studia Sci. Math. Hungar. 5 (1970), 461-470. - [St87] Stiebitz, M., Subgraphs of colour-critical graphs. Combinatorica 7 (1987), 303-312. - [LMY23] Luo, C., Ma, J. and Yang, T., On the maximum number of edges in \(k\)-critical graphs. Combin. Probab. Comput. 32 (2023), 900-911. arXiv:2301.01656
The question is due to Erdős [Er69b, p. 28]; see also [Er93, p. 341]. See also erdosproblems.com/944 and erdosproblems.com/1032.
Quoted from FormalConjectures/ErdosProblems/917.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/917.
The file states 10 research or textbook statements: 2 open and 8 solved. It also has 1 test statement and 1 API statement, counted here but not shown.
Erdos917.erdos_917.parts.i
Solved: stated here without proof.
Let \(k\geq 4\) and \(f_k(n)\) be the largest number of edges in a graph on \(n\) vertices which has chromatic number \(k\) and is critical (i.e. deleting any edge reduces the chromatic number).
Is it true that
\[f_k(n) \gg_k n^2?\]This is the first part. It was proved by Toft [To70]. We read \(\gg_k\) as: for each \(k\) there is \(c > 0\) with \(f_k(n) \geq cn^2\) for all large \(n\).
theorem erdos_917.parts.i :
∀ k : ℕ, 4 ≤ k → ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop, c * (n : ℝ) ^ 2 ≤ (f k n : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/917.lean, line 105.
Erdos917.erdos_917.parts.ii
Open: stated without proof.
Let \(k\geq 4\) and \(f_k(n)\) be the largest number of edges in a graph on \(n\) vertices which has chromatic number \(k\) and is critical (i.e. deleting any edge reduces the chromatic number).
Is it true that
\[f_6(n)\sim n^2/4?\]This is the second part.
theorem erdos_917.parts.ii :
(fun n : ℕ ↦ (f 6 n : ℝ)) ~[atTop] (fun n : ℕ ↦ (n : ℝ) ^ 2 / 4)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/917.lean, line 119.
Erdos917.erdos_917.parts.iii
Solved: stated here without proof.
Let \(k\geq 4\) and \(f_k(n)\) be the largest number of edges in a graph on \(n\) vertices which has chromatic number \(k\) and is critical (i.e. deleting any edge reduces the chromatic number).
More generally, is it true that, for \(k\geq 6\),
\[f_k(n) \sim \frac{1}{2}\left(1-\frac{1}{\lfloor k/3\rfloor}\right)n^2?\]This is the third part. It has a negative answer: the constructions in
erdos_917.variants.lower_constructiondisprove it for \(k \not\equiv 0 \pmod 3\) (seeerdos_917.variants.not_asymptotic).
theorem erdos_917.parts.iii :
¬ ∀ k : ℕ, 6 ≤ k → (fun n : ℕ ↦ (f k n : ℝ)) ~[atTop] conjecturedValue k
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/917.lean, line 135.
Erdos917.erdos_917.variants.lower_construction
Solved: stated here without proof.
Constructions of Stiebitz [St87] show that, for \(k\geq 6\), there exist infinitely many values of \(n\) such that
\[f_k(n) \geq \frac{1}{2}\left(1-\frac{1}{\lfloor k/3\rfloor+\delta_k}\right)n^2\]where \(\delta_k=0\) if \(k\equiv 0\pmod{3}\), \(\delta_k=1/7\) if \(k\equiv 1\pmod{3}\), and \(\delta_k = 24/69\) if \(k\equiv 2\pmod{3}\).
[LMY23] state the same bound in the form \((\frac12-\frac{3}{2k-\delta_k'})n^2\) with \(\delta_k'=0,8/7,44/23\), and credit the constructions to Toft [To70].
theorem erdos_917.variants.lower_construction (k : ℕ) (hk : 6 ≤ k) :
∃ᶠ n : ℕ in atTop,
1 / 2 * (1 - 1 / (((k / 3 : ℕ) : ℝ) + delta k)) * (n : ℝ) ^ 2 ≤ (f k n : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/917.lean, line 150.
Erdos917.erdos_917.variants.not_asymptotic
Solved: stated here without proof.
The constructions in
erdos_917.variants.lower_constructiondisprove Erdős' conjectured asymptotic \(f_k(n) \sim \frac{1}{2}\left(1-\frac{1}{\lfloor k/3\rfloor}\right)n^2\) for \(k\not\equiv 0\pmod{3}\), \(k \geq 6\).
theorem erdos_917.variants.not_asymptotic (k : ℕ) (hk : 6 ≤ k) (h3 : ¬ 3 ∣ k) :
¬ (fun n : ℕ ↦ (f k n : ℝ)) ~[atTop] conjecturedValue k
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/917.lean, line 161.
Erdos917.erdos_917.variants.three_dvd
Open: stated without proof.
The remaining case of the third question: is it true that, for \(k\geq 6\) with \(3 \mid k\),
\[f_k(n) \sim \frac{1}{2}\left(1-\frac{1}{\lfloor k/3\rfloor}\right)n^2?\]For \(k = 6\) this is
erdos_917.parts.ii.
theorem erdos_917.variants.three_dvd :
∀ k : ℕ, 6 ≤ k → 3 ∣ k → (fun n : ℕ ↦ (f k n : ℝ)) ~[atTop] conjecturedValue k
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/917.lean, line 171.
Erdos917.erdos_917.variants.dirac
Solved: stated here without proof.
In fact Dirac [Di52] proved
\[f_6(4n+2) \geq 4n^2+8n+3,\]as witnessed by taking two disjoint copies of \(C_{2n+1}\) and adding all edges between them.
We take \(n \geq 1\), so that \(C_{2n+1}\) is a cycle.
theorem erdos_917.variants.dirac (n : ℕ) (hn : 1 ≤ n) :
4 * n ^ 2 + 8 * n + 3 ≤ f 6 (4 * n + 2)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/917.lean, line 183.
Erdos917.erdos_917.variants.erdos_three_dvd
Solved: stated here without proof.
Erdős [Er69b] observed that Dirac's construction generalises to show that, if \(3\mid k\), there are infinitely many values of \(n\) (those of the shape \(mk/3\) where \(m\) is odd) such that
\[f_k(n) \geq \frac{1}{2}\left(1-\frac{1}{k/3}\right)n^2 + n.\]We take \(m \geq 3\), so that the cycle \(C_m\) exists.
theorem erdos_917.variants.erdos_three_dvd (k : ℕ) (hk : 3 ≤ k) (h3 : 3 ∣ k) (m : ℕ)
(hm : Odd m) (hm3 : 3 ≤ m) :
conjecturedValue k (m * (k / 3)) + ((m * (k / 3) : ℕ) : ℝ) ≤ (f k (m * (k / 3)) : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/917.lean, line 195.
Erdos917.erdos_917.variants.stiebitz_upper
Solved: stated here without proof.
Stiebitz also proved the general upper bound
\[f_k(n) < \mathrm{ex}(n;K_{k-1})\sim \frac{1}{2}\left(1-\frac{1}{k-2}\right)n^2\]for large \(n\).
Here \(k \geq 4\), as in [LMY23].
theorem erdos_917.variants.stiebitz_upper (k : ℕ) (hk : 4 ≤ k) :
∀ᶠ n : ℕ in atTop,
f k n < SimpleGraph.extremalNumber n (SimpleGraph.completeGraph (Fin (k - 1)))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/917.lean, line 208.
Erdos917.erdos_917.variants.luo_ma_yang
Solved: stated here without proof.
Luo, Ma, and Yang [LMY23] have improved this upper bound to
\[f_k(n) \leq \frac{1}{2}\left(1-\frac{1}{k-2}-\frac{1}{36(k-1)^2}+o(1)\right)n^2.\][LMY23, Theorem 1.1] proves the stronger bound \(f_k(n) \leq \mathrm{ex}(n;K_{k-1}) - \frac{n^2}{36(k-1)^2}\) for \(k \geq 4\) and all large \(n\), where \(\mathrm{ex}(n;K_{k-1})\) is the number of edges of the Turán graph \(T_{k-2}(n)\). We state this form.
theorem erdos_917.variants.luo_ma_yang (k : ℕ) (hk : 4 ≤ k) :
∀ᶠ n : ℕ in atTop, (f k n : ℝ) ≤
(SimpleGraph.extremalNumber n (SimpleGraph.completeGraph (Fin (k - 1))) : ℝ) -
(n : ℝ) ^ 2 / (36 * ((k : ℝ) - 1) ^ 2)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/917.lean, line 222.
Sources
TheoremErdős Problem 918#
References: - erdosproblems.com/918 - [ErHa68b] Erdős, P. and Hajnal, A., On chromatic number of infinite graphs. (1968), 83--98. - [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.
Quoted from FormalConjectures/ErdosProblems/918.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/918.
The file states 9 research or textbook statements: 4 open, 1 solved and 4 textbook results.
Erdos918.erdos_918.parts.i
Open: stated without proof.
Is there a graph with \(\aleph_2\) vertices and chromatic number \(\aleph_2\) such that every subgraph on \(\aleph_1\) vertices has chromatic number \(\leq\aleph_0\)?
theorem erdos_918.parts.i :
∃ (V : Type u) (G : SimpleGraph V), #V = ℵ_ 2 ∧ G.chromaticCardinal = ℵ_ 2 ∧
∀ (W : Set V) (_ : #W = ℵ₁), (G.induce W).chromaticCardinal ≤ ℵ₀
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/918.lean, line 41.
Erdos918.erdos_918.parts.ii
Open: stated without proof.
Is there a graph with \(\aleph_{\omega+1}\) vertices and chromatic number \(\aleph_1\) such that every subgraph on \(\aleph_\omega\) vertices has chromatic number \(\leq\aleph_0\)?
theorem erdos_918.parts.ii :
∃ (V : Type u) (G : SimpleGraph V), #V = ℵ_ (ω + 1) ∧ G.chromaticCardinal = ℵ₁ ∧
∀ (W : Set V) (_ : #W = ℵ_ ω), (G.induce W).chromaticCardinal ≤ ℵ₀
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/918.lean, line 52.
Erdos918.erdos_918.variants.all_subgraphs.parts.i
Open: stated without proof.
Is there a graph with \(\aleph_2\) vertices and chromatic number \(\aleph_2\) such that every subgraph on \(\aleph_1\) vertices has chromatic number \(\leq\aleph_0\)?
theorem erdos_918.variants.all_subgraphs.parts.i :
∃ (V : Type u) (G : SimpleGraph V), #V = ℵ_ 2 ∧ G.chromaticCardinal = ℵ_ 2 ∧
∀ (H : G.Subgraph) (_ : #H.verts = ℵ₁), H.coe.chromaticCardinal ≤ ℵ₀
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/918.lean, line 66.
Erdos918.erdos_918.variants.all_subgraphs.parts.ii
Open: stated without proof.
Is there a graph with \(\aleph_{\omega+1}\) vertices and chromatic number \(\aleph_1\) such that every subgraph on \(\aleph_\omega\) vertices has chromatic number \(\leq\aleph_0\)?
theorem erdos_918.variants.all_subgraphs.parts.ii :
∃ (V : Type u) (G : SimpleGraph V), #V = ℵ_ (ω + 1) ∧ G.chromaticCardinal = ℵ₁ ∧
∀ (H : G.Subgraph) (_ : #H.verts = ℵ_ ω), H.coe.chromaticCardinal ≤ ℵ₀
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/918.lean, line 74.
Erdos918.erdos_918.variants.erdos_hajnal
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/82c9238052cac467baaf930d5dbe8ae6191a574c/erdos-918/Solution.lean#L56.
A question of Erd\H{o}s and Hajnal [ErHa68b], who proved, assuming the generalized continuum hypothesis, that for every finite \(k \geq 1\) there is a graph with chromatic number \(\aleph_1\) and \(\aleph_k\) vertices where each subgraph on less than \(\aleph_k\) vertices has chromatic number \(\leq \aleph_0\).
theorem erdos_918.variants.erdos_hajnal (hGCH : ∀ c : Cardinal.{u}, ℵ₀ ≤ c → 2 ^ c = Order.succ c)
(k : ℕ) (hk : 0 < k) : ∃ (V : Type u) (G : SimpleGraph V),
#V = ℵ_ k ∧ G.chromaticCardinal = ℵ₁ ∧
∀ (W : Set V) (_ : #W < ℵ_ k), (G.induce W).chromaticCardinal ≤ ℵ₀
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/918.lean, line 89.
Erdos918.erdos_918.variants.eq_aleph_0.parts.i
Textbook result, stated without proof. A Lean proof is at https://github.com/linrock/math-proofs/blob/82c9238052cac467baaf930d5dbe8ae6191a574c/erdos-918/Solution.lean#L62.
In [Er69b] the questions are stated with \(= \aleph_0\) rather than \(\leq\aleph_0\). This is a likely typo since it can be shown that no such graph exists in this case.
This is the first question with induced subgraphs.
theorem erdos_918.variants.eq_aleph_0.parts.i :
¬∃ (V : Type u) (G : SimpleGraph V), #V = ℵ_ 2 ∧ G.chromaticCardinal = ℵ_ 2 ∧
∀ (W : Set V) (_ : #W = ℵ₁), (G.induce W).chromaticCardinal = ℵ₀
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/918.lean, line 106.
Erdos918.erdos_918.variants.eq_aleph_0_all_subgraphs.parts.i
Textbook result, stated without proof. A Lean proof is at https://github.com/linrock/math-proofs/blob/82c9238052cac467baaf930d5dbe8ae6191a574c/erdos-918/Solution.lean#L67.
In [Er69b] the questions are stated with \(= \aleph_0\) rather than \(\leq\aleph_0\). This is a likely typo since it can be shown that no such graph exists in this case.
This is the first question with all subgraphs.
theorem erdos_918.variants.eq_aleph_0_all_subgraphs.parts.i :
¬∃ (V : Type u) (G : SimpleGraph V), #V = ℵ_ 2 ∧ G.chromaticCardinal = ℵ_ 2 ∧
∀ (H : G.Subgraph) (_ : #H.verts = ℵ₁), H.coe.chromaticCardinal = ℵ₀
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/918.lean, line 117.
Erdos918.erdos_918.variants.eq_aleph_0.parts.ii
Textbook result, stated without proof. A Lean proof is at https://github.com/linrock/math-proofs/blob/82c9238052cac467baaf930d5dbe8ae6191a574c/erdos-918/Solution.lean#L72.
In [Er69b] the questions are stated with \(= \aleph_0\) rather than \(\leq\aleph_0\). This is a likely typo since it can be shown that no such graph exists in this case.
This is the second question with induced subgraphs.
theorem erdos_918.variants.eq_aleph_0.parts.ii :
¬∃ (V : Type u) (G : SimpleGraph V), #V = ℵ_ (ω + 1) ∧ G.chromaticCardinal = ℵ₁ ∧
∀ (W : Set V) (_ : #W = ℵ_ ω), (G.induce W).chromaticCardinal = ℵ₀
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/918.lean, line 133.
Erdos918.erdos_918.variants.eq_aleph_0_all_subgraphs.parts.ii
Textbook result, stated without proof. A Lean proof is at https://github.com/linrock/math-proofs/blob/82c9238052cac467baaf930d5dbe8ae6191a574c/erdos-918/Solution.lean#L78.
In [Er69b] the questions are stated with \(= \aleph_0\) rather than \(\leq\aleph_0\). This is a likely typo since it can be shown that no such graph exists in this case.
This is the second question with all subgraphs.
theorem erdos_918.variants.eq_aleph_0_all_subgraphs.parts.ii :
¬∃ (V : Type u) (G : SimpleGraph V), #V = ℵ_ (ω + 1) ∧ G.chromaticCardinal = ℵ₁ ∧
∀ (H : G.Subgraph) (_ : #H.verts = ℵ_ ω), H.coe.chromaticCardinal = ℵ₀
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/918.lean, line 144.
Sources
TheoremErdős Problem 920#
References: - erdosproblems.com/166 - erdosproblems.com/920 - erdosproblems.com/986 - erdosproblems.com/1104 - [Br26] D. Brada\v{c}, Nearly tight exponents for off-diagonal Ramsey numbers. arXiv:2605.28793 (2026). - [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. - [GrYa68] Graver, Jack E. and Yackel, James, Some graph theoretic results associated with Ramsey's theorem. J. Combinatorial Theory (1968), 125--175. - [MaVe23] Mattheus, S. and Verstraete, J., The asymptotics of \(r(4,t)\). arXiv:2306.04007 (2023).
Quoted from FormalConjectures/ErdosProblems/920.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/920.
The file states 5 research or textbook statements: 5 solved.
Erdos920.erdos_920
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos920.lean#L76.
Is it true that, for \(k\geq 4\), \(f_k(n) \gg \frac{n^{1-\frac{1}{k-1}}}{(\log n)^{c_k}}\) for some constant \(c_k>0\)?
This problem follows immediately from Mattheus and Verstraete's lower bound [MaVe23] for k = 4 and Bradač's lower bound [Br26] for k ≥ 5.
theorem erdos_920 :
∀ k : ℕ, k ≥ 4 → ∃ c > 0,
(fun n ↦ f k n) ≫ (fun n ↦ (n : ℝ) ^ (1 - 1 / ((k : ℝ) - 1)) / (log n) ^ c)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/920.lean, line 60.
Erdos920.erdos_920.variants.upper_bound
Solved: stated here without proof.
Graver and Yackel [GrYa68] proved that \(f_k(n) \ll \left(n\frac{\log\log n}{\log n}\right)^{1-\frac{1}{k-1}}.\)
theorem erdos_920.variants.upper_bound (k : ℕ) (hk : k ≥ 3) :
(fun n ↦ f k n) ≪ (fun n ↦ ((n : ℝ) * log (log n) / log n) ^ (1 - 1 / ((k : ℝ) - 1)))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/920.lean, line 70.
Erdos920.erdos_920.variants.k_eq_3
Solved: stated here without proof.
It is known that \(f_3(n)\asymp (n/\log n)^{1/2}\) (see [erdosproblems.com/1104]).
theorem erdos_920.variants.k_eq_3 :
(fun n ↦ (f 3 n : ℝ)) =Θ[atTop] (fun n ↦ ((n : ℝ) / log n) ^ (1 / 2 : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/920.lean, line 78.
Erdos920.erdos_920.variants.lower_bound_k_eq_4
Solved: stated here without proof.
The lower bound \(R(4,m) \gg m^3/(\log m)^4\) of Mattheus and Verstraete [MaVe23] (see [erdosproblems.com/166]) implies \(f_4(n) \gg \frac{n^{2/3}}{(\log n)^{4/3}}\).
theorem erdos_920.variants.lower_bound_k_eq_4 :
(fun n ↦ f 4 n) ≫ (fun n ↦ (n : ℝ) ^ (2 / 3 : ℝ) / (log n) ^ (4 / 3 : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/920.lean, line 87.
Erdos920.erdos_920.variants.lower_bound_k_ge_5
Solved: stated here without proof.
A positive answer to this question for all \(k\geq 5\), i.e. \(f_k(n) \gg \frac{n^{1-\frac{1}{k-1}}}{(\log n)^{c_k}}\) for some constant \(c_k>0\), follows from the lower bound in [erdosproblems.com/986] given by Bradač [Br26].
theorem erdos_920.variants.lower_bound_k_ge_5 (k : ℕ) (hk : k ≥ 5) :
∃ c > 0, (fun n ↦ f k n) ≫ (fun (n : ℕ) ↦
(n : ℝ) ^ (1 - 1 / ((k : ℝ) - 1)) / (log n) ^ c)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/920.lean, line 97.
Sources
TheoremErdős Problem 921#
References: - erdosproblems.com/921 - [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. - [Ga63] Gallai, T., Kritische Graphen. I. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1963), 165-192. - [KST84] Kierstead, H. A., Szemerédi, E. and Trotter, W. T., On coloring graphs with locally small chromatic number. Combinatorica (1984), 183-185.
Quoted from FormalConjectures/ErdosProblems/921.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/921.
The file states 1 research or textbook statement: 1 solved.
Erdos921.erdos_921
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos921.lean#L39.
Let \(k\geq 4\) and let \(f_k(n)\) be the largest \(m\) such that there is a graph on \(n\) vertices with chromatic number \(k\) in which every odd cycle has length \(> m\). Then
\[f_k(n) \asymp n^{\frac{1}{k-2}}.\]A question of Erdős and Gallai.
Proved for all \(k\geq 4\) by Kierstead, Szemerédi, and Trotter [KST84].
The linked formal proof (Codex and GPT-5.6 Sol) states this as
f k n = Θ(n ^ (1 / (k - 2))), wheref k nis the largestmsuch that some graph onnvertices with chromatic numberkhas no odd cycle of length at mostm; the two eventual statements below are the two halves of this estimate.
theorem erdos_921 :
∀ (k : ℕ), 4 ≤ k →
∃ (c₁ c₂ : ℝ), 0 < c₁ ∧ 0 < c₂ ∧
(∀ᶠ (n : ℕ) in atTop,
(∃ (G : SimpleGraph (Fin n)),
G.chromaticNumber = (k : ℕ∞) ∧
∀ l ∈ G.oddCycleLengths, c₁ * (n : ℝ) ^ (1 / ((k : ℝ) - 2)) < (l : ℝ))) ∧
(∀ᶠ (n : ℕ) in atTop,
∀ (G : SimpleGraph (Fin n)),
G.chromaticNumber = (k : ℕ∞) →
∃ l ∈ G.oddCycleLengths, (l : ℝ) ≤ c₂ * (n : ℝ) ^ (1 / ((k : ℝ) - 2)))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/921.lean, line 56.
Sources
TheoremErdős Problem 922#
References: - erdosproblems.com/922 - [ErHa67b] Erdős, P. and Hajnal, András, On chromatic graphs. Mat. Lapok (1967), 1-4. - [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. - [Fo70b] Folkman, J. H., An upper bound on the chromatic number of a graph. (1970), 437-457.
Quoted from FormalConjectures/ErdosProblems/922.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/922.
The file states 1 research or textbook statement: 1 solved.
Erdos922.erdos_922
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos922.lean#L5595.
Let \(k\geq 0\). Let \(G\) be a graph such that every subgraph \(H\) contains an independent set of size \(\geq (n-k)/2\), where \(n\) is the number of vertices of \(H\). Must \(G\) have chromatic number at most \(k+2\)?
A question of Erdős and Hajnal [ErHa67b]. The case \(k=0\) is trivial, but they could not prove this even for \(k=1\).
This is true, and was proved by Folkman [Fo70b].
See also 73.
theorem erdos_922 : ∀ (k : ℕ) (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) →
G.chromaticNumber ≤ k + 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/922.lean, line 52.
Sources
TheoremErdős Problem 923#
References: - erdosproblems.com/923 - [Er69b] Erdős, P., Problems and results in chromatic graph theory. Proof Techniques in Graph Theory (1969), 27-35. - [Ro77] Rödl, V., On the chromatic number of subgraphs of a given graph. Proc. Amer. Math. Soc. (1977), 370-371.
Quoted from FormalConjectures/ErdosProblems/923.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/923.
The file states 1 research or textbook statement: 1 solved.
Erdos923.erdos_923
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos923.lean.
Is it true that, for every \(k\), there is some \(f(k)\) such that if \(G\) has chromatic number \(\geq f(k)\) then \(G\) contains a triangle-free subgraph with chromatic number \(\geq k\)?
This is true, as shown by Rödl [Ro77].
theorem erdos_923 : ∀ (V : Type*) (n : ℕ),
∃ k : ℕ, ∀ G : SimpleGraph V, k ≤ G.chromaticNumber →
∃ H ≤ G, n ≤ H.chromaticNumber ∧ H.CliqueFree 3
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/923.lean, line 43.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.