Erdős Problem 1000 to Erdős Problem 1026
TheoremErdős Problem 1000#
References: - erdosproblems.com/1000 - [Ca50b] Cassels, J. W. S., Some metrical theorems in Diophantine approximation. I. Proc. Cambridge Philos. Soc. (1950), 209-218. - [Er64b] Erdős, P., Problems and results on diophantine approximations. Compositio Math. (1964), 52-65. - [Ha] Haight, J. A., Metric Diophantine approximation and related topics. PhD thesis.
Quoted from FormalConjectures/ErdosProblems/1000.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/1000.
The file states 5 research or textbook statements: 5 solved.
Erdos1000.erdos_1000
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1000.lean.
Let \(A=\{n_1\lt n_2\lt \cdots\}\) be an infinite sequence of positive integers, and let \(\phi_A(k)\) count the number of \(1\leq m\leq n_k\) such that the fraction \(\frac{m}{n_k}\) cannot be written as \(\frac{b}{n_j}\) for any integer \(b\) and any \(j\lt k\); equivalently,
\[ \frac{n_k}{(m,n_k)}\nmid n_j \]for all \(1\leq j\lt k\).
Is there a sequence \(A\) such that
\[ \lim_{N\to \infty}\frac{1}{N}\sum_{k\leq N}\frac{\phi_A(k)}{n_k}=0? \]This was solved by Haight [Ha] who proved that such a sequence does exist (contrary to Erdős' expectations).
theorem erdos_1000 :
∃ n : ℕ → ℕ, StrictMono n ∧ 0 < n 0 ∧
Tendsto (phiAvg n) atTop (𝓝 0)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1000.lean, line 75.
Erdos1000.erdos_1000.variants.totient_le
Proved here.
It is trivial that \(\phi_A(k)\geq \phi(n_k)\), where \(\phi\) is the Euler totient function.
theorem erdos_1000.variants.totient_le (n : ℕ → ℕ) (hn : StrictMono n) (hn0 : 0 < n 0)
(k : ℕ) :
(n k).totient ≤ phiSeq n k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1000.lean, line 84.
Erdos1000.erdos_1000.variants.liminf_eq_zero
Solved: stated here without proof.
The study of \(\phi_A\) was introduced by Cassels [Ca50b], who proved that there exist sequences such that
\[ \liminf_{N\to \infty}\frac{1}{N}\sum_{k\leq N}\frac{\phi_A(k)}{n_k}=0. \]
theorem erdos_1000.variants.liminf_eq_zero :
∃ n : ℕ → ℕ, StrictMono n ∧ 0 < n 0 ∧
atTop.liminf (phiAvg n) = 0
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1000.lean, line 131.
Erdos1000.erdos_1000.variants.not_tendsto_zero
Solved: stated here without proof.
Erdős [Er64b] proved that the limit of \(\frac{\phi_A(k)}{n_k}\) as \(k\to \infty\) cannot be \(0\).
theorem erdos_1000.variants.not_tendsto_zero (n : ℕ → ℕ) (hn : StrictMono n) (hn0 : 0 < n 0) :
¬ Tendsto (fun k : ℕ => (phiSeq n k : ℝ) / (n k : ℝ)) atTop (𝓝 0)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1000.lean, line 140.
Erdos1000.erdos_1000.variants.limsup_eq_one
Solved: stated here without proof.
In fact he proved that if \(\liminf \frac{\phi_A(k)}{n_k}=0\) then \(\limsup \frac{\phi_A(k)}{n_k}=1\).
theorem erdos_1000.variants.limsup_eq_one (n : ℕ → ℕ) (hn : StrictMono n) (hn0 : 0 < n 0)
(h : atTop.liminf (fun k : ℕ => (phiSeq n k : ℝ) / (n k : ℝ)) = 0) :
atTop.limsup (fun k : ℕ => (phiSeq n k : ℝ) / (n k : ℝ)) = 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1000.lean, line 149.
Sources
TheoremErdős Problem 1001#
References: - erdosproblems.com/1001 - [Er64b] Erdős, P., Problems and results on diophantine approximations. Compositio Math. 16 (1964), 52-65. PDF - [EST58] Erdős, P. and Szüsz, P. and Turán, P., Remarks on the theory of diophantine approximation. Colloq. Math. 6 (1958), 119-126. - [KeSo66] Kesten, H. and Sós, V. T., On two problems of Erdős, Szüsz and Turán concerning diophantine approximations. Acta Arith. 12 (1966/67), 183-192. - [XiZa06] Xiong, Maosheng and Zaharescu, Alexandru, A problem of Erdős-Szüsz-Turán on diophantine approximation. Acta Arith. 125 (2006), 163-177. - [Bo08] Boca, Florin P., A problem of Erdős, Szüsz and Turán concerning Diophantine approximations. Int. J. Number Theory 4 (2008), 691-708.
Quoted from FormalConjectures/ErdosProblems/1001.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/1001.
The file states 2 research or textbook statements: 2 solved.
Erdos1001.erdos_1001.parts.i
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1001.lean#L8077.
Let \(S(N,A,c)\) be the measure of the set of those \(\alpha\in (0,1)\) such that
\[\left\lvert \alpha-\frac{x}{y}\right\rvert< \frac{A}{y^2}\]for some \(N\leq y\leq cN\) and \((x,y)=1\). Does
\[\lim_{N\to \infty}S(N,A,c)=f(A,c)\]exist?
This is a problem of Erdős, Szüsz, and Turán [EST58], restated in [Er64b, p. 62]. The existence of the limit for all \(A>0\) and \(c\geq 1\) was proved by Kesten and Sós [KeSo66]. Boca [Bo08] and Xiong and Zaharescu [XiZa06, Theorem 2] gave further proofs. We assume \(A>0\) and \(c\geq 1\), since otherwise \(S=0\). The second question, the explicit form of \(f(A,c)\), is not stated here.
theorem erdos_1001.parts.i (A c : ℝ) (hA : 0 < A) (hc : 1 ≤ c) :
∃ f : ℝ, Tendsto (fun N : ℕ ↦ S N A c) atTop (𝓝 f)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1001.lean, line 76.
Erdos1001.erdos_1001.variants.est_formula
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1001.lean#L1047.
Erdős, Szüsz, and Turán [EST58] proved that
\[f(A,c)=\frac{12 A\log c}{\pi^2}\]when \(0\lt A< \frac{c}{1+c^2}\). Here \(c\geq 1\), since the range \(N\leq y\leq cN\) is empty for \(c<1\).
theorem erdos_1001.variants.est_formula (A c : ℝ) (hA : 0 < A) (hc : 1 ≤ c)
(hAc : A < c / (1 + c ^ 2)) :
Tendsto (fun N : ℕ ↦ S N A c) atTop (𝓝 (12 * A * Real.log c / Real.pi ^ 2))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1001.lean, line 89.
Sources
TheoremErdős Problem 1002#
References: - erdosproblems.com/1002 - [Ke60] Kesten, Harry, Uniform distribution {\({\rm mod}\,1\)}. Ann. of Math. (2) (1960), 445--471.
Quoted from FormalConjectures/ErdosProblems/1002.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/1002.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos1002.erdos_1002
Open: stated without proof.
For any \(0\lt \alpha<1\), let \(f(\alpha,n)=\frac{1}{\log n}\sum_{1\leq k\leq n}(\tfrac{1}{2}- \{ \alpha k\})\). Does \(f(\alpha,n)\) have an asymptotic distribution function?
In other words, is there a non-decreasing function \(g\) such that \(g(-\infty)=0\), \(g(\infty)=1\), and \(\lim_{n\to \infty}\lvert \{ \alpha\in (0,1): f(\alpha,n)\leq c\}\rvert=g(c)\)?
theorem erdos_1002 :
∃ g : ℝ → ℝ, Monotone g ∧
Tendsto g atBot (𝓝 0) ∧
Tendsto g atTop (𝓝 1) ∧
letI f := fun (α : ℝ) (n : ℕ) ↦
(1 / log n) * ∑ k ∈ Icc (1 : ℕ) n, (1 / 2 - Int.fract (α * k))
∀ c : ℝ, Tendsto (fun (n : ℕ) ↦ (volume { α | α ∈ Ioo (0 : ℝ) 1 ∧ f α n ≤ c }).toReal)
atTop (𝓝 (g c))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1002.lean, line 42.
Erdos1002.erdos_1002.variants.kesten
Solved: stated here without proof.
Kesten [Ke60] proved that if \(f(\alpha,\beta,n)=\frac{1}{\log n}\sum_{1\leq k\leq n}(\tfrac{1}{2}- \{\beta+\alpha k\})\) then \(f(\alpha,\beta,n)\) has asymptotic distribution function \(g(c)=\frac{1}{\pi}\int_{-\infty}^{\rho c}\frac{1}{1+t^2}\mathrm{d}t\), where \(\rho>0\) is an explicit constant.
theorem erdos_1002.variants.kesten :
∃ ρ > 0,
let g := fun (c : ℝ) ↦ (1 / π) * ∫ t in Iic (ρ * c), 1 / (1 + t^2)
∀ c : ℝ, Tendsto (fun (n : ℕ) ↦
(volume { p : ℝ × ℝ | let ⟨α, β⟩ := p; α ∈ Icc (0 : ℝ) 1 ∧ β ∈ Icc (0 : ℝ) 1 ∧
(1 / log n) * ∑ k ∈ Icc (1 : ℕ) n, (1 / 2 - Int.fract (β + α * k)) ≤ c }).toReal)
atTop (𝓝 (g c))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1002.lean, line 59.
Sources
TheoremErdős Problem 1003#
Reference: erdosproblems.com/1003
Quoted from FormalConjectures/ErdosProblems/1003.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/1003.
The file states 3 research or textbook statements: 2 open and 1 solved.
Erdos1003.erdos_1003
Open: stated without proof.
Are there infinitely many solutions to \(\phi(n) = \phi(n+1)\), where \(\phi\) is the Euler totient function?
theorem erdos_1003 : Set.Infinite {n | φ n = φ (n + 1)}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1003.lean, line 38.
Erdos1003.erdos_1003.variants.Icc
Open: stated without proof.
Erdős [Er85e] says that, presumably, for every \(k \geq 1\) the equation
\[\phi(n) = \phi(n+1) = \cdots = \phi (n+k)\]has infinitely many solutions.
[Er85e] Erdős, P., Some problems and results in number theory. Number theory and combinatorics. Japan 1984 (Tokyo, Okayama and Kyoto, 1984) (1985), 65-87.
theorem erdos_1003.variants.Icc :
∀ k ≥ 1, {n | ∀ i ∈ Set.Icc 1 k, φ n = φ (n + i)}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1003.lean, line 48.
Erdos1003.erdos_1003.variants.eps87
Solved: stated here without proof.
Erdős, Pomerance, and Sárközy [EPS87] proved that for all large \(x\), the number of \(n \leq x\) with \(\phi(n) = \phi(n+1)\) is at most
\[\frac{x}{\exp((\log x)^{1/3})}\].
[EPS87] Erd\H os, Paul and Pomerance, Carl and S\'ark\"ozy, Andr\'as, On locally repeated values of certain arithmetic functions. {II}. Proc. Amer. Math. Soc. (1987), 1--7.
theorem erdos_1003.variants.eps87 : ∀ᶠ x in atTop,
{(n : ℕ) | (n ≤ x) ∧ φ n = φ (n + 1)}.ncard ≤
x / Real.exp ((x.log) ^ ((1 : ℝ) / 3))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1003.lean, line 59.
Sources
TheoremErdős Problem 1004#
Reference: erdosproblems.com/1004
Quoted from FormalConjectures/ErdosProblems/1004.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/1004.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos1004.erdos_1004
Open: stated without proof.
For any fixed c > 0, if x is sufficiently large then there exists n ≤ x such that the values of φ(n+k) are all distinct for 1 ≤ k ≤ (log x)^c. This is an open problem.
theorem erdos_1004 :
∀ c > (0 : ℝ), ∀ᶠ x in atTop, ∃ n ≤ x,
IsDistinctTotientRun n ⌊(Real.log (x : ℝ)) ^ c⌋₊
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1004.lean, line 42.
Erdos1004.erdos_1004.variants.le_of_isDistinctTotientRun
Solved: stated here without proof.
Erdős, Pomerance, and Sárközy [EPS87] proved that if φ(n+k) are all distinct for 1 ≤ k ≤ K then K ≤ n / exp(c (log n)^{1/3}) for some constant c > 0. Here we state the existence of such a constant c.
theorem erdos_1004.variants.le_of_isDistinctTotientRun :
∃ (c : ℝ) (hc : c > 0),
∀ᶠ n in atTop, ∀ (K : ℕ), IsDistinctTotientRun n K →
(K : ℝ) ≤ (n : ℝ) / Real.exp (c * (Real.log n) ^ (1/3 : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1004.lean, line 53.
Sources
TheoremErdős Problem 1005#
References: - erdosproblems.com/1005 - [Ma42] Mayer, A. E., A mean value theorem concerning Farey series. Quart. J. Math. Oxford Ser. (1942), 48-57. - [Er43] Erdős, P., A note on Farey series. Quart. J. Math. Oxford Ser. (1943), 82-85. - [vD25b] van Doorn, W., Improved bounds for the Mayer-Erdős phenomenon on similarly ordered Farey fractions. arXiv:2509.00121 (2025).
Quoted from FormalConjectures/ErdosProblems/1005.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/1005.
The file states 2 research or textbook statements: 2 solved.
Erdos1005.erdos_1005
Solved: stated here without proof.
Let \(\frac{a_1}{b_1}, \frac{a_2}{b_2}, \ldots\) be the Farey fractions of order \(n \geq 4\). Let \(f(n)\) be the largest integer such that if \(1 \leq k < l \leq k + f(n)\) then \(\frac{a_k}{b_k}\) and \(\frac{a_l}{b_l}\) are similarly ordered, in other words \((a_k - a_l)(b_k - b_l) \geq 0\). Estimate \(f(n)\): in particular, is there a constant \(c > 0\) such that \(f(n) = (c + o(1)) n\) for all large \(n\)?
Mayer [Ma42] proved that \(f(n) \to \infty\) and Erdős [Er43] that \(f(n) \gg n\). Van Doorn [vD25b] proved \((1/12 - o(1)) n \le f(n) \le n / 4 + O(1)\) and conjectured that \(f(n) = (1/4 + o(1)) n\), which was proved by Cipollini and GPT-5.5; see
erdos_1005.variants.constant.
theorem erdos_1005 :
∃ c : ℝ, 0 < c ∧ Tendsto (fun n : ℕ => (f n : ℝ) / n) atTop (𝓝 c)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1005.lean, line 70.
Erdos1005.erdos_1005.variants.constant
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1005.lean#L44.
The constant in Problem 1005 is \(c = 1/4\): \(f(n) = (1/4 + o(1)) n\) (Cipollini and GPT-5.5; formalised by Cipollini, van Doorn and Aristotle).
theorem erdos_1005.variants.constant :
Tendsto (fun n : ℕ => (f n : ℝ) / n) atTop (𝓝 (1 / 4))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1005.lean, line 79.
Sources
TheoremErdős Problem 1007#
References: - erdosproblems.com/1007 - [ChNo16] Chaffee, Joe and Noble, Matt, Dimension 4 and dimension 5 graphs with minimum edge set. Australas. J. Combin. (2016), 327-333. - [Ho13] House, Roger F., A 4-dimensional graph has at least 9 edges. Discrete Math. (2013), 1783-1789.
Quoted from FormalConjectures/ErdosProblems/1007.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/1007.
The file states 4 research or textbook statements: 4 solved.
Erdos1007.erdos_1007
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1007.lean.
The dimension of a graph \(G\) is the minimal \(n\) such that \(G\) can be embedded in \(\mathbb{R}^n\) such that every edge of \(G\) is a unit line segment.
What is the smallest number of edges in a graph with dimension \(4\)?
Answer: The smallest number of edges is \(9\), achieved solely by \(K_{3,3}\), proved by House [Ho13]. An alternative proof was given by Chaffee and Noble [ChNo16], who also prove that the smallest number of edges in a graph of dimension \(5\) is \(15\) (achieved by \(K_6\) and \(K_{1,3,3}\)).
theorem erdos_1007 :
IsLeast {m | ∃ (n : ℕ) (G : SimpleGraph (Fin n)), G.HasDimension 4 ∧ G.edgeSet.ncard = m}
9
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1007.lean, line 54.
Erdos1007.erdos_1007.variants.dimension_four_extremal
Solved: stated here; a Lean proof is at https://github.com/Dishah3241/Erdos1007/blob/43f89415a6663848a1445effbda8b3abe77b052b/Erdos1007/Standalone/Mathlib/InlineErdos1007Proof.lean#L306.
The smallest number of edges in a graph of dimension \(4\) is achieved solely by \(K_{3,3}\).
theorem erdos_1007.variants.dimension_four_extremal (n : ℕ) (G : SimpleGraph (Fin n))
(hdim : G.HasDimension 4) (hcard : G.edgeSet.ncard = 9)
(hdeg : ∀ v : Fin n, ∃ w : Fin n, G.Adj v w) :
Nonempty (G ≃g completeBipartiteGraph (Fin 3) (Fin 3))
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1007.lean, line 66.
Erdos1007.erdos_1007.variants.dimension_five
Solved: stated here; a Lean proof is at https://github.com/Dishah3241/Erdos1007Dim5/blob/7118d68eabffe49e41a672d16eb8ddba2608f03d/Erdos1007Dim5/Standalone/Mathlib/InlineErdos1007Dim5Proof.lean#L145.
The smallest number of edges in a graph of dimension \(5\) is \(15\).
theorem erdos_1007.variants.dimension_five :
IsLeast {m | ∃ (n : ℕ) (G : SimpleGraph (Fin n)), G.HasDimension 5 ∧ G.edgeSet.ncard = m}
15
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1007.lean, line 79.
Erdos1007.erdos_1007.variants.dimension_five_extremal
Solved: stated here; a Lean proof is at https://github.com/Dishah3241/Erdos1007Dim5/blob/7118d68eabffe49e41a672d16eb8ddba2608f03d/Erdos1007Dim5/Standalone/Mathlib/InlineErdos1007Dim5Proof.lean#L161.
The smallest number of edges in a graph of dimension \(5\) is achieved by \(K_6\) and \(K_{1,3,3}\).
theorem erdos_1007.variants.dimension_five_extremal :
((SimpleGraph.completeGraph (Fin 6)).HasDimension 5 ∧
(SimpleGraph.completeGraph (Fin 6)).edgeSet.ncard = 15) ∧
(K133.HasDimension 5 ∧ K133.edgeSet.ncard = 15)
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1007.lean, line 91.
Sources
TheoremErdős Problem 1008#
References: - erdosproblems.com/1008 - [CFS14b] Conlon, D. and Fox, J. and Sudakov, B., Large subgraphs without complete bipartite graphs. arXiv:1401.6711 (2014). - [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.
Quoted from FormalConjectures/ErdosProblems/1008.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/1008.
The file states 4 research or textbook statements: 4 solved.
Erdos1008.erdos_1008
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1008.lean.
Does every graph with \(m\) edges contain a subgraph with \(\gg m^{2/3}\) edges which contains no \(C_4\)?
This problem was first solved in the affirmative by Conlon, Fox, and Sudakov [CFS14b]. A simple proof is given by Hunter in the comments.
theorem erdos_1008 :
∃ c > (0 : ℝ), ∀ (V : Type) [Fintype V] (G : SimpleGraph V),
∃ H ≤ G, (cycleGraph 4).Free H ∧
c * (G.edgeSet.ncard : ℝ) ^ (2 / 3 : ℝ) ≤ (H.edgeSet.ncard : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1008.lean, line 46.
Erdos1008.erdos_1008.variants.three_quarters
Solved: stated here without proof.
Originally asked by Bollobás and Erdős in 'a colloquium on graph theory at Tihany' with \(m^{2/3}\) replaced by \(m^{3/4}\). Folkman showed this is false with the counterexample \(K_{n,n^2}\), which has \(n^3\) edges, and yet every subgraph with \(>n^2+\binom{n}{2}\) edges contains a \(C_4\).
theorem erdos_1008.variants.three_quarters :
¬ ∃ c > (0 : ℝ), ∀ (V : Type) [Fintype V] (G : SimpleGraph V),
∃ H ≤ G, (cycleGraph 4).Free H ∧
c * (G.edgeSet.ncard : ℝ) ^ (3 / 4 : ℝ) ≤ (H.edgeSet.ncard : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1008.lean, line 58.
Erdos1008.erdos_1008.variants.folkman
Solved: stated here without proof.
Folkman's counterexample \(K_{n,n^2}\), which has \(n^3\) edges, and yet every subgraph with \(>n^2+\binom{n}{2}\) edges contains a \(C_4\).
theorem erdos_1008.variants.folkman (n : ℕ) :
((completeBipartiteGraph (Fin n) (Fin (n ^ 2))).edgeSet.ncard = n ^ 3) ∧
∀ H ≤ completeBipartiteGraph (Fin n) (Fin (n ^ 2)),
n ^ 2 + n.choose 2 < H.edgeSet.ncard → cycleGraph 4 ⊑ H
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1008.lean, line 69.
Erdos1008.erdos_1008.variants.lower_bound
Solved: stated here without proof.
In [Er71] Erdős revises the conjecture to \(m^{2/3}\), and notes \(\gg m^{1/2}\) is trivial.
theorem erdos_1008.variants.lower_bound :
∃ c > (0 : ℝ), ∀ (V : Type) [Fintype V] (G : SimpleGraph V),
∃ H ≤ G, (cycleGraph 4).Free H ∧
c * (G.edgeSet.ncard : ℝ) ^ (1 / 2 : ℝ) ≤ (H.edgeSet.ncard : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1008.lean, line 79.
Sources
TheoremErdős Problem 1009#
References: - erdosproblems.com/1009 - [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. - [Gy88] Győri, E., On the number of edge-disjoint triangles in graphs of given size. (1988), 267--276.
Quoted from FormalConjectures/ErdosProblems/1009.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/1009.
The file states 2 research or textbook statements: 2 solved.
Erdos1009.erdos_1009
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1009.lean#L2347.
Is it true that, for every \(c>0\), there exists \(f(c)\) such that every graph on \(n\) vertices with at least \(\lfloor n^2/4\rfloor+k\) edges, where \(k\lt c n\), contains at least \(k-f(c)\) many edge disjoint triangles?
Erdős [Er71] proved this for \(c<1/2\) using a theorem of Erdős and Gallai, which says that every graph on \(n\) vertices with at least \((n-1)^2/4+2\) many edges, with chromatic number \(3\), must contain a triangle. In fact, Erdős proved this is true with \(f(c)=0\) for \(c<1/2\). At first Erdős thought \(f(c)=0\) for larger values of \(c\) but this is false: an example of Sauer proves that \(f(2)\geq 1\).
This is true, and was proved by Győri [Gy88] who proved that this is true with \(f(c)\ll c^2\), and also that \(f(c)=0\) if \(c<2\) for odd \(n\) or \(c<3/2\) for even \(n\).
A family of edge disjoint triangles is a finite set of \(3\)-cliques of \(G\) any two of which share at most one vertex.
theorem erdos_1009 : ∀ c : ℝ, 0 < c → ∃ f : ℕ, ∀ (n k : ℕ) (G : SimpleGraph (Fin n)),
n ^ 2 / 4 + k ≤ G.edgeSet.ncard → (k : ℝ) < c * n →
∃ T : Finset (Finset (Fin n)), (∀ t ∈ T, G.IsNClique 3 t) ∧
(T : Set (Finset (Fin n))).Pairwise (fun s t => (s ∩ t).card ≤ 1) ∧ k ≤ T.card + f
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1009.lean, line 55.
Erdos1009.erdos_1009.variants.sauer
Solved: stated here without proof.
Sauer gave an example of a graph on \(n\) vertices with \(\lfloor n^2/4\rfloor+2n-6\) many edges which contains only \(2n-7\) many edge disjoint triangles: if \(n=2r+4\) then \(G\) is the complete tripartite graph on \([r]\times [r]\times [4]\), with a \(K_4\) on the \([4]\) vertices also.
theorem erdos_1009.variants.sauer : ∀ r : ℕ, 1 ≤ r → ∃ G : SimpleGraph (Fin (2 * r + 4)),
G.edgeSet.ncard = (2 * r + 4) ^ 2 / 4 + 2 * (2 * r + 4) - 6 ∧
∀ T : Finset (Finset (Fin (2 * r + 4))), (∀ t ∈ T, G.IsNClique 3 t) →
(T : Set (Finset (Fin (2 * r + 4)))).Pairwise (fun s t => (s ∩ t).card ≤ 1) →
T.card ≤ 2 * (2 * r + 4) - 7
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1009.lean, line 67.
Sources
TheoremErdős Problem 1010#
References: - erdosproblems.com/1010 - [Er62d] Erdős, P., On a theorem of Rademacher-Turán. Illinois J. Math. (1962), 122-127. - [LoSi76] Lovász, L. and Simonovits, Miklós, On the number of complete subgraphs of a graph. (1976), 431-441. - [NiKh81] Nikiforov, V. S. and Khadzhiivanov, N. G., Solution of the problem of P. Erdős on the number of triangles in graphs with \(n\) vertices and \([n^2/4]+l\) edges. C. R. Acad. Bulgare Sci. (1981), 969-970.
Quoted from FormalConjectures/ErdosProblems/1010.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/1010.
The file states 3 research or textbook statements: 3 solved.
Erdos1010.erdos_1010
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1010.lean#L612.
Let \(t\lt \lfloor n/2\rfloor\). Does every graph on \(n\) vertices with \(\lfloor n^2/4\rfloor+t\) edges contain at least \(t\lfloor n/2\rfloor\) triangles?
Rademacher proved that every graph on \(n\) vertices with \(\lfloor n^2/4\rfloor+1\) edges contains at least \(\lfloor n/2\rfloor\) triangles. Erdős [Er62d] proved that every graph on \(n\) vertices with \(\lfloor n^2/4\rfloor+t\) edges contains at least \(t\lfloor n/2\rfloor\) triangles, for all \(t\lt cn\), for some constant \(c>0\).
This is true, and was proved independently by Lovász and Simonovits [LoSi76] and Nikiforov and Khadzhiivanov [NiKh81].
theorem erdos_1010 : ∀ n t : ℕ, t < n / 2 → ∀ G : SimpleGraph (Fin n),
G.edgeFinset.card = n ^ 2 / 4 + t → t * (n / 2) ≤ (G.cliqueFinset 3).card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1010.lean, line 55.
Erdos1010.erdos_1010.variants.rademacher
Solved: stated here without proof.
Rademacher proved that every graph on \(n\) vertices with \(\lfloor n^2/4\rfloor+1\) edges contains at least \(\lfloor n/2\rfloor\) triangles.
theorem erdos_1010.variants.rademacher : ∀ n : ℕ, ∀ G : SimpleGraph (Fin n),
G.edgeFinset.card = n ^ 2 / 4 + 1 → n / 2 ≤ (G.cliqueFinset 3).card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1010.lean, line 65.
Erdos1010.erdos_1010.variants.erdos
Solved: stated here without proof.
Erdős [Er62d] proved that every graph on \(n\) vertices with \(\lfloor n^2/4\rfloor+t\) edges contains at least \(t\lfloor n/2\rfloor\) triangles, for all \(t\lt cn\), for some constant \(c>0\).
theorem erdos_1010.variants.erdos : ∃ c : ℝ, 0 < c ∧ ∀ n t : ℕ, t < c * n →
∀ G : SimpleGraph (Fin n), G.edgeFinset.card = n ^ 2 / 4 + t →
t * (n / 2) ≤ (G.cliqueFinset 3).card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1010.lean, line 75.
Sources
TheoremErdős Problem 1013#
References: - erdosproblems.com/1013 - [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. - [GrYa68] Graver, J. E. and Yackel, J., Some graph theoretic results associated with Ramsey's theorem. J. Combinatorial Theory 4 (1968), 125-175. - [DaIl22] Davies, E. and Illingworth, F., The \(\chi\)-Ramsey problem for triangle-free graphs. SIAM J. Discrete Math. 36 (2022), 1124-1134. - [HHKP25] Hefty, Z., Horn, P., King, D. and Pfender, F., Improving \(R(3,k)\) in just two bites. arXiv:2510.19718 (2025).
Quoted from FormalConjectures/ErdosProblems/1013.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/1013.
The file states 5 research or textbook statements: 2 open and 3 solved. It also has 1 test statement and 1 API statement, counted here but not shown.
Erdos1013.erdos_1013.parts.i
Open: stated without proof.
Let \(h_3(k)\) be the minimal \(n\) such that there exists a triangle-free graph on \(n\) vertices with chromatic number \(k\). Find an asymptotic for \(h_3(k)\), and also prove
\[\lim_{k\to \infty}\frac{h_3(k+1)}{h_3(k)}=1.\]This is the first part.
theorem erdos_1013.parts.i :
(fun k ↦ (h3 k : ℝ)) ~[atTop] erdos_1013.parts.i.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1013.lean, line 69.
Erdos1013.erdos_1013.parts.ii
Open: stated without proof.
Let \(h_3(k)\) be the minimal \(n\) such that there exists a triangle-free graph on \(n\) vertices with chromatic number \(k\). Find an asymptotic for \(h_3(k)\), and also prove
\[\lim_{k\to \infty}\frac{h_3(k+1)}{h_3(k)}=1.\]This is the second part.
theorem erdos_1013.parts.ii :
Tendsto (fun k : ℕ ↦ (h3 (k + 1) : ℝ) / h3 k) atTop (nhds 1)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1013.lean, line 81.
Erdos1013.erdos_1013.variants.graver_yackel
Solved: stated here without proof.
Graver and Yackel [GrYa68] proved
\[h_3(k)\gg \frac{\log k}{\log\log k}k^2.\]
theorem erdos_1013.variants.graver_yackel :
∃ c > (0 : ℝ), ∀ᶠ k : ℕ in atTop,
c * (Real.log k / Real.log (Real.log k)) * k ^ 2 ≤ (h3 k : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1013.lean, line 90.
Erdos1013.erdos_1013.variants.lower
Solved: stated here without proof.
The upper bound \(f(n) \leq (2+o(1))(n/\log n)^{1/2}\) of Davies and Illingworth [DaIl22] for the function \(f\) of [1104] gives
\[\left(\frac{1}{2}-o(1)\right)k^2\log k\leq h_3(k).\]
theorem erdos_1013.variants.lower :
∀ ε > (0 : ℝ), ∀ᶠ k : ℕ in atTop,
(1 / 2 - ε) * k ^ 2 * Real.log k ≤ (h3 k : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1013.lean, line 101.
Erdos1013.erdos_1013.variants.upper
Solved: stated here without proof.
The lower bound \(f(n) \geq (1-o(1))(n/\log n)^{1/2}\) for the function \(f\) of [1104], which follows from the construction of Hefty, Horn, King, and Pfender [HHKP25], gives
\[h_3(k) \leq (2+o(1))k^2\log k.\]The site states \((1+o(1))k^2\log k\), but the bounds recorded in [1104] give only \(2+o(1)\).
theorem erdos_1013.variants.upper :
∀ ε > (0 : ℝ), ∀ᶠ k : ℕ in atTop,
(h3 k : ℝ) ≤ (2 + ε) * k ^ 2 * Real.log k
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1013.lean, line 113.
Sources
TheoremErdős Problem 1014#
References: - erdosproblems.com/1014 - [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. - [OpenAI26] On the ratio of \(R(k,\ell)\) and \(R(k,\ell+1)\), proof due to an internal model at OpenAI (2026). https://cdn.openai.com/pdf/6dc7175d-d9e7-4b8d-96b8-48fe5798cd5b/Ramsey.pdf
Quoted from FormalConjectures/ErdosProblems/1014.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/1014.
The file states 2 research or textbook statements: 2 solved.
Erdos1014.erdos_1014
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1014.lean.
Let \(R(k,l)\) be the Ramsey number, so the minimal \(n\) such that every graph on at least \(n\) vertices contains either a \(K_k\) or an independent set on \(l\) vertices.
Prove, for fixed \(k\geq 3\), that
\[\lim_{l\to \infty}\frac{R(k,l+1)}{R(k,l)}=1.\]This has been solved by an internal model at OpenAI.
theorem erdos_1014 : ∀ k : ℕ, 3 ≤ k →
Tendsto (fun l : ℕ ↦ (R(k, l + 1) : ℝ) / (R(k, l) : ℝ)) atTop (𝓝 1)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1014.lean, line 55.
Erdos1014.erdos_1014.variants.upper_bound
Solved: stated here without proof.
That proof in fact shows that
\[R(k,l+1)\leq (1+O(l^{-c/k^2}))R(k,l)\]for some constant \(c>0\).
theorem erdos_1014.variants.upper_bound :
∃ c : ℝ, 0 < c ∧ ∀ k : ℕ, 3 ≤ k → ∃ C : ℝ, ∀ᶠ l : ℕ in atTop,
(R(k, l + 1) : ℝ) ≤ (1 + C * (l : ℝ) ^ (-c / (k : ℝ) ^ 2)) * (R(k, l) : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1014.lean, line 65.
Sources
TheoremErdős Problem 1017#
References: - erdosproblems.com/1017 - [EGP66] Erdős, Paul and Goodman, A. W. and Pósa, Lajos, The representation of a graph by set intersections. Canadian J. Math. (1966), 106–112. - [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. - [GyKe17] Győri, Ervin and Keszegh, Balázs, On the number of edge-disjoint triangles in \(K_4\)-free graphs. Combinatorica (2017), 1113–1124. - [Lo68] Lovász, L., On covering of graphs. Theory of Graphs (Proc. Colloq., Tihany, 1966) (1968), 231–236.
Quoted from FormalConjectures/ErdosProblems/1017.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/1017.
The file states 2 research or textbook statements: 2 open. It also has 2 test statements and 3 API statements, counted here but not shown.
Erdos1017.erdos_1017.lower_bound
Open: stated without proof.
Let \(f(n,k)\) be such that every graph on \(n\) vertices and \(k\) edges can be partitioned into at most \(f(n,k)\) edge-disjoint complete graphs. Estimate \(f(n,k)\) for \(k>n^2/4\).
theorem erdos_1017.lower_bound :
∀ n k : ℕ, k ≤ n.choose 2 → n * n < 4 * k →
erdos_1017.lower_bound.answer n k ≤ f n k
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1017.lean, line 108.
Erdos1017.erdos_1017.upper_bound
Open: stated without proof.
Estimate an upper bound for \(f(n,k)\), the worst-case number of complete subgraphs needed to partition the edges of an \(n\)-vertex, \(k\)-edge graph, for \(n^2/4 < k \le \binom{n}{2}\).
theorem erdos_1017.upper_bound :
∀ n k : ℕ, k ≤ n.choose 2 → n * n < 4 * k →
f n k ≤ erdos_1017.upper_bound.answer n k
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1017.lean, line 119.
Sources
TheoremErdős Problem 1020#
References: - erdosproblems.com/1020 - [BDE76] Bollobás, B. and Daykin, D. E. and Erdős, P., Sets of independent edges of a hypergraph. Quart. J. Math. Oxford Ser. (2) (1976), 25--32. - [Er65d] Erdős, P., A problem on independent {\(r\)}-tuples. Ann. Univ. Sci. Budapest. Eötvös Sect. Math. (1965), 93--95. - [ErGa59] Erdős, P. and Gallai, T., On maximal paths and circuits of graphs. Acta Math. Acad. Sci. Hungar. (1959), 337-356 (unbound insert). - [FLM12] Frankl, Peter and Łuczak, Tomasz and Mieczkowska, Katarzyna, On matchings in hypergraphs. Electron. J. Combin. (2012), Paper 42, 5. - [FRR12] Frankl, Peter and Rödl, Vojtech and Ruciński, Andrzej, On the maximum number of edges in a triple system not containing a disjoint family of a given size. Combin. Probab. Comput. (2012), 141--148. - [Fr17] Frankl, Peter, Proof of the {E}rdős matching conjecture in a new range. Israel J. Math. (2017), 421--430. - [Fr87] Frankl, Peter, The shifting technique in extremal set theory. (1987), 81--110. - [HLS12] Huang, Hao and Loh, Po-Shen and Sudakov, Benny, The size of a hypergraph and its matching number. Combin. Probab. Comput. (2012), 442--450. - [Kl68] Kleitman, Daniel J., Maximal number of subsets of a finite set no {\(k\)} of which are pairwise disjoint. J. Combinatorial Theory (1968), 157--163. - [KoKu23] Kolupaev, Dmitriy and Kupavskii, Andrey, Erdős matching conjecture for almost perfect matchings. Discrete Math. (2023), Paper No. 113304, 9. - [LuMi14] Łuczak, Tomasz and Mieczkowska, Katarzyna, On {E}rdős' extremal problem on matchings in hypergraphs. J. Combin. Theory Ser. A (2014), 178--194.
Quoted from FormalConjectures/ErdosProblems/1020.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/1020.
The file states 1 research or textbook statement: 1 open.
Erdos1020.erdos_1020
Open: stated without proof.
Let \(f(n;r,k)\) be the maximal number of edges in an \(r\)-uniform hypergraph which contains no set of \(k\) many independent edges.
For all \(r\geq 3\),
\[f(n;r,k)=\max\left(\binom{rk-1}{r}, \binom{n}{r}-\binom{n-k+1}{r}\right).\]Note: the source states the formula with no range on
nork, but some restriction is needed: e.g. forr = 3,k = 2,n = 4no two disjoint triples fit in4vertices, so the left-hand side is4.choose 3 = 4while the right-hand side is5.choose 3 = 10. We requirek ≥ 1andn ≥ r*k - 1: this is the smallestnaccommodating the construction counted by the first term (allr-subsets of a fixed(r*k - 1)-set), and atn = r*k - 1the equality holds trivially, since the completer-uniform hypergraph has nok-matching. The source's commentary likewise calls the casen < k*rtrivial.
theorem erdos_1020 (r : ℕ) (hr : 3 ≤ r) (n k : ℕ) (hk : 0 < k)
(hrk : r * k - 1 ≤ n) :
f n r k = max ((r * k - 1).choose r)
(n.choose r - (n - k + 1).choose r)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1020.lean, line 73.
Sources
TheoremErdős Problem 1021#
References: - erdosproblems.com/1021 - [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. - [Er74c] Erdős, Paul, Extremal problems on graphs and hypergraphs. (1974), 75-84. - [CoLe21] Conlon, David and Lee, Joonkyung, On the extremal number of subdivisions. Int. Math. Res. Not. IMRN (2021), 9122--9145. - [Ja19] Janzer, Oliver, Improved bounds for the extremal number of subdivisions. Electron. J. Combin. (2019), Paper No. 3.3, 6.
Quoted from FormalConjectures/ErdosProblems/1021.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/1021.
The file states 2 research or textbook statements: 2 solved.
Erdos1021.erdos_1021
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1021.lean#L2359.
Is it true that, for every \(k \geq 3\), there is a constant \(c_k > 0\) such that
\[\mathrm{ex}(n, G_k) \ll n^{3/2 - c_k},\]where \(G_k\) is the bipartite graph between \(\{y_1, \ldots, y_k\}\) and \(\{z_1, \ldots, z_{\binom{k}{2}}\}\), with each \(z_j\) joined to a unique pair of \(y_i\)?
A conjecture of Erdős and Simonovits [Er71, Er74c], who proved (in unpublished work) that one must have \(c_k \to 0\) as \(k \to \infty\). The graph \(G_k\) is the \(1\)-subdivision of \(K_k\); for \(k = 3\) it is the \(6\)-cycle. This was proved by Conlon and Lee [CoLe21] with \(c_k = 6^{-k}\), improved to \(c_k = \frac{1}{4k - 6}\) by Janzer [Ja19]; see
erdos_1021.variants.janzer.
theorem erdos_1021 :
∀ k : ℕ, 3 ≤ k → ∃ c : ℝ, 0 < c ∧
(fun n : ℕ ↦ (SimpleGraph.extremalNumber n (cliqueSubdivision k) : ℝ)) =O[atTop]
fun n : ℕ ↦ (n : ℝ) ^ (3 / 2 - c)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1021.lean, line 73.
Erdos1021.erdos_1021.variants.janzer
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1021.lean#L2336.
Janzer [Ja19] proved that one can take \(c_k = \frac{1}{4k - 6}\).
theorem erdos_1021.variants.janzer (k : ℕ) (hk : 3 ≤ k) :
(fun n : ℕ ↦ (SimpleGraph.extremalNumber n (cliqueSubdivision k) : ℝ)) =O[atTop]
fun n : ℕ ↦ (n : ℝ) ^ (3 / 2 - 1 / (4 * (k : ℝ) - 6))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1021.lean, line 83.
Sources
TheoremErdős Problem 1022#
References: - erdosproblems.com/1022 - [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. - [Lo68] Lovász, L., On covering of graphs. Theory of Graphs (Proc. Colloq., Tihany, 1966) (1968), 231-236. - [Wo13b] Wood, D. R., Hypergraph colouring and degeneracy. arXiv:1310.2972 (2013).
Quoted from FormalConjectures/ErdosProblems/1022.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/1022.
The file states 3 research or textbook statements: 3 solved.
Erdos1022.erdos_1022
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/latest/ErdosProblems/Erdos1022.lean.
Is there a constant \(c_t\), where \(c_t\to \infty\) as \(t\to \infty\), such that if \(\mathcal{F}\) is a finite family of finite sets, all of size at least \(t\), and for every set \(X\) there are \(\lt c_t\lvert X\rvert\) many \(A\in \mathcal{F}\) with \(A\subseteq X\), then \(\mathcal{F}\) has chromatic number \(2\) (in other words, has property B)?
This is false, and \(c_t<2\) for all \(t\): a counterexample is provided by Wood [Wo13b], who constructs, for any \(r\geq 2\), a triangle-free \(2\)-degenerate \(r\)-uniform hypergraph with chromatic number \(3\). A similar counterexample was found independently by KoishiChan in the comments.
This was formalized in Lean by Alexeev using Aristotle.
theorem erdos_1022 :
¬ ∃ c : ℕ → ℝ, Filter.Tendsto c Filter.atTop Filter.atTop ∧
∀ t : ℕ, SparseImpliesPropertyB t (c t)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1022.lean, line 60.
Erdos1022.erdos_1022.variants.lt_two
Solved: stated here without proof.
This is false, and \(c_t<2\) for all \(t\): a counterexample is provided by Wood [Wo13b], who constructs, for any \(r\geq 2\), a triangle-free \(2\)-degenerate \(r\)-uniform hypergraph with chromatic number \(3\). A similar counterexample was found independently by KoishiChan in the comments.
theorem erdos_1022.variants.lt_two :
∀ (t : ℕ) (c : ℝ), SparseImpliesPropertyB t c → c < 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1022.lean, line 72.
Erdos1022.erdos_1022.variants.lovasz
Solved: stated here without proof.
Erdős originally conjectured, in this language, that \(c_2=1\), which he reports in [Er71] was proved by Lovász.
theorem erdos_1022.variants.lovasz :
IsGreatest {c : ℝ | SparseImpliesPropertyB 2 c} 1
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1022.lean, line 81.
Sources
TheoremErdős Problem 1023#
References: - erdosproblems.com/1023 - [Er71, p.105] Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109.
Quoted from FormalConjectures/ErdosProblems/1023.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/1023.
The file states 3 research or textbook statements: 3 solved.
Erdos1023.erdos_1023
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1023.lean.
Let \(F(n)\) be the maximal size of a family of subsets of \(\{1,\ldots,n\}\) such that no set in this family is the union of other members of the family. Is it true that there is a constant \(c>0\) such that
\[F(n)\sim c \frac{2^n}{n^{1/2}}?\]Hunter observes in the comments that this follows from the solution to [447], which implies \(F(n)\sim \binom{n}{n/2}\).
theorem erdos_1023 :
∃ c : ℝ, 0 < c ∧
((fun n : ℕ => (F n : ℝ)) ~[atTop]
(fun n : ℕ => c * 2 ^ n / (n : ℝ) ^ (1 / 2 : ℝ)))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1023.lean, line 55.
Erdos1023.erdos_1023.variants.erdos_kleitman
Solved: stated here without proof.
Erdős and Kleitman proved in unpublished work that
\[F(n)\asymp \frac{2^n}{n^{1/2}}.\]([Er71] has an exponent of \(3/2\), but this is presumably a typo.)
theorem erdos_1023.variants.erdos_kleitman :
(fun n : ℕ => (F n : ℝ)) =Θ[atTop] (fun n : ℕ => (2 : ℝ) ^ n / (n : ℝ) ^ (1 / 2 : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1023.lean, line 67.
Erdos1023.erdos_1023.variants.hunter
Solved: stated here without proof.
Hunter observes in the comments that this follows from the solution to [447], which implies \(F(n)\sim \binom{n}{n/2}\).
theorem erdos_1023.variants.hunter :
(fun n : ℕ => (F n : ℝ)) ~[atTop] (fun n : ℕ => (n.choose (n / 2) : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1023.lean, line 76.
Sources
TheoremErdős Problem 1024#
References: - erdosproblems.com/1024 - [PhRo86] Phelps, K. T. and R\"odl, V., Steiner triple systems with minimum independence number. Ars Combin. (1986), 167--172.
Quoted from FormalConjectures/ErdosProblems/1024.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/1024.
The file states 1 research or textbook statement: 1 solved.
Erdos1024.erdos_1024
Solved: stated here without proof.
Let \(f(n)\) be such that every \(3\)-uniform linear hypergraph on \(n\) vertices contains an independent set on \(f(n)\) vertices. Estimate \(f(n)\).
Phelps and Rödl [PhRo86] proved \(f(n) \asymp (n\log n)^{1/2}\).
theorem erdos_1024 :
(fun n ↦ (Hypergraph.linearIndependenceNumber n : ℝ)) =Θ[atTop]
erdos_1024.answer
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1024.lean, line 44.
Sources
TheoremErdős Problem 1025#
References: - erdosproblems.com/1025 - [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. - [ErHa58] Erdős, P. and Hajnal, A., On the structure of set mappings. Acta Math. Acad. Sci. Hungar. (1958), 111-133. - [Sp72] Spencer, Joel, Turán's theorem for \(k\)-graphs. Discrete Math. (1972), 183--186. - [CFS16] Conlon, David and Fox, Jacob and Sudakov, Benny, Short proofs of some extremal results II. J. Combin. Theory Ser. B (2016), 173--196.
Quoted from FormalConjectures/ErdosProblems/1025.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/1025.
The file states 1 research or textbook statement: 1 solved.
Erdos1025.erdos_1025
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1025.lean#L829.
Let \(f\) be a function from all pairs of elements in \(\{1,\ldots,n\}\) to \(\{1,\ldots,n\}\) such that \(f(x,y)\neq x\) and \(\neq y\) for all \(x,y\). We call \(X\subseteq \{1,\ldots,n\}\) independent if whenever \(x,y\in X\) we have \(f(x,y)\not\in X\).
Let \(g(n)\) be such that, in every function \(f\), there is an independent set of size at least \(g(n)\). Estimate \(g(n)\).
A question of Erdős and Hajnal [ErHa58], who could prove \(n^{1/3} \ll g(n) \ll (n\log n)^{1/2}\). Spencer [Sp72] proved \(g(n)\gg n^{1/2}\). Conlon, Fox, and Sudakov [CFS16] proved \(g(n)\ll n^{1/2}\).
theorem erdos_1025 : (fun n : ℕ => (g n : ℝ)) =Θ[atTop] fun n : ℕ => √n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1025.lean, line 67.
Sources
TheoremErdős Problem 1026#
References: - erdosproblems.com/1026 - [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. - [Ha57] Hanani, Haim, On the number of monotonic subsequences. Bull. Res. Council Israel Sect. F (1957/58), 11-13. - [St95] Steele, J. Michael, Variations on the monotone subsequence theme of Erdős and Szekeres. (1995), 111-131. - [TWY16] Tidor, J. and Wang, V. and Yang, B., \(1\)-color avoiding paths, special tournaments, and incidence geometry. arXiv:1608.04153 (2016). - [Wa17] Wagner, Adam Zsolt, Large subgraphs in rainbow-triangle free colorings. J. Graph Theory (2017), 141-148.
Quoted from FormalConjectures/ErdosProblems/1026.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/1026.
The file states 5 research or textbook statements: 5 solved.
Erdos1026.erdos_1026
Solved: stated here without proof.
Let \(x_1,\ldots,x_n\) be a sequence of distinct real numbers. Determine
\[ \max\left(\sum x_{i_r}\right), \]where the maximum is taken over all monotonic subsequences.
This is as Erdős posed the problem in [Er71], which is rather ambiguous. Discussion between several users in the comments section has led to the following precise possible question, as posed by van Doorn:
What is the largest constant \(c\) such that, for all sequences of \(n\) real numbers \(x_1,\ldots,x_n\),
\[ \max\left(\sum x_{i_r}\right) > (c-o(1))\frac{1}{\sqrt{n}}\sum x_i \](where again the maximum is taken over all monotonic subsequences)?
Cambie makes the stronger conjecture that if \(x_1,\ldots,x_{k^2}\) are distinct positive real numbers with \(\sum x_i=1\) then there is always a monotonic subsequence with sum at least \(1/k\).
This stronger conjecture appears to have been first proved by Tidor, Wang, and Yang [TWY16], and is also implicit in work of Wagner [Wa17]. A proof was given and formalised by Aristotle (see the comments), with an alternative proof provided by Chan. In particular, this shows that \(c=1\).
theorem erdos_1026 : IsGreatest admissibleConstants 1
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1026.lean, line 94.
Erdos1026.erdos_1026.variants.upper_bound
Solved: stated here without proof.
A construction of Cambie in the comments shows that \(c\leq 1\).
theorem erdos_1026.variants.upper_bound : 1 ∈ upperBounds admissibleConstants
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1026.lean, line 101.
Erdos1026.erdos_1026.variants.lower_bound
Solved: stated here without proof.
Hanani [Ha57] showed that every sequence is the disjoint union of at most \((\sqrt{2}+o(1))\sqrt{n}\) many monotonic subsequences, whence \(c\geq 1/\sqrt{2}\).
theorem erdos_1026.variants.lower_bound : 1 / Real.sqrt 2 ∈ admissibleConstants
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1026.lean, line 109.
Erdos1026.erdos_1026.variants.hanani
Solved: stated here without proof.
Hanani [Ha57] showed that every sequence is the disjoint union of at most \((\sqrt{2}+o(1))\sqrt{n}\) many monotonic subsequences.
theorem erdos_1026.variants.hanani (ε : ℝ) (hε : 0 < ε) :
∀ᶠ n : ℕ in atTop, ∀ x : Fin n → ℝ, Function.Injective x →
∃ (m : ℕ) (I : Fin m → Finset (Fin n)),
(∀ j, MonotoneOn x ↑(I j) ∨ AntitoneOn x ↑(I j)) ∧
(Pairwise fun j k => Disjoint (I j) (I k)) ∧
(Finset.univ : Finset (Fin m)).biUnion I = Finset.univ ∧
(m : ℝ) ≤ (Real.sqrt 2 + ε) * Real.sqrt (n : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1026.lean, line 117.
Erdos1026.erdos_1026.variants.weighted_erdos_szekeres
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1026.lean.
Cambie makes the stronger conjecture that if \(x_1,\ldots,x_{k^2}\) are distinct positive real numbers with \(\sum x_i=1\) then there is always a monotonic subsequence with sum at least \(1/k\). This is a weighted-form of the Erdős-Szekeres theorem, and is also mentioned (as an open question) in a survey on the latter by Steele [St95].
This stronger conjecture appears to have been first proved by Tidor, Wang, and Yang [TWY16], and is also implicit in work of Wagner [Wa17]. A proof was given and formalised by Aristotle (see the comments), with an alternative proof provided by Chan.
theorem erdos_1026.variants.weighted_erdos_szekeres (k : ℕ) (hk : 0 < k) (x : Fin (k ^ 2) → ℝ)
(hx : Function.Injective x) (hx' : ∀ i, 0 < x i) (hsum : (∑ i, x i) = 1) :
∃ S ∈ monotonicSubsequenceSums x, 1 / (k : ℝ) ≤ S
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1026.lean, line 138.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.