Erdős Problem 150 to Erdős Problem 171
TheoremErdős Problem 150#
References: - erdosproblems.com/150 - [Br24] Bradač, D., On a question of Erdős and Nešetřil about minimal cuts in a graph. arXiv:2409.02974 (2024). - [Er88] Erdős, P., Problems and results in combinatorial analysis and graph theory. Discrete Math. (1988), 81-92. - [FKTV08] Fomin, Fedor V. and Kratsch, Dieter and Todinca, Ioan and Villanger, Yngve, Exact algorithms for treewidth and minimum fill-in. SIAM J. Comput. (2008), 1058-1079. - [FoVi12] Fomin, Fedor V. and Villanger, Yngve, Treewidth computation and extremal combinatorics. Combinatorica (2012), 289-308. - [GaMa18] Gaspers, Serge and Mackenzie, Simon, On the number of minimal separators in graphs. J. Graph Theory (2018), 653-659.
Quoted from FormalConjectures/ErdosProblems/150.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/150.
The file states 5 research or textbook statements: 5 solved.
Erdos150.erdos_150
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos150.lean.
A minimal cut of a graph is a minimal set of vertices whose removal disconnects the graph. Let \(c(n)\) be the maximum number of minimal cuts a graph on \(n\) vertices can have.
Does \(c(n)^{1/n}\to \alpha\) for some \(\alpha <2\)?
It is unclear in [Er88] whether Erdős knew that the limit existed, which follows from a simple argument first given in the literature (to the best of my knowledge) by Bradač [Br24].
That \(\alpha<2\) was proved by Fomin, Kratsch, Todinca, and Villanger [FKTV08], who proved \(\alpha \leq 1.7087\). This was independently studied by Bradač [Br24] (unaware of this earlier work), who proved that \(\alpha \leq 2^{H(1/3)}\approx 1.8899\), where \(H(\cdot)\) is the binary entropy function.
This was formalized in Lean by Monticone using Aristotle.
theorem erdos_150 :
∃ α : ℝ, α < 2 ∧
Tendsto (fun n : ℕ ↦ (maxMinimalCuts n : ℝ) ^ (1 / n : ℝ)) atTop (𝓝 α)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/150.lean, line 73.
Erdos150.erdos_150.variants.erdos_nesetril
Solved: stated here without proof.
Asked by Erdős and Nešetřil, who also ask whether \(c(3m+2)=3^m\).
Note that the lower bound \(1.4457\leq \alpha\) of Gaspers and Mackenzie [GaMa18] provides a negative answer to the above question of Erdős and Nešetřil.
theorem erdos_150.variants.erdos_nesetril :
¬ ∀ m : ℕ, maxMinimalCuts (3 * m + 2) = 3 ^ m
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/150.lean, line 85.
Erdos150.erdos_150.variants.seymour
Solved: stated here without proof.
Seymour observed that \(c(3m+2)\geq 3^m\), as seen by the graph of \(m\) independent paths of length \(4\) joining two vertices.
theorem erdos_150.variants.seymour (m : ℕ) : 3 ^ m ≤ maxMinimalCuts (3 * m + 2)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/150.lean, line 94.
Erdos150.erdos_150.variants.lower_bound
Solved: stated here without proof.
The current best-known bounds on \(\alpha\) are
\[1.4457\leq \alpha \leq \frac{1+\sqrt{5}}{2}\approx 1.618.\]The lower bound is due to Gaspers and Mackenzie [GaMa18].
theorem erdos_150.variants.lower_bound (α : ℝ)
(hα : Tendsto (fun n : ℕ ↦ (maxMinimalCuts n : ℝ) ^ (1 / n : ℝ)) atTop (𝓝 α)) :
1.4457 ≤ α
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/150.lean, line 103.
Erdos150.erdos_150.variants.upper_bound
Solved: stated here without proof.
The current best-known bounds on \(\alpha\) are
\[1.4457\leq \alpha \leq \frac{1+\sqrt{5}}{2}\approx 1.618.\]The upper bound is due to Fomin and Villanger [FoVi12] (with a simpler proof in [GaMa18]).
theorem erdos_150.variants.upper_bound (α : ℝ)
(hα : Tendsto (fun n : ℕ ↦ (maxMinimalCuts n : ℝ) ^ (1 / n : ℝ)) atTop (𝓝 α)) :
α ≤ (1 + Real.sqrt 5) / 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/150.lean, line 114.
Sources
TheoremErdős Problem 151#
References: - erdosproblems.com/151 - [Er88] Erdős, P., Problems and results in combinatorial analysis and graph theory. Discrete Math. (1988), 81-92. - [EGT92] Erdős, P. and Gallai, T. and Tuza, Zs., Covering the cliques of a graph with vertices. Discrete Math. (1992), 279-289.
Quoted from FormalConjectures/ErdosProblems/151.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/151.
The file states 4 research or textbook statements: 2 open and 2 solved.
Erdos151.erdos_151
Open: stated without proof.
For a graph \(G\), let \(\tau(G)\) denote the minimal number of vertices that include at least one from each maximal clique of \(G\) on at least two vertices. Let \(H(n)\) be maximal such that every triangle-free graph on \(n\) vertices contains an independent set on \(H(n)\) vertices.
If \(G\) is a graph on \(n\) vertices, is \(\tau(G)\leq n-H(n)\)?
Erdős remarked that this is perhaps completely wrongheaded [Er88].
theorem erdos_151 :
∀ (n : ℕ) (G : SimpleGraph (Fin n)), cliqueTransversalNumber G ≤ n - H n
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/151.lean, line 52.
Erdos151.erdos_151.variants.cliqueFree_four
Open: stated without proof.
Erdős and Gallai made no progress on the question even when \(G\) is \(K_4\)-free [Er88].
theorem erdos_151.variants.cliqueFree_four :
∀ (n : ℕ) (G : SimpleGraph (Fin n)), G.CliqueFree 4 →
cliqueTransversalNumber G ≤ n - H n
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/151.lean, line 60.
Erdos151.erdos_151.variants.cliqueFree_three
Solved: stated here without proof.
If \(G\) is triangle-free, then \(\tau(G)\leq n-H(n)\): the complement of an independent set meets every edge.
theorem erdos_151.variants.cliqueFree_three (n : ℕ) (G : SimpleGraph (Fin n))
(hG : G.CliqueFree 3) : cliqueTransversalNumber G ≤ n - H n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/151.lean, line 70.
Erdos151.erdos_151.variants.sqrt_bound
Solved: stated here without proof.
It is easy to see that \(\tau(G)\leq n-\sqrt{n}\). We state this with \(\lfloor\sqrt{n}\rfloor\): with the real square root the bound fails for a single edge (\(n = 2\), \(\tau = 1\)).
theorem erdos_151.variants.sqrt_bound (n : ℕ) (G : SimpleGraph (Fin n)) :
cliqueTransversalNumber G ≤ n - Nat.sqrt n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/151.lean, line 79.
Sources
TheoremErdős Problem 152#
TODO: Formalize the corresponding conjecture for infinite Sidon sets.
References: - erdosproblems.com/152 - [DM26a] DeepMind prover agent, formal proof of Erdős problem 152 (2026) - [DM26b] DeepMind prover agent, formal proof of the quadratic variant of Erdős problem 152 (2026) - [ESS94] Erdős, P. and Sárközy, A. and Sós, T., On Sum Sets of Sidon Sets, I. Journal of Number Theory (1994), 329-347.
Quoted from FormalConjectures/ErdosProblems/152.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/152.
The file states 2 research or textbook statements: 2 solved.
Erdos152.erdos_152
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/29c60aa79729701905cf9e92517af23f588971f2/FormalConjectures/ErdosProblems/152.lean#L485.
Must
lim f n = ∞?This was proved formally by the DeepMind prover agent [DM26a].
theorem erdos_152 : Tendsto f atTop atTop
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/152.lean, line 54.
Erdos152.erdos_152.variants.square
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/ff58c933d53bb807bf85d98a47402703f9f14ed3/FormalConjectures/ErdosProblems/152.lean#L496.
Must
f n ≫ n ^ 2?This stronger quadratic variant was also proved formally by the DeepMind prover agent [DM26b].
theorem erdos_152.variants.square :
(fun n => f n : ℕ → ℝ) ≫ (fun n => n ^ 2 : ℕ → ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/152.lean, line 65.
Sources
TheoremErdős Problem 153#
TODO: Formalize the corresponding conjecture for infinite Sidon sets.
References: - erdosproblems.com/153 - [ESS94] Erdős, P. and Sárközy, A. and Sós, T., On Sum Sets of Sidon Sets, I. Journal of Number Theory (1994), 329-347.
Quoted from FormalConjectures/ErdosProblems/153.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/153.
The file states 1 research or textbook statement: 1 open.
Erdos153.erdos_153
Open: stated without proof.
Let \(A\) be a finite Sidon set and \(A+A=\{s_1\lt \cdots\lt s_t\}\). Is it true that
\[\frac{1}{t}\sum_{1\leq i\lt t}(s_{i+1}-s_i)^2 \to \infty\]as \(\lvert A\rvert\to \infty\)?
theorem erdos_153 : Tendsto f atTop atTop
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/153.lean, line 49.
Sources
TheoremErdős Problem 154#
References: - erdosproblems.com/154 - [Li98] Lindström, Bernt, Well distribution of Sidon sets in residue classes. J. Number Theory (1998), 197-200. - [Ko99] Kolountzakis, Mihail N., On the uniform distribution in residue classes of dense sets of integers with distinct sums. J. Number Theory (1999), 147-153. - [ESS94] Erdős, P. and Sárközy, A. and Sós, T., On Sum Sets of Sidon Sets, I. Journal of Number Theory (1994), 329-347.
Quoted from FormalConjectures/ErdosProblems/154.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/154.
The file states 2 research or textbook statements: 2 solved.
Erdos154.erdos_154
Solved: stated here; a Lean proof is at https://github.com/willblair0708/lean-proofs/blob/f297d710018270c66b296082766334974260bcbc/ErdosProblems/Erdos154/Sumset.lean#L555.
Let \(A\subset \{1,\ldots,N\}\) be a Sidon set with \(\lvert A\rvert\sim N^{1/2}\). Must \(A+A\) be well-distributed over all small moduli? In particular, must about half the elements of \(A+A\) be even and half odd?
The answer is yes. Lindström [Li98] proved the analogous statement for \(A\) itself (see
erdos_154.variants.lindstrom), later strengthened by Kolountzakis [Ko99]; well-distribution of \(A+A\) then follows using the Sidon property.We state the question for the sumset: for any sequence of Sidon sets \(A_k\subseteq\{0,\ldots,N_k\}\) with \(N_k\to\infty\) and \(\lvert A_k\rvert\sim N_k^{1/2}\), and any modulus \(m\geq 2\), the proportion of elements of \(A_k+A_k\) congruent to \(i\pmod m\) (i.e. the count divided by \(\lvert A_k+A_k\rvert\)) tends to \(1/m\) for every residue \(i\lt m\).
theorem erdos_154 :
∀ (m : ℕ) (hm : 2 ≤ m) (N : ℕ → ℕ) (A : ℕ → Finset ℕ),
Tendsto (fun k => (N k : ℝ)) atTop atTop →
(∀ k, ∀ x ∈ A k, x ≤ N k) →
(∀ k, IsSidon (A k : Set ℕ)) →
Tendsto (fun k => ((A k).card : ℝ) / Real.sqrt (N k)) atTop (nhds 1) →
∀ i < m, Tendsto
(fun k => (((A k + A k).filter (fun s => s % m = i)).card : ℝ) / ((A k + A k).card : ℝ))
atTop (nhds (1 / m))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/154.lean, line 58.
Erdos154.erdos_154.variants.lindstrom
Solved: stated here; a Lean proof is at https://github.com/Woett/Lean-files/blob/main/ErdosProblem154.lean.
Lindström's result for \(A\) itself [Li98], later strengthened by Kolountzakis [Ko99]: for any sequence of Sidon sets \(A_k\subseteq\{0,\ldots,N_k\}\) with \(N_k\to\infty\) and \(\lvert A_k\rvert\sim N_k^{1/2}\), and any modulus \(m\geq 2\), the number of elements of \(A_k\) congruent to \(i\pmod m\), divided by \(N_k^{1/2}\), tends to \(1/m\) for every residue \(i\lt m\).
Well-distribution of \(A+A\) (the actual question,
erdos_154) follows from this using the Sidon property.
theorem erdos_154.variants.lindstrom :
∀ (m : ℕ) (hm : 2 ≤ m) (N : ℕ → ℕ) (A : ℕ → Finset ℕ),
Tendsto (fun k => (N k : ℝ)) atTop atTop →
(∀ k, ∀ x ∈ A k, x ≤ N k) →
(∀ k, IsSidon (A k : Set ℕ)) →
Tendsto (fun k => ((A k).card : ℝ) / Real.sqrt (N k)) atTop (nhds 1) →
∀ i < m, Tendsto
(fun k => (((A k).filter (fun a => a % m = i)).card : ℝ) / Real.sqrt (N k))
atTop (nhds (1 / m))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/154.lean, line 80.
Sources
TheoremErdős Problem 155#
Reference: erdosproblems.com/155
Quoted from FormalConjectures/ErdosProblems/155.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/155.
The file states 1 research or textbook statement: 1 open.
Erdos155.erdos_155
Open: stated without proof.
Is it true that for every \(k \geq 1\) we have
\[ F(N + k) \leq F(N) + 1 \]for all sufficiently large \(N\)?
theorem erdos_155 : ∀ k ≥ 1, ∀ᶠ N in atTop, F (N + k) ≤ F N + 1
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/155.lean, line 45.
Sources
TheoremErdős Problem 156#
References: - erdosproblems.com/156 - [ESS94] Erdős, P. and Sárközy, A. and Sós, T., On Sum Sets of Sidon Sets, I. Journal of Number Theory (1994), 329-347. - [Ru98b] Ruzsa, Imre Z., A small maximal Sidon set. Ramanujan J. (1998), 55-58.
Quoted from FormalConjectures/ErdosProblems/156.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/156.
The file states 3 research or textbook statements: 1 open and 2 solved. It also has 1 test statement, counted here but not shown.
Erdos156.erdos_156
Open: stated without proof.
Does there exist a maximal Sidon set \(A\subset \{1,\ldots,N\}\) of size \(O(N^{1/3})\)?
A question of Erdős, Sárközy, and Sós [ESS94].
theorem erdos_156 :
(fun N ↦ (minMaximalSidonSet N : ℝ)) =O[atTop] (fun N ↦ (N : ℝ) ^ (1 / 3 : ℝ))
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/156.lean, line 50.
Erdos156.erdos_156.variants.greedy_lower_bound
Solved: stated here without proof.
It is easy to prove that the greedy construction of a maximal Sidon set in \(\{1,\ldots,N\}\) has size \(\gg N^{1/3}\).
theorem erdos_156.variants.greedy_lower_bound :
(fun N ↦ ((Finset.greedySidonBelow N).card : ℝ)) ≫ (fun N ↦ (N : ℝ) ^ (1 / 3 : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/156.lean, line 65.
Erdos156.erdos_156.variants.ruzsa_upper_bound
Solved: stated here without proof.
Ruzsa [Ru98b] constructed a maximal Sidon set of size \(\ll (N\log N)^{1/3}\).
theorem erdos_156.variants.ruzsa_upper_bound :
(fun N ↦ (minMaximalSidonSet N : ℝ)) ≪
(fun N ↦ ((N : ℝ) * Real.log N) ^ (1 / 3 : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/156.lean, line 73.
Sources
TheoremErdős Problem 157#
References: - erdosproblems.com/157 - [ESS94] Erdős, P. and Sárközy, A. and Sós, T., On sum sets of Sidon sets, I. Journal of Number Theory (1994), 329-347. - [Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269. - [Pi23] Pilatte, C., A solution to the Erdős–Sárközy–Sós problem on asymptotic Sidon bases of order 3. Compositio Math. (2024), 1418-1432.
Quoted from FormalConjectures/ErdosProblems/157.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/157.
The file states 1 research or textbook statement: 1 solved.
Erdos157.erdos_157
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos157/Unconditional.lean.
Does there exist an infinite Sidon set which is an asymptotic basis of order \(3\)?
Yes, as shown by Pilatte [Pi23].
theorem erdos_157 :
∃ A : Set ℕ, A.Infinite ∧ IsSidon A ∧ A.IsAsymptoticAddBasisOfOrder 3
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/157.lean, line 45.
Sources
TheoremErdős Problem 158#
References: - erdosproblems.com/158 - [ESS94] Erdős, P. and Sárközy, A. and Sós, T., On Sum Sets of Sidon Sets, I. Journal of Number Theory (1994), 329-347.
Quoted from FormalConjectures/ErdosProblems/158.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/158.
The file states 3 research or textbook statements: 1 open and 2 solved. It also has 1 API statement, counted here but not shown.
Erdos158.erdos_158
Open: stated without proof.
Let
Abe an infiniteB₂[2]set. Mustliminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) = 0?
theorem erdos_158 : ∀ A : Set ℕ, A.Infinite → B2 2 A →
liminf (fun N : ℕ => (A ∩ .Iio N).ncard * (N : ℝ) ^ (- 1 / 2 : ℝ)) atTop = 0
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/158.lean, line 60.
Erdos158.erdos_158.variants.isSidon'
Solved: stated here without proof.
Let
Abe an infinite Sidon set. Thenliminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) * (log N) ^ (1 / 2) < ∞. This is proved in [ESS94].
theorem erdos_158.variants.isSidon' {A : Set ℕ} (hAinf : A.Infinite) (hAsid : IsSidon A) :
liminf (fun N ↦ ENNReal.ofReal ((A ∩ .Iio N).ncard * N ^ (- 1 / 2 : ℝ) * log N ^ (1 / 2 : ℝ)))
atTop < ⊤
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/158.lean, line 67.
Erdos158.erdos_158.variants.isSidon
Proved here.
As a corollary of
erdos_158.isSidon', we can prove thatliminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) = 0for any infinite Sidon setA.
theorem erdos_158.variants.isSidon {A : Set ℕ} (hAinf : A.Infinite) (hAsid : IsSidon A) :
liminf (fun N : ℕ => (A ∩ .Iio N).ncard * (N : ℝ) ^ (- 1 / 2 : ℝ)) atTop = 0
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/158.lean, line 75.
Sources
TheoremErdős Problem 159#
References: - erdosproblems.com/159 - [Er78] Erdős, P., Problems and results in combinatorial analysis and combinatorial number theory. Proc. Ninth Southeastern Conf. Combinatorics, Graph Theory and Computing (1978), 29-40. - [Sp77] Spencer, J., Asymptotic lower bounds for Ramsey functions. Discrete Math. (1977), 69-76.
Quoted from FormalConjectures/ErdosProblems/159.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/159.
The file states 1 research or textbook statement: 1 open.
Erdos159.erdos_159
Open: stated without proof.
There exists some constant \(c>0\) such that
\[R(C_4,K_n) \ll n^{2-c}.\]The prize of $100 is offered in [Er78] for a proof or disproof.
This problem is #17 in Ramsey Theory in the graphs problem collection.
theorem erdos_159 :
∃ (c : ℝ) (_ : 0 < c) (C : ℝ),
∀ (n : ℕ), 1 ≤ n →
(SimpleGraph.graphRamsey (SimpleGraph.cycleGraph 4)
(SimpleGraph.completeGraph (Fin n)) : ℝ) ≤ C * (n : ℝ) ^ (2 - c)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/159.lean, line 43.
Sources
TheoremErdős Problem 160#
Reference: erdosproblems.com/160
Quoted from FormalConjectures/ErdosProblems/160.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/160.
The file states 4 research or textbook statements: 2 open and 2 solved.
Erdos160.erdos_160.known_upper
Solved: stated here without proof.
On Mathoverflow user leechlattice shows that \(h(n) \ll n^{\frac 2 3}\).
theorem erdos_160.known_upper :
(fun n => (erdos_160.h n : ℝ)) =O[atTop] fun n => (n : ℝ) ^ ((2 : ℝ) / 3)
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/160.lean, line 48.
Erdos160.erdos_160.better_upper
Open: stated without proof.
Estimate \(h(n)\) by finding a better upper bound.
theorem erdos_160.better_upper :
(fun n => (erdos_160.h n : ℝ)) =O[atTop] erdos_160.better_upper.answer ∧
erdos_160.better_upper.answer =o[atTop] fun n => (n : ℝ) ^ ((2 : ℝ) / 3)
Category research open; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/160.lean, line 60.
Erdos160.erdos_160.better_lower
Open: stated without proof.
Estimate \(h(n)\) by finding a better lower bound.
theorem erdos_160.better_lower:
(erdos_160.better_lower.answer =O[atTop] fun n => (erdos_160.h n : ℝ)) ∧
∀ c > 0,
(fun (n : ℕ) => exp (c * log n ^ ((1 : ℝ) / 12))) =O[atTop] (fun n => (erdos_160.h n : ℝ)) →
∀ c > 0, (fun (n : ℕ) => exp (c * log n ^ ((1 : ℝ) / 12))) =o[atTop]
erdos_160.better_lower.answer
Category research open; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/160.lean, line 71.
Erdos160.erdos_160.variants.known_lower
Solved: stated here without proof.
The observation of Zachary Hunter in that question coupled with the bounds of Kelley-Meka KeMe23 imply that
\[h(N) \gg \exp(c(\log N)^{\frac 1 {12}})\]for some \(c > 0\).
theorem erdos_160.variants.known_lower :
∃ c > 0, (fun (n : ℕ) => exp (c * log (n : ℝ) ^ ((1 : ℝ) / 12)))
=O[atTop] fun n => (erdos_160.h n : ℝ)
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/160.lean, line 86.
Sources
TheoremErdős Problem 161#
References: - erdosproblems.com/161 - [CFS11] Conlon, David and Fox, Jacob and Sudakov, Benny, Large almost monochromatic subsets in hypergraphs. Israel J. Math. (2011), 423--432. - [Er90b] Erdős, Paul, Problems and results on graphs and hypergraphs: similarities and differences . Mathematics of Ramsey theory (1990), 12-28.
Quoted from FormalConjectures/ErdosProblems/161.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/161.
The file states 2 research or textbook statements: 2 open.
Erdos161.erdos_161.parts.i
Open: stated without proof.
Let \(\alpha\in[0,1/2)\) and \(n,t\geq 1\). Let \(F^{(t)}(n,\alpha)\) be the smallest \(m\) such that we can \(2\)-colour the edges of the complete \(t\)-uniform hypergraph on \(n\) vertices such that if \(X\subseteq [n]\) with \(\lvert X\rvert \geq m\) then there are at least \(\alpha \binom{\lvert X\rvert}{t}\) many \(t\)-subsets of \(X\) of each colour. For fixed \(n,t\) as we change \(\alpha\) from \(0\) to \(1/2\) does \(F^{(t)}(n,\alpha)\) increase continuously or are there jumps? Only one jump?
Here growth is compared up to constant factors as \(n\to\infty\). At \(\alpha=0\), each color must occur, following the source's Ramsey convention.
theorem erdos_161.parts.i :
∀ t : ℕ, 1 ≤ t →
{p | p.1 ∈ Set.Ico (0 : ℝ) (1 / 2) ∧ p.2 ∈ Set.Ico (0 : ℝ) (1 / 2) ∧
(fun n ↦ (Hypergraph.balancedColoringThreshold n t p.1 : ℝ)) =Θ[atTop]
(fun n ↦ (Hypergraph.balancedColoringThreshold n t p.2 : ℝ))} =
erdos_161.parts.i.answer t
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/161.lean, line 50.
Erdos161.erdos_161.parts.ii
Open: stated without proof.
For fixed \(t\geq 3\), do all positive densities below \(1/2\) give the same asymptotic order?
theorem erdos_161.parts.ii :
∀ t : ℕ, 3 ≤ t → ∀ α β : ℝ,
0 < α → α < 1 / 2 → 0 < β → β < 1 / 2 →
(fun n ↦ (Hypergraph.balancedColoringThreshold n t α : ℝ)) =Θ[atTop]
(fun n ↦ (Hypergraph.balancedColoringThreshold n t β : ℝ))
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/161.lean, line 62.
Sources
TheoremErdős Problem 162#
References: - erdosproblems.com/162 - [Er90b] Erdős, Paul, Problems and results on graphs and hypergraphs: similarities and differences. Mathematics of Ramsey theory (1990), 12-28.
Quoted from FormalConjectures/ErdosProblems/162.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/162.
The file states 3 research or textbook statements: 1 open, 1 solved and 1 textbook result. It also has 2 API statements, counted here but not shown.
Erdos162.erdos_162
Open: stated without proof.
Let \(\alpha > 0\) and \(n \geq 1\). Let \(F(n,\alpha)\) be the largest \(k\) such that there exists some 2-colouring of the edges of \(K_n\) in which any induced subgraph \(H\) on at least \(k\) vertices contains more than \(\alpha\binom{|H|}{2}\) many edges of each colour.
Prove that for every fixed \(0 \leq \alpha \leq 1/2\), as \(n \to \infty\), \(F(n,\alpha) \sim c_\alpha \log n\) for some constant \(c_\alpha\).
We require \(\alpha < 1/2\): at \(\alpha = 1/2\) no colouring works for any
k ≤ n(seeerdos_162.variants.half).
theorem erdos_162 (α : ℝ) (h0 : 0 ≤ α) (h1 : α < 1 / 2) :
∃ c : ℝ, (fun n : ℕ ↦ (F n α : ℝ)) ~[atTop] (fun n : ℕ ↦ c * Real.log n)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/162.lean, line 65.
Erdos162.erdos_162.variants.bounds
Solved: stated here without proof.
It is easy to show with the probabilistic method that there exist \(c_1(\alpha), c_2(\alpha)\) such that \(c_1(\alpha)\log n < F(n,\alpha) < c_2(\alpha)\log n\).
theorem erdos_162.variants.bounds (α : ℝ) (h0 : 0 ≤ α) (h1 : α < 1 / 2) :
∃ c₁ c₂ : ℝ, 0 < c₁ ∧ c₁ < c₂ ∧ ∀ᶠ n : ℕ in atTop,
c₁ * Real.log n < F n α ∧ (F n α : ℝ) < c₂ * Real.log n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/162.lean, line 74.
Erdos162.erdos_162.variants.half
Textbook result, proved here.
At \(\alpha = 1/2\) the two colour counts in \(H\) add up to \(\binom{|H|}{2}\), so both cannot exceed half of it. Hence \(F(n, 1/2) = n + 1\), and the claim fails at \(\alpha = 1/2\).
theorem erdos_162.variants.half (n : ℕ) : F n (1 / 2) = n + 1
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/162.lean, line 84.
Sources
TheoremErdős Problem 163#
References: - erdosproblems.com/163 - [BuEr75] Burr, S. A. and Erdős, P., On the Ramsey number of graphs with small degree-ratio. Colloq. Math. Soc. János Bolyai (1975). - [Le17] Lee, C., Ramsey numbers of degenerate graphs. Ann. of Math. (2) 185 (2017), 791-829.
Quoted from FormalConjectures/ErdosProblems/163.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/163.
The file states 1 research or textbook statement: 1 solved.
Erdos163.erdos_163
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos163.lean#L53.
The Burr-Erdős conjecture: For any \(d\geq 1\) if \(H\) is a graph such that every subgraph contains a vertex of degree at most \(d\) then
\[R(H)\ll_d n.\]Solved by Lee [Le17], who proved that \(R(H) \leq 2^{2^{O(d)}}n\).
This problem is #9 in Ramsey Theory in the graphs problem collection.
The linked formal proof (Codex and GPT-5.6 Sol) gives, for graphs
HonFin n, a natural constantC ≥ 1withRamseyFor H (C * n)(every red/blue colouring ofK_{C n}contains a monochromatic copy ofH); transporting alongFintype.equivFingives the statement below.
theorem erdos_163 :
∀ (d : ℕ), 1 ≤ d →
∃ C > (0 : ℝ), ∀ (V : Type) [Fintype V] (H : SimpleGraph V),
H.IsDegenerate d →
(SimpleGraph.diagonalGraphRamsey H : ℝ) ≤ C * Fintype.card V
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/163.lean, line 50.
Sources
TheoremErdős Problem 164#
References: - erdosproblems.com/164 - [Er76g] Erdős, P., Problems and results on combinatorial number theory. II. J. Indian Math. Soc. (N.S.) (1976), 285-298. - [Er86] Erdős, P., Problémes et résultats en théorie des nombres. (1986). - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999). - [ABLLPSTT26] B. Alexeev, K. Barreto, Y. Li, J. D. Lichtman, L. Price, J. I. Shah, Q. Tang, and T. Tao, Primitive sets and Von Mangoldt Chains: Erdős problem #1196 and beyond. arXiv:2605.00301 (2026). - [Er35] Erdős, Paul, Note on Sequences of Integers No One of Which is Divisible By Any Other. J. London Math. Soc. (1935), 126-128. - [Li23] Lichtman, J. D., A proof of the Erdős primitive set conjecture. arXiv:2202.02384 (2023).
Quoted from FormalConjectures/ErdosProblems/164.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/164.
The file states 1 research or textbook statement: 1 solved.
Erdos164.erdos_164
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos164.lean.
A set \(A\subset \mathbb{N}\) is primitive if no member of \(A\) divides another. Is the sum
\[\sum_{n\in A}\frac{1}{n\log n}\]maximised over all primitive sets when \(A\) is the set of primes?
Erdős [Er35] proved that this sum always converges for a primitive set. Lichtman [Li23] proved that the answer is yes. An alternative, simpler, proof is given by Alexeev, Barreto, Li, Lichtman, Price, Shah, Tang, and Tao [ABLLPSTT26].
theorem erdos_164 :
∀ A : Set ℕ, (∀ a ∈ A, 2 ≤ a) → Erdos1196.IsPrimitive A →
(∑' a : A, 1 / ((a : ℕ) * Real.log (a : ℕ))) ≤
∑' p : {p : ℕ | p.Prime}, 1 / ((p : ℕ) * Real.log (p : ℕ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/164.lean, line 54.
Sources
TheoremErdős Problem 165#
References: - erdosproblems.com/165 - [Er61] Erdős, P., Graph theory and probability. II. Canad. J. Math. (1961), 346-352. - [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. - [Er90b] Erdős, Paul, Problems and results on graphs and hypergraphs: similarities and differences. Mathematics of Ramsey theory (1990), 12-28. - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350. - [Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67. - [Sh83] Shearer, J. B., A note on the independence number of triangle-free graphs. Discrete Math. (1983), 83-87. - [Ki95] Kim, J. H., The Ramsey number \(R(3,t)\) has order of magnitude \(t^2/\log t\). Random Structures Algorithms (1995), 173-207. - [CJMS25] Campos, M. and Jenssen, M. and Michelen, M. and Sahasrabudhe, J., A new lower bound for the Ramsey numbers \(R(3,k)\). arXiv:2505.13371 (2025). - [HHKP25] Hefty, Z. and Horn, P. and King, D. and Pfender, F., Improving \(R(3,k)\) in just two bites. arXiv:2510.19718 (2025).
Quoted from FormalConjectures/ErdosProblems/165.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/165.
The file states 4 research or textbook statements: 2 open and 2 solved.
Erdos165.erdos_165
Open: stated without proof.
Give an asymptotic formula for \(R(3,k)\).
theorem erdos_165 :
(fun k : ℕ ↦ (R(3, k) : ℝ)) ~[atTop] erdos_165.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/165.lean, line 60.
Erdos165.erdos_165.variants.conjecture
Open: stated without proof.
Campos, Jenssen, Michelen and Sahasrabudhe [CJMS25] and Hefty, Horn, King and Pfender [HHKP25] conjecture that \(R(3,k) \sim \frac{k^2}{2\log k}\).
theorem erdos_165.variants.conjecture :
(fun k : ℕ ↦ (R(3, k) : ℝ)) ~[atTop] (fun k : ℕ ↦ (k : ℝ) ^ 2 / (2 * Real.log k))
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/165.lean, line 69.
Erdos165.erdos_165.variants.upper
Solved: stated here without proof.
Shearer [Sh83] proved \(R(3,k) \leq (1+o(1))\frac{k^2}{\log k}\).
theorem erdos_165.variants.upper :
∀ ε > (0 : ℝ), ∀ᶠ k : ℕ in atTop,
(R(3, k) : ℝ) ≤ (1 + ε) * (k : ℝ) ^ 2 / Real.log k
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/165.lean, line 77.
Erdos165.erdos_165.variants.lower
Solved: stated here without proof.
Hefty, Horn, King and Pfender [HHKP25] proved \(R(3,k) \geq (1/2+o(1))\frac{k^2}{\log k}\), improving earlier bounds of Kim [Ki95] and Campos, Jenssen, Michelen and Sahasrabudhe [CJMS25].
theorem erdos_165.variants.lower :
∀ ε > (0 : ℝ), ∀ᶠ k : ℕ in atTop,
(1 / 2 - ε) * (k : ℝ) ^ 2 / Real.log k ≤ (R(3, k) : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/165.lean, line 87.
Sources
TheoremErdős Problem 166#
References: - erdosproblems.com/166 - [Sp77] Spencer, J., Asymptotic lower bounds for Ramsey functions. Discrete Math. (1977), 69-76. - [AKS80] Ajtai, M., Komlós, J. and Szemerédi, E., A note on Ramsey numbers. J. Combin. Theory Ser. A (1980), 354-360. - [MaVe23] Mattheus, S. and Verstraëte, J., The asymptotics of \(r(4,t)\). Ann. of Math. (2024), 941-965.
Quoted from FormalConjectures/ErdosProblems/166.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/166.
The file states 2 research or textbook statements: 2 solved. It also has 1 test statement, counted here but not shown.
Erdos166.erdos_166
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos166.lean#L83.
Prove that
\[R(4,k) \gg \frac{k^3}{(\log k)^{O(1)}}.\]This is true, and was proved by Mattheus and Verstraëte [MaVe23], who showed that \(R(4,k) \gg \frac{k^3}{(\log k)^4}\). This problem is #5 in Ramsey Theory in the graphs problem collection.
The linked formal proof (Codex and GPT-5.6 Sol, via the construction of Bradač used for Problem 920) gives
k ^ 3 / (log k) ^ c = O(R(4, k))for a naturalc > 0, with the Ramsey number defined throughCliqueFree/IndepSetFree; this implies the statement below.
theorem erdos_166 :
∃ (c C : ℝ), 0 < c ∧ 0 < C ∧
∀ᶠ (k : ℕ) in atTop,
(SimpleGraph.classicalRamsey 4 k : ℝ) ≥
C * (k : ℝ) ^ 3 / (Real.log k) ^ c
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/166.lean, line 53.
Erdos166.erdos_166.variants.mattheus_verstraete
Solved: stated here without proof.
Mattheus and Verstraëte [MaVe23] proved the explicit lower bound
\[R(4,k) \gg \frac{k^3}{(\log k)^4}.\]
theorem erdos_166.variants.mattheus_verstraete :
∃ C : ℝ, 0 < C ∧ ∀ᶠ (k : ℕ) in atTop,
(SimpleGraph.classicalRamsey 4 k : ℝ) ≥ C * (k : ℝ) ^ 3 / (Real.log k) ^ 4
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/166.lean, line 65.
Sources
TheoremErdős Problem 168#
Reference: erdosproblems.com/168
Quoted from FormalConjectures/ErdosProblems/168.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/168.
The file states 3 research or textbook statements: 2 open and 1 solved. It also has 6 API statements, counted here but not shown.
Erdos168.erdos_168.parts.i
Open: stated without proof.
What is the limit \(F(N)/N\) as \(N \to \infty\)?
theorem erdos_168.parts.i :
Filter.Tendsto (fun N => (F N / N : ℝ)) Filter.atTop (𝓝 erdos_168.parts.i.answer)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/168.lean, line 94.
Erdos168.erdos_168.parts.ii
Open: stated without proof.
Is the limit \(F(N)/N\) as \(N \to \infty\) irrational?
theorem erdos_168.parts.ii :
Irrational (Filter.atTop.limsup (fun N => (F N / N : ℝ)))
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/168.lean, line 100.
Erdos168.erdos_168.variants.limit_exists
Solved: stated here without proof.
The limit \(F(N)/N\) as \(N \to \infty\) exists. (proved by Graham, Spencer, and Witsenhausen)
theorem erdos_168.variants.limit_exists :
∃ x, Filter.Tendsto (fun N => (F N / N : ℝ)) Filter.atTop (𝓝 x)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/168.lean, line 106.
Sources
LemmaErdős Problem 170#
Reference: erdosproblems.com/170
Quoted from FormalConjectures/ErdosProblems/170.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/170.
The file states 2 research or textbook statements: 1 open and 1 solved. It also has 1 API statement, counted here but not shown.
Erdos170.erdos170
Open: stated without proof.
The problem is to determine the limit of the sequence \(\frac{F(N)}{\sqrt{N}}\) as \(N \to \infty\).
lemma erdos170 : Filter.Tendsto (fun N => F N / √N) Filter.atTop (𝓝 erdos170.answer)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/170.lean, line 63.
Erdos170.erdos170.existing_bounds
Solved: stated here without proof.
The existence of the limit has been proved by Erdős and Gál [ErGa48]. The lower bound has been proven by Leech [Le56], who refined an argument of Rédei and Rényi. The upper bound is due to Wichmann [Wi63].
lemma erdos170.existing_bounds :
∃ x ∈ Set.Icc lower_bound upper_bound,
Filter.Tendsto (fun N => F N / √N) Filter.atTop (𝓝 x)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/170.lean, line 74.
Sources
TheoremErdős Problem 171#
References: - erdosproblems.com/171 - [ErGr79] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory: van der Waerden's theorem and related topics. Enseign. Math. (1979), 325-344. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [FuKa91] Furstenberg, H. and Katznelson, Y., A density version of the Hales-Jewett Theorem. Journal d'Analyse Mathématique (1991), 64-119. - [Po12] Polymath, D. H. J., A new proof of the density Hales–Jewett theorem. Ann. Math. (2012), 1283-1327.
Quoted from FormalConjectures/ErdosProblems/171.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/171.
The file states 1 research or textbook statement: 1 solved.
Erdos171.erdos_171
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos171.lean#L42.
Is it true that for every \(\epsilon>0\) and integer \(t\geq 1\), if \(N\) is sufficiently large and \(A\) is a subset of \([t]^N\) of size at least \(\epsilon t^N\) then \(A\) must contain a combinatorial line \(P\) (a set \(P=\{p_1,\ldots,p_t\}\) where for each coordinate \(1\leq j\leq t\) the \(j\)th coordinate of \(p_i\) is either \(i\) or constant).
The 'density Hales-Jewett' problem. This was proved by Furstenberg and Katznelson [FuKa91]. A new elementary proof, which gives quantitative bounds, was proved by the Polymath project [Po12].
Combinatorial lines are Mathlib's
Combinatorics.Line (Fin t) (Fin N)(which have at least one non-constant coordinate).
theorem erdos_171 : ∀ ε : ℝ, 0 < ε → ∀ t : ℕ, 1 ≤ t → ∀ᶠ N : ℕ in atTop,
∀ A : Finset (Fin N → Fin t), ε * t ^ N ≤ A.card →
∃ l : Combinatorics.Line (Fin t) (Fin N), ∀ i : Fin t, l i ∈ A
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/171.lean, line 57.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.