Erdős Problem 100 to Erdős Problem 123
TheoremErdős Problem 100#
References: * erdosproblems.com/100 * [Kanold](No references found) * [GuKa15](Guth, Larry and Katz, Nets Hawk, On the Erd\H{o}s distinct distances problem in the plane. Ann. of Math. (2) (2015), 155-190.) * [Piepmeyer](No references found)
Quoted from FormalConjectures/ErdosProblems/100.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/100.
The file states 5 research or textbook statements: 2 open and 3 solved.
Erdos100.erdos_100
Open: stated without proof.
Is the diameter of \(A\) at least \(Cn\) for some constant \(C > 0\)?
theorem erdos_100 :
∃ C > (0 : ℝ), ∀ᶠ n in atTop, ∀ A : Finset ℝ²,
A.card = n →
DistancesSeparated A →
diam (A : Set ℝ²) > C * n
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/100.lean, line 44.
Erdos100.erdos_100.variants.strong
Open: stated without proof.
Stronger conjecture: diameter \(\geq n - 1\) for sufficiently large \(n\).
theorem erdos_100.variants.strong :
∀ᶠ n in atTop, ∀ A : Finset ℝ²,
A.card = n →
DistancesSeparated A →
diam (A : Set ℝ²) ≥ n - 1
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/100.lean, line 53.
Erdos100.erdos_100.variants.kanold
Solved: stated here without proof.
From [Kanold]: diameter \(\geq n^{3/4}\). TODO: find reference
theorem erdos_100.variants.kanold :
∃ C > (0 : ℝ), ∀ᶠ n in atTop, ∀ A : Finset ℝ²,
A.card = n →
DistancesSeparated A →
diam (A : Set ℝ²) ≥ (n : ℝ) ^ (3 / 4 : ℝ)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/100.lean, line 63.
Erdos100.erdos_100.variants.guth_katz
Solved: stated here without proof.
From [GuKa15]: diameter \(\gg n / \log n\).
theorem erdos_100.variants.guth_katz :
∃ C > (0 : ℝ), ∀ᶠ n in atTop, ∀ A : Finset ℝ²,
A.card = n →
DistancesSeparated A →
diam (A : Set ℝ²) ≥ C * n / log n
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/100.lean, line 72.
Erdos100.erdos_100_piepmeyer
Solved: stated here; a Lean proof is at https://github.com/theaustinhatfield/formal-conjectures/blob/solve-erdos-100-piepmeyer/FormalConjectures/ErdosProblems/100.lean.
From [Piepmeyer]: 9 points with diameter \(< 5\). TODO: find reference
theorem erdos_100_piepmeyer :
∃ A : Finset ℝ², A.card = 9 ∧ DistancesSeparated A ∧
diam (A : Set ℝ²) < 5
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/100.lean, line 83.
Sources
TheoremErdős Problem 101#
Reference: erdosproblems.com/101
Quoted from FormalConjectures/ErdosProblems/101.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/101.
The file states 1 research or textbook statement: 1 open.
Erdos101.erdos_101
Open: stated without proof.
Given \(n\) points in \(\mathbb{R}^2\), no five of which are on a line, the number of lines containing four points is \(o(n^2)\).
theorem erdos_101 : (fun n => (numLinesWithFourPointMax n : ℝ)) =o[atTop] (fun n => (n : ℝ)^2)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/101.lean, line 47.
Sources
TheoremErdős Problem 102#
Reference: erdosproblems.com/102
Quoted from FormalConjectures/ErdosProblems/102.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/102.
The file states 4 research or textbook statements: 2 open and 2 solved. It also has 4 API statements, counted here but not shown.
Erdos102.erdos_102
Open: stated without proof.
Let \(c > 0\) and let \(h_c(n)\) be such that for any \(n\) points in \(\mathbb{R}^2\) with at least \(cn^2\) lines that each contain more than three of the points, some line contains \(h_c(n)\) of the points. Is it true that, for fixed \(c > 0\), \(h_c(n) \to \infty\)?
theorem erdos_102 :
∀ c > 0, ∀ M : ℕ, ∀ᶠ n in atTop, (M : ℕ∞) ≤ h c n
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/102.lean, line 116.
Erdos102.erdos_102.variants.five
Open: stated without proof.
It is not known whether \(h_c(n) \geq 5\) for all sufficiently large \(n\).
theorem erdos_102.variants.five :
∀ c > 0, ∀ᶠ n in atTop, (5 : ℕ∞) ≤ h c n
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/102.lean, line 124.
Erdos102.erdos_102.variants.upper_sqrt
Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/eee8e904a0eb8511302bc809b9486116ec079e69/Proofs/T_Erdos102_erdos_102_variants_upper_sqrt.lean#L1100.
It is easy to see that \(h_c(n) \ll_c n^{1/2}\): for all sufficiently small \(c > 0\) there are admissible configurations (e.g. grids) in which no line contains more than \(C_c n^{1/2}\) points.
theorem erdos_102.variants.upper_sqrt :
∃ c₀ > (0 : ℝ), ∀ c ∈ Set.Ioc 0 c₀, ∃ C : ℝ, ∀ᶠ n in atTop,
h c n ≤ (⌈C * Real.sqrt n⌉₊ : ℕ∞)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/102.lean, line 134.
Erdos102.erdos_102.variants.hunter
Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/eee8e904a0eb8511302bc809b9486116ec079e69/Proofs/T_Erdos102_erdos_102_variants_hunter.lean#L1113.
Erdős [Er95] suggested that perhaps \(h_c(n) \gg_c n^{1/2}\). Zach Hunter pointed out that this is false: the points of \(\{1, \dots, m\}^d\) with \(n \approx m^d\), randomly projected to \(\mathbb{R}^2\), meet every line in \(\ll_d n^{1/d}\) points and determine \(\gg_d n^2\) lines with more than three points. This gives \(h_c(n) \ll n^{1 / \log(1/c)}\); we state the underlying form: for every \(d \geq 1\) there is \(c > 0\) with \(h_c(n) \ll_d n^{1/d}\).
theorem erdos_102.variants.hunter :
∀ d : ℕ, 1 ≤ d → ∃ c > (0 : ℝ), ∃ C : ℝ, ∀ᶠ n in atTop,
h c n ≤ (⌈C * (n : ℝ) ^ (1 / (d : ℝ))⌉₊ : ℕ∞)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/102.lean, line 148.
Sources
TheoremErdős Problem 103#
References: - erdosproblems.com/103
Quoted from FormalConjectures/ErdosProblems/103.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/103.
The file states 2 research or textbook statements: 2 open.
Erdos103.erdos_103
Open: stated without proof.
Let \(h(n)\) count the number of incongruent sets of \(n\) points in \(\mathbb{R}^2\) which minimise the diameter subject to the constraint that \(d(x,y)\geq 1\) for all points \(x\neq y\). Is it true that \(h(n)\to \infty\)?
theorem erdos_103 : Tendsto h atTop (nhds ⊤)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/103.lean, line 61.
Erdos103.erdos_103.variants.two_le
Open: stated without proof.
It is not even known whether \(h(n)\geq 2\) for all large \(n\).
theorem erdos_103.variants.two_le : ∀ᶠ n in atTop, 2 ≤ h n
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/103.lean, line 68.
Sources
TheoremErdős Problem 104#
References: - erdosproblems.com/104 - [El84] Elekes, G., {\(n\)} points in the plane can determine \(n^{3/2}\) unit circles. Combinatorica (1984), 131. - [Er75h] Erdős, P., Some problems on elementary geometry. Austral. Math. Soc. Gaz. (1975), 2-3. - [Er81d] Erdős, P., Some applications of graph theory and combinatorial methods to number theory and geometry. Algebraic methods in graph theory, Vol. I, II (Szeged, 1978) (1981), 137-148. - [Er92e] Erdős, Pál, Some Unsolved problems in Geometry, Number Theory and Combinatorics. Eureka (1992), 44-48. - [HaMe86] Harborth, Heiko and Mengersen, Ingrid, Point sets with many unit circles. Discrete Math. (1986), 193--197.
Quoted from FormalConjectures/ErdosProblems/104.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/104.
The file states 1 research or textbook statement: 1 open.
Erdos104.erdos_104
Open: stated without proof.
Given \(n\) points in \(\mathbb{R}^2\) the number of distinct unit circles containing at least three points is \(o(n^2)\).
theorem erdos_104 :
(fun n : ℕ => (maxUnitCircleCount n : ℝ)) =o[atTop] (fun n : ℕ => (n : ℝ) ^ 2)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/104.lean, line 61.
Sources
TheoremErdős Problem 105#
References: - erdosproblems.com/105 - [Be83] Beck, József, On the lattice property of the plane and some problems of Dirac, Motzkin and Erdős in combinatorial geometry. Combinatorica (1983), 281-297. - [ErPu95] Erdős, P. and Purdy, G., Two combinatorial problems in the plane. Discrete Comput. Geom. (1995), 441-443. - [SzTr83] Szemerédi, Endre and Trotter, Jr., William T., Extremal problems in discrete geometry. Combinatorica (1983), 381-392.
Quoted from FormalConjectures/ErdosProblems/105.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/105.
The file states 4 research or textbook statements: 4 solved.
Erdos105.erdos_105
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos105.lean.
Let \(A,B\subset \mathbb{R}^2\) be disjoint sets of size \(n\) and \(n-3\) respectively, with not all of \(A\) contained on a single line. Is there a line which contains at least two points from \(A\) and no points from \(B\)?
This has been disproved by Xichuan in the comments, who has found three explicit counterexamples.
theorem erdos_105 :
¬ ∀ A B : Finset ℝ², Disjoint A B → A.card = B.card + 3 →
¬ Collinear ℝ (A : Set ℝ²) →
∃ p ∈ A, ∃ q ∈ A, p ≠ q ∧ ∀ b ∈ B, b ∉ line[ℝ, p, q]
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/105.lean, line 49.
Erdos105.erdos_105.variants.hickerson
Solved: stated here without proof.
A construction of Hickerson shows that this fails with \(n-2\).
theorem erdos_105.variants.hickerson : ¬ ∀ A B : Finset ℝ², Disjoint A B →
A.card = B.card + 2 → ¬ Collinear ℝ (A : Set ℝ²) →
∃ p ∈ A, ∃ q ∈ A, p ≠ q ∧ ∀ b ∈ B, b ∉ line[ℝ, p, q]
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/105.lean, line 59.
Erdos105.erdos_105.variants.beck_szemeredi_trotter
Solved: stated here without proof.
A result independently proved by Beck [Be83] and Szemerédi and Trotter [SzTr83] (see [211]) implies it is true with \(n-3\) replaced by \(cn\) for some constant \(c>0\).
theorem erdos_105.variants.beck_szemeredi_trotter : ∃ c > (0 : ℝ),
∀ A B : Finset ℝ², Disjoint A B → (B.card : ℝ) ≤ c * A.card →
¬ Collinear ℝ (A : Set ℝ²) →
∃ p ∈ A, ∃ q ∈ A, p ≠ q ∧ ∀ b ∈ B, b ∉ line[ℝ, p, q]
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/105.lean, line 69.
Erdos105.erdos_105.variants.sub_four
Solved: stated here; a Lean proof is at https://github.com/kusasyu36/erdos105-sub-four/blob/a2d073034d2d15af216d8bd71771f1eda13b3de3/Erdos105SubFour.lean#L93.
It remains possible that this holds with \(n-4\) (or in general with \(n-O(1)\) or \((1-o(1))n\)).
This fails with \(n-4\) as well: Core_65536 gives an explicit counterexample in the forum (24 July 2026), with \(|A| = 10\) and \(|B| = 6\) and integer coordinates, in which every line through two points of \(A\) contains a point of \(B\). The incidences have been verified in Lean.
theorem erdos_105.variants.sub_four :
¬ ∀ A B : Finset ℝ², Disjoint A B → A.card = B.card + 4 →
¬ Collinear ℝ (A : Set ℝ²) →
∃ p ∈ A, ∃ q ∈ A, p ≠ q ∧ ∀ b ∈ B, b ∉ line[ℝ, p, q]
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/105.lean, line 86.
Sources
TheoremErdős Problem 107#
References: - erdosproblems.com/107 - Wikipedia
Quoted from FormalConjectures/ErdosProblems/107.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/107.
The file states 5 research or textbook statements: 1 open and 4 solved. It also has 2 test statements, counted here but not shown.
Erdos107.erdos_107
Open: stated without proof.
Let \(f(n)\) be minimal such that any \(f(n)\) points in \(ℝ^2\), no three on a line, contain \(n\) points which form the vertices of a convex \(n\)-gon. Prove that \(f(n) = 2^{n-2} + 1\).
theorem erdos_107 : ∀ n ≥ 3, f n = 2^(n - 2) + 1
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/107.lean, line 50.
Erdos107.nonempty_cardSet
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/cd3cf0b176e95209584bf35555a7c0e501255f6e/erdos-107/Solution.lean#L59.
For every \(n ≥ 3\), there exists \(N\) such that any \(N\) points, no three on a line, contain a convex \(n\)-gon.
theorem nonempty_cardSet : ∀ n ≥ 3, (cardSet n).Nonempty
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/107.lean, line 58.
Erdos107.variants.ersz_bounds
Solved: stated here without proof.
Erdős and Szekeres proved the bounds
\[ 2^{n-2} + 1 ≤ f(n) ≤ \binom{2n-4}{n-2} + 1 \]([ErSz60] and [ErSz35] respectively).
[ErSz60] Erdős, P. and Szekeres, G., On some extremum problems in elementary geometry. Ann. Univ. Sci. Budapest. Eötvös Sect. Math. (1960/61), 53-62.
[ErSz35] Erdős, P. and Szekeres, G., A combinatorial problem in geometry. Compos. Math. (1935), 463-470.
theorem ersz_bounds :
∀ n ≥ 3, 2^(n - 2) + 1 ≤ f n ∧ f n ≤ Nat.choose (2 * n - 4) (n - 2) + 1
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/107.lean, line 141.
Erdos107.variants.su_bound
Solved: stated here without proof.
Suk [Su17] proved
\[ f(n) ≤ 2^{(1+o(1))n}. \][Su17] Suk, Andrew, On the Erdős-Szekeres convex polygon problem. J. Amer. Math. Soc. (2017), 1047-1053.
theorem su_bound :
∃ r : ℕ → ℝ, r =o[atTop] (fun n => (n : ℝ)) ∧
∀ n ≥ 3, (f n : ℝ) ≤ 2^(n + r n)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/107.lean, line 155.
Erdos107.variants.hmpt_bound
Solved: stated here without proof.
The current best bound is due to Holmsen, Mojarrad, Pach, and Tardos [HMPT20], who prove
\[ f(n) ≤ 2^{n+O(\sqrt{n\log n})}. \][HMPT20] Holmsen, Andreas F. and Mojarrad, Hossein Nassajian and Pach, János and Tardos, Gábor, Two extensions of the Erdős-Szekeres problem. J. Eur. Math. Soc. (JEMS) (2020), 3981-3995.
theorem hmpt_bound :
∃ r : ℕ → ℝ, r =O[atTop] (fun n => Real.sqrt (n * Real.log n)) ∧
∀ n ≥ 3, (f n : ℝ) ≤ 2^(n + r n)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/107.lean, line 171.
Sources
TheoremErdős Problem 108#
Reference: erdosproblems.com/108
Quoted from FormalConjectures/ErdosProblems/108.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/108.
The file states 1 research or textbook statement: 1 open.
Erdos108.erdos_108
Open: stated without proof.
For every r ≥ 4 and k ≥ 2 is there some finite f(k,r) such that every graph of chromatic number ≥ f(k,r) contains a subgraph of girth ≥ r and chromatic number ≥ k?
theorem erdos_108 :
∀ r ≥ 4, ∀ k ≥ (2 : ℕ), ∃ (f : ℕ),
∀ (V : Type u) (G : SimpleGraph V) (_ : Nonempty V)
(hchro : f ≤ SimpleGraph.chromaticNumber G),
∃ (H : G.Subgraph), (SimpleGraph.girth H.coe ≥ r) ∧
(SimpleGraph.chromaticNumber H.coe ≥ k)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/108.lean, line 39.
Sources
TheoremErdős Problem 109#
References: - erdosproblems.com/109 - [MRR19] J. Moreira, F.K. Richter, and D. Robertson, A proof of a sumset conjecture of Erdős, Annals of Math. 189 (2019), 605-652.
Quoted from FormalConjectures/ErdosProblems/109.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/109.
The file states 1 research or textbook statement: 1 solved.
Erdos109.erdos_109
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos109.lean#L9074.
Any \(A\subseteq \mathbb{N}\) of positive upper density contains a sumset \(B+C\) where both \(B\) and \(C\) are infinite.
The Erdős sumset conjecture. Proved by Moreira, Richter, and Robertson [MRR19].
theorem erdos_109 (A : Set ℕ) (h : A.upperDensity > 0) :
∃ B C : Set ℕ, B.Infinite ∧ C.Infinite ∧ B + C ⊆ A
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/109.lean, line 44.
Sources
TheoremErdős Problem 110#
References: - erdosproblems.com/110 - [EHS82] Erdős, P. and Hajnal, A. and Szemerédi, E., On almost bipartite large chromatic graphs. Theory and practice of combinatorics (1982), 117-123. PDF - [Er87] Erdős, P., Some problems on finite and infinite graphs. Logic and combinatorics (Arcata, Calif., 1985) (1987), 223-228. PDF - [Er95d] Erdős, Paul, On some problems in combinatorial set theory. Publ. Inst. Math. (Beograd) (N.S.) (1995), 61-65. - [KoSh05] Komjáth, Péter and Shelah, Saharon, Finite subgraphs of uncountably chromatic graphs. J. Graph Theory (2005), 28--38. - [La20] Lambie-Hanson, Chris, On the growth rate of chromatic numbers of finite subgraphs. Adv. Math. (2020), 107176, 13. arXiv:1902.08177 - [dBEr51] de Bruijn, N. G. and Erdős, P., A colour problem for infinite graphs and a problem in the theory of relations. Indag. Math. (1951), 369--373.
Quoted from FormalConjectures/ErdosProblems/110.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/110.
The file states 3 research or textbook statements: 3 solved.
Erdos110.erdos_110
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos110.lean#L161.
Is there some \(F(n)\) such that every graph with chromatic number \(\aleph_1\) has, for all large \(n\), a subgraph with chromatic number \(n\) on at most \(F(n)\) vertices?
A question of Erdős, Hajnal, and Szemerédi (see [EHS82], [Er87, p. 225, Problem 6], [Er95d]). The answer is no: Komjáth and Shelah [KoSh05] proved that it is consistent that the answer is no, and Lambie-Hanson [La20, Theorem A] constructed a counterexample in ZFC. The statement below is therefore the negation. Subgraphs need not be induced, and finiteness of
H.vertsis explicit becauseSet.ncardis0on infinite sets. Graphs are taken inType 1, the universe of the vertex type in the linked proof's construction. A counterexample inTypewould give one inType 1byULift; conversely, Lambie-Hanson's graph has \(2^{\aleph_1}\) vertices, so it also exists inType.
theorem erdos_110 :
¬ ∃ F : ℕ → ℕ, ∀ (V : Type 1) (G : SimpleGraph V), Erdos737.ChromaticNumberAlephOne G →
∀ᶠ n : ℕ in atTop, ∃ H : G.Subgraph,
H.verts.Finite ∧ H.verts.ncard ≤ F n ∧ H.coe.chromaticNumber = (n : ℕ∞)
Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/110.lean, line 63.
Erdos110.erdos_110.variants.lambie_hanson
Solved: stated here without proof.
Lambie-Hanson's quantitative theorem [La20, Theorem A], of which
erdos_110is a consequence: for every \(f : \mathbb{N} \to \mathbb{N}\) there is a graph with chromatic number \(\aleph_1\) such that, for every \(k \geq 3\), every finite subgraph with fewer than \(f(k)\) vertices has chromatic number less than \(k\). (The graph constructed in [La20] has \(2^{\aleph_1}\) vertices.)
theorem erdos_110.variants.lambie_hanson (f : ℕ → ℕ) :
∃ (V : Type 1) (G : SimpleGraph V), Erdos737.ChromaticNumberAlephOne G ∧
∀ k : ℕ, 3 ≤ k → ∀ H : G.Subgraph, H.verts.Finite → H.verts.ncard < f k →
H.coe.chromaticNumber < (k : ℕ∞)
Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/110.lean, line 76.
Erdos110.erdos_110.variants.de_bruijn_erdos
Solved: stated here without proof.
A theorem of de Bruijn and Erdős [dBEr51] implies that, if \(G\) has infinite chromatic number, then \(G\) has a finite subgraph of chromatic number \(n\) for every \(n\geq 1\).
Infinite chromatic number is
G.chromaticNumber = ⊤.
theorem erdos_110.variants.de_bruijn_erdos {V : Type*} (G : SimpleGraph V)
(hG : G.chromaticNumber = ⊤) (n : ℕ) (hn : 1 ≤ n) :
∃ H : G.Subgraph, H.verts.Finite ∧ H.coe.chromaticNumber = (n : ℕ∞)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/110.lean, line 89.
Sources
TheoremErdős Problem 111#
References: - erdosproblems.com/111 - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. (1981) - [EHS82] Erdős, P., Hajnal, A., and Szemerédi, E., On almost bipartite large chromatic graphs. Theory and practice of combinatorics (1982), 117–123. - [Er87] Erdős, P., Some problems on finite and infinite graphs. (1987) - [Er90] Erdős, P., Some of my favourite unsolved problems. (1990) - [Er97d] Erdős, P., Some recent problems and results in graph theory. (1997) - [Er97f] Erdős, P., Some unsolved problems. (1997)
See also Erdős Problem [74].
Formalization notes
bipartiteDistance G: the minimum number of edges to delete from a (finite) simple graph \(G\) to make it bipartite. Defined as the infimum over all spanning subgraphs \(H \leq G\) withH.IsBipartiteof the number of edges inG.edgeSet \ H.edgeSet.
hG G n: for a graph \(G\) on vertex type \(V\),hG G nis the supremum over all sets \(S\) of vertices of cardinality \(n\) ofbipartiteDistance (G.induce S). This matches the problem's formulation: "any subgraph of \(G\) on \(n\) vertices can be made bipartite after deleting at most \(h_G(n)\) edges."
Quoted from FormalConjectures/ErdosProblems/111.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/111.
The file states 4 research or textbook statements: 2 open and 2 solved.
Erdos111.erdos_111
Open: stated without proof.
Erdős Problem 111 (Erdős, Hajnal, Szemerédi [EHS82]):
If \(G\) is a graph with chromatic number \(\aleph_1\), is it true that \(h_G(n)/n \to \infty\)?
Formally: for every graph \(G\) (on a type \(V\)) with chromatic cardinal \(\aleph_1\), the ratio \(h_G(n)/n\) tends to infinity: for every constant \(C\), all sufficiently large \(n\) satisfy \(h_G(n) > C \cdot n\).
theorem erdos_111 :
∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = ℵ_ 1 →
Filter.Tendsto (fun n : ℕ => (hG G n : ℝ) / n) Filter.atTop Filter.atTop
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/111.lean, line 83.
Erdos111.erdos_111.variants.lower_bound
Solved: stated here without proof.
Linear lower bound (ZFC, [EHS82]): Every graph \(G\) with chromatic number \(\aleph_1\) has \(h_G(n) \geq c \cdot n\) for some positive constant \(c > 0\) and all sufficiently large \(n\) (i.e., the linear lower bound \(h_G(n) \gg n\) is known).
This follows from the fact that every graph with uncountable chromatic number contains \(\aleph_1\) vertex-disjoint odd cycles of some fixed odd length \(\ell\): any induced subgraph on \(n\) vertices containing \(\gg n / \ell\) such cycles requires removing \(\gg n\) edges to become bipartite.
This is a strictly weaker statement than the headline
erdos_111, which asks for \(h_G(n)/n \to \infty\) (i.e., \(h_G(n)\) grows super-linearly — the constantccould be taken arbitrarily large for a fixed graph \(G\)). Whether the linear lower bound can be improved to super-linear remains the open question.
theorem erdos_111.variants.lower_bound :
∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = ℵ_ 1 →
∃ c : ℝ, 0 < c ∧
∀ᶠ n : ℕ in Filter.atTop, c * n ≤ hG G n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/111.lean, line 106.
Erdos111.erdos_111.variants.upper_bound_existence
Solved: stated here without proof.
Upper bound existence (Erdős-Hajnal-Szemerédi [EHS82]): There exists a graph \(G\) with chromatic number \(\aleph_1\) such that \(h_G(n) \ll n^{3/2}\), i.e., there is a constant \(C > 0\) with \(h_G(n) \leq C \cdot n^{3/2}\) for all \(n\).
theorem erdos_111.variants.upper_bound_existence :
∃ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = ℵ_ 1 ∧
(fun n : ℕ => (hG G n : ℝ)) =O[atTop] (fun n : ℕ => (n : ℝ) ^ (3 / 2 : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/111.lean, line 118.
Erdos111.erdos_111.variants.erdos_conjecture
Open: stated without proof.
Erdős conjectured [Er81] that for every \(\varepsilon > 0\) there is a graph \(G\) with \(\chi(G) = \aleph_1\) such that \(h_G(n) \ll n^{1+\varepsilon}\). The graph is chosen after \(\varepsilon\).
theorem erdos_111.variants.erdos_conjecture :
∀ ε : ℝ, 0 < ε → ∃ (V : Type) (G : SimpleGraph V),
G.chromaticCardinal = ℵ_ 1 ∧
(fun n : ℕ => (hG G n : ℝ)) =O[atTop] (fun n : ℕ => (n : ℝ) ^ (1 + ε))
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/111.lean, line 129.
Sources
TheoremErdős Problem 113#
References: - erdosproblems.com/113 - [ErSi84] Erdős, P. and Simonovits, M., Cube-supersaturated graphs and related problems. Progress in graph theory (Waterloo, Ont., 1982) (1984), 203-218. - [Er90] Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467-478. - [Er91] Erdős, P., Problems and results in combinatorial analysis and combinatorial number theory. Graph theory, combinatorics, and applications, Vol. 1 (Kalamazoo, MI, 1988) (1991), 397-406. - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350. - [Ja23b] Janzer, Oliver, Disproof of a conjecture of Erdős and Simonovits on the Turán number of graphs with minimum degree 3. Int. Math. Res. Not. IMRN (2023), 8478--8494.
Quoted from FormalConjectures/ErdosProblems/113.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/113.
The file states 1 research or textbook statement: 1 solved.
Erdos113.erdos_113
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos113.lean#L4902.
If \(G\) is bipartite then \(\mathrm{ex}(n;G)\ll n^{3/2}\) if and only \(G\) is \(2\)-degenerate, that is, \(G\) contains no induced subgraph with minimal degree at least 3.
Conjectured by Erdős and Simonovits [ErSi84]. Erdős first offered $250 for a proof and $100 for a counterexample, but in [Er93] offered $500 for a counterexample. Disproved by Janzer [Ja23b] who constructed, for any \(\epsilon>0\), a \(3\)-regular bipartite graph \(H\) such that
\[\mathrm{ex}(n;H)\ll n^{\frac{4}{3}+\epsilon}.\]The linked formal proof refutes the "only if" direction via Janzer's construction.
theorem erdos_113 : ¬ ∀ (V : Type) [Fintype V] (G : SimpleGraph V), G.IsBipartite →
(((fun n : ℕ => (extremalNumber n G : ℝ)) =O[atTop] fun n : ℕ => (n : ℝ) ^ (3 / 2 : ℝ)) ↔
G.IsDegenerate 2)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/113.lean, line 60.
Sources
TheoremErdős Problem 114#
References: - erdosproblems.com/114 - [EHP58] Erdős, P., Herzog, F. and Piranian, G., Metric properties of polynomials. J. Analyse Math. (1958), 125-148. - [ErHa99] Eremenko, A. and Hayman, W., On the length of lemniscates. Michigan Math. J. (1999), 409-415. arXiv:0805.2295 - [Ta25] Tao, T., The maximal length of the Erdős–Herzog–Piranian lemniscate in high degree (2025). arXiv:2512.12455
Quoted from FormalConjectures/ErdosProblems/114.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/114.
The file states 4 research or textbook statements: 1 open, 2 solved and 1 textbook result.
Erdos114.erdos_114
Open: stated without proof.
If \(p(z) \in \mathbb{C}[z]\) is a monic polynomial of degree \(n\), is the length of the curve \(\{z \in \mathbb{C} : \lvert p(z)\rvert = 1\}\) maximised when \(p(z) = z^n - 1\)?
We require \(n \geq 1\). For \(n = 0\) the only monic polynomial is \(1\), whose level set is all of \(\mathbb{C}\), while \(z^0 - 1 = 0\) has an empty level set.
theorem erdos_114 :
∀ n : ℕ, 1 ≤ n → ∀ p : ℂ[X], p.Monic → p.natDegree = n →
lemniscateLength p ≤ lemniscateLength (X ^ n - 1)
Category research open; AMS 28 Measure and integration, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/114.lean, line 53.
Erdos114.erdos_114.variants.large_n
Solved: stated here without proof.
Tao [Ta25] proved that \(z^n - 1\) maximises the length of the lemniscate for all sufficiently large \(n\).
theorem erdos_114.variants.large_n : ∀ᶠ n in atTop, ∀ p : ℂ[X], p.Monic → p.natDegree = n →
lemniscateLength p ≤ lemniscateLength (X ^ n - 1)
Category research solved; AMS 28 Measure and integration, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/114.lean, line 63.
Erdos114.erdos_114.variants.two
Solved: stated here without proof.
Eremenko and Hayman [ErHa99] proved the case \(n = 2\).
theorem erdos_114.variants.two (p : ℂ[X]) (hp : p.Monic) (hdeg : p.natDegree = 2) :
lemniscateLength p ≤ lemniscateLength (X ^ 2 - 1)
Category research solved; AMS 28 Measure and integration, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/114.lean, line 69.
Erdos114.erdos_114.variants.one
Textbook result, proved here.
The case \(n = 1\). A monic linear polynomial is \(z - a\). Its lemniscate is a translate of the lemniscate of \(z - 1\), and translations preserve Hausdorff measure.
theorem erdos_114.variants.one (p : ℂ[X]) (hp : p.Monic) (hdeg : p.natDegree = 1) :
lemniscateLength p ≤ lemniscateLength (X ^ 1 - 1)
Category textbook; AMS 28 Measure and integration, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/114.lean, line 78.
Sources
TheoremErdős Problem 115#
References: - erdosproblems.com/115 - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Er90] Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467-478. - [ErLe94] Erëmenko, A. and Lempert, L., An extremal problem for polynomials. Proc. Amer. Math. Soc. (1994), 191-193. - [Po59a] Pommerenke, Ch., On the derivative of a polynomial. Michigan Math. J. (1959), 373-375.
Quoted from FormalConjectures/ErdosProblems/115.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/115.
The file states 1 research or textbook statement: 1 solved.
Erdos115.erdos_115
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos115.lean.
If \(p(z)\) is a polynomial of degree \(n\) such that \(\{z : \lvert p(z)\rvert\leq 1\}\) is connected then is it true that
\[\max_{\substack{z\in\mathbb{C}\\ \lvert p(z)\rvert\leq 1}} \lvert p'(z)\rvert \leq (\tfrac{1}{2}+o(1))n^2?\]Eremenko and Lempert [ErLe94] have shown this is true, and in fact Chebyshev polynomials are the extreme examples.
theorem erdos_115 :
∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ p : Polynomial ℂ, p.Monic → p.natDegree = n →
IsConnected {z : ℂ | ‖p.eval z‖ ≤ 1} → ∀ z : ℂ, ‖p.eval z‖ ≤ 1 →
‖p.derivative.eval z‖ ≤ (1 / 2 + ε) * (n : ℝ) ^ 2
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/115.lean, line 51.
Sources
TheoremErdős Problem 116#
References: - erdosproblems.com/116 - [EHP58] Erdős, P. and Herzog, F. and Piranian, G., Metric properties of polynomials. J. Analyse Math. (1958), 125-148. - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79. - [Er90] Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467-478. - [Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67. - [Po61] Pommerenke, Ch., On metric properties of complex polynomials. Michigan Math. J. (1961), 97-115. - [KLR25] M. Krishnapur, E. Lundberg, and K. Ramachandran, On the area of polynomial lemniscates. arXiv:2503.18270 (2025). - [Wa88] Wagner, Gerold, On the area of lemniscate domains. J. Analyse Math. (1988), 159-167. - [Po28] G. Pólya, Beitrag zue Verallgemeinerung des Verzerrungssatzes auf mehrfach zusammenhängende Gebiete. S-B. Akad. Wiss. (1928), 228-232 and 280-282.
Quoted from FormalConjectures/ErdosProblems/116.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/116.
The file states 4 research or textbook statements: 4 solved.
Erdos116.erdos_116
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos116.lean#L918.
Let \(p(z)=\prod_{i=1}^n (z-z_i)\) for \(\lvert z_i\rvert \leq 1\). Is it true that
\[\lvert\{ z: \lvert p(z)\rvert <1\}\rvert>n^{-O(1)}\](or perhaps even \(>(\log n)^{-O(1)}\))?
Conjectured by Erdős, Herzog, and Piranian [EHP58]. The lower bound \(\gg n^{-4}\) follows from a result of Pommerenke [Po61]. The lower bound \(\gg (\log n)^{-1}\) was proved by Krishnapur, Lundberg, and Ramachandran [KLR25].
Wagner [Wa88] proves, for \(n\geq 3\), the existence of such polynomials with
\[\lvert\{ z: \lvert p(z)\rvert <1\}\rvert \ll_\epsilon (\log\log n)^{-1/2+\epsilon}\]for all \(\epsilon>0\). Krishnapur, Lundberg, and Ramachandran [KLR25] improved this upper bound to \(\ll (\log\log n)^{-1}\).
Pólya [Po28] showed the upper bound \(\lvert\{ z: \lvert p(z)\rvert <1\}\rvert \leq \pi\) always holds, and this is achieved only when the \(z_i\) are identical.
theorem erdos_116 : ∃ c : ℝ, 0 < c ∧ ∃ C : ℕ, ∀ n : ℕ, 0 < n →
∀ z : Fin n → ℂ, (∀ i, ‖z i‖ ≤ 1) →
ENNReal.ofReal (c / n ^ C) ≤ volume {w : ℂ | ‖∏ i, (w - z i)‖ < 1}
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/116.lean, line 70.
Erdos116.erdos_116.variants.log
Solved: stated here without proof.
The lower bound \(\lvert\{ z: \lvert p(z)\rvert <1\}\rvert \gg (\log n)^{-1}\) was proved by Krishnapur, Lundberg, and Ramachandran [KLR25]; in particular the answer to the \((\log n)^{-O(1)}\) form of the question is also yes.
theorem erdos_116.variants.log : ∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 2 ≤ n →
∀ z : Fin n → ℂ, (∀ i, ‖z i‖ ≤ 1) →
ENNReal.ofReal (c / Real.log n) ≤ volume {w : ℂ | ‖∏ i, (w - z i)‖ < 1}
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/116.lean, line 81.
Erdos116.erdos_116.variants.upper
Solved: stated here without proof.
Krishnapur, Lundberg, and Ramachandran [KLR25] proved that there are polynomials with \(\lvert\{ z: \lvert p(z)\rvert <1\}\rvert \ll (\log\log n)^{-1}\), improving a result of Wagner [Wa88].
theorem erdos_116.variants.upper : ∃ C : ℝ, ∀ n : ℕ, 3 ≤ n →
∃ z : Fin n → ℂ, (∀ i, ‖z i‖ ≤ 1) ∧
volume {w : ℂ | ‖∏ i, (w - z i)‖ < 1} ≤ ENNReal.ofReal (C / Real.log (Real.log n))
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/116.lean, line 92.
Erdos116.erdos_116.variants.polya
Solved: stated here without proof.
Pólya [Po28]: \(\lvert\{ z: \lvert p(z)\rvert <1\}\rvert \leq \pi\) always holds.
theorem erdos_116.variants.polya (n : ℕ) (z : Fin n → ℂ) :
volume {w : ℂ | ‖∏ i, (w - z i)‖ < 1} ≤ ENNReal.ofReal Real.pi
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/116.lean, line 99.
Sources
TheoremErdős Problem 118#
Reference: erdosproblems.com/118
References: - [Sc99] Schipperus, R. Countable partition ordinals. Thesis, University of Colorado (1999). - [Sc10] Schipperus, R. Countable partition ordinals. Ann. Pure Appl. Logic 161 (2010), 1195–1215. - [Da99] Darby, C. Negative partition relations for ordinals \(\omega^{\omega^\delta}\). J. Combin. Theory Ser. B 76 (1999), 205–222. - [La00] Larson, J. A. An ordinal partition avoiding pentagrams. J. Symbolic Logic 65 (2000), 969–978. - [HST10] Hajnal, A.; Larson, J. A. Partition relations. Handbook of set theory, Springer (2010), 129–213.
Quoted from FormalConjectures/ErdosProblems/118.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/118.
The file states 2 research or textbook statements: 2 solved. It also has 1 test statement, counted here but not shown.
Erdos118.erdos_118
Solved: stated here without proof.
Erdős Problem 118 (problem of Erdős and Hajnal). Let \(\alpha\) be such that \(\alpha \to (\alpha, 3)^2\). For every \(n \ge 3\), must \(\alpha \to (\alpha, n)^2\)?
The original question is asked for cardinals, ordinals, and order types; we state the ordinal version, which is the standard reading: ordinals \(\alpha\) with \(\alpha \to (\alpha, 3)^2\) are called partition ordinals.
The answer is no, shown independently by Schipperus [Sc99, Sc10] and Darby [Da99]. Larson [La00] gave the concrete counterexample \(\alpha = \omega^{\omega^2}\), for which \(\alpha \to (\alpha, 3)^2\) holds yet \(\alpha \not\to (\alpha, 5)^2\). See Chapter 2.9 of [HST10] for further background.
theorem erdos_118 :
¬ ∀ α : Ordinal.{0}, OrdinalRamsey α α 3 →
∀ n : ℕ, 3 ≤ n → OrdinalRamsey α α n
Category research solved; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/118.lean, line 74.
Erdos118.erdos_118.variants.larson
Solved: stated here without proof.
Larson (2000). The ordinal \(\alpha = \omega^{\omega^2}\) is a partition ordinal, \(\omega^{\omega^2} \to (\omega^{\omega^2}, 3)^2\), yet \(\omega^{\omega^2} \not\to (\omega^{\omega^2}, 5)^2\) [La00], so the answer to the Erdős–Hajnal question is negative already at \(n = 5\).
theorem larson : OrdinalRamsey (ω ^ ω ^ (2 : Ordinal)) (ω ^ ω ^ (2 : Ordinal)) 3 ∧
¬ OrdinalRamsey (ω ^ ω ^ (2 : Ordinal)) (ω ^ ω ^ (2 : Ordinal)) 5
Category research solved; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/118.lean, line 90.
Sources
TheoremErdős Problem 119#
References: - erdosproblems.com/119 - [Be91] Beck, J., The modulus of polynomials with zeros on the unit circle: A problem of Erdős. Annals of Math. (1991), 609-651. - [Er57] Erdős, Paul, Some unsolved problems. Michigan Math. J. (1957), 291-300. - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Er64b] Erdős, P., Problems and results on diophantine approximations. Compositio Math. (1964), 52-65. - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79. - [Er90] Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467-478. - [Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10. - [Ha74] Hayman, W. K., Research problems in function theory: new problems. (1974), 155--180. - [Li77] Linden, C. N., The modulus of polynomials with zeros on the unit circle. Bull. London Math. Soc. (1977), 65--69. - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999). - [Wa80] Wagner, Gerold, On a problem of Erdős in {D}iophantine approximation. Bull. London Math. Soc. (1980), 81--88.
Quoted from FormalConjectures/ErdosProblems/119.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/119.
The file states 3 research or textbook statements: 3 solved.
Erdos119.erdos_119.parts.i
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1268917deaaaa0d674f651287027baa26cea9920/src/latest/ErdosProblems/Erdos119.lean#L1759.
Is it true that \(\limsup M_n = \infty\)?
This is Problem 4.1 in [Ha74] where it is attributed to Erdős.
The weaker conjecture that \(\limsup M_n=\infty\) was proved by Wagner [Wa80], who show that there is some \(c>0\) with \(M_n>(\log n)^c\) infinitely often.
theorem erdos_119.parts.i :
∀ (z : ℕ → ℂ) (hz : ∀ i : ℕ, ‖z i‖ = 1),
atTop.limsup (fun n => (M z n : EReal)) = ⊤
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/119.lean, line 77.
Erdos119.erdos_119.parts.ii
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1268917deaaaa0d674f651287027baa26cea9920/src/latest/ErdosProblems/Erdos119.lean#L1712.
Is it true that there exists \(c > 0\) such that for infinitely many \(n\) we have \(M_n > n^c\)?
The second question was answered by Beck [Be91], who proved that there exists some \(c>0\) such that \(\max_{n\leq N} M_n > N^c\).
theorem erdos_119.parts.ii :
∀ (z : ℕ → ℂ) (hz : ∀ i : ℕ, ‖z i‖ = 1),
∃ (c : ℝ) (hc : c > 0), Infinite {n : ℕ | M z n > n ^ c}
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/119.lean, line 90.
Erdos119.erdos_119.parts.iii
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1268917deaaaa0d674f651287027baa26cea9920/src/latest/ErdosProblems/Erdos119.lean#L1687.
Is it true that there exists \(c > 0\) such that, for all large \(n\), \(\sum_{k \leq n} M_k > n^{1 + c}\)?
The $100 prize was offered for the third question in [Er97f]. This was resolved by GPT 5.6 and Korsky (see the proof claims), who proved that \(\sum_{k\leq n}M_k \gg \frac{n^{5/4}}{\sqrt{\log n}}\) (and hence for infinitely many \(n\) we have \(M_n> n^{1/4-o(1)}\)).
theorem erdos_119.parts.iii :
∀ (z : ℕ → ℂ) (hz : ∀ i : ℕ, ‖z i‖ = 1),
∃ (c : ℝ) (hc : c > 0), ∀ᶠ n in atTop,
∑ k ∈ range n, M z k > n ^ (1 + c)
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/119.lean, line 104.
Sources
TheoremErdős Problem 120#
Reference: - erdosproblems.com/120 - St20 Steinhaus, Hugo, Sur les distances des points dans les ensembles de measure positive. Fund. Math. (1920), 93-104.
Quoted from FormalConjectures/ErdosProblems/120.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/120.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos120.erdos_120
Open: stated without proof.
Let \(A \subseteq \mathbb{R}\) be an infinite set. Must there be a set \(E \subseteq \mathbb{R}\) of positive measure which does not contain any set of the shape \(a * A + b\) for some \(a,b \in \mathbb{R}\) and \(a \neq 0\)?
theorem erdos_120 : ∀ A : Set ℝ, A.Infinite → Erdos120For A
Category research open; AMS 05 Combinatorics, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/120.lean, line 48.
Erdos120.erdos_120.variants.finite_set
Solved: stated here without proof.
Steinhaus [St20] has proved Erdős 120 to be false whenever \(A\) is a finite set.
theorem erdos_120.variants.finite_set {A : Set ℝ} (h : A.Finite) : ¬ Erdos120For A
Category research solved; AMS 05 Combinatorics, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/120.lean, line 55.
Sources
TheoremErdős Problem 121#
References: - erdosproblems.com/121 - [Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269. - [Er97] Erdős, Paul, Problems in number theory. New Zealand J. Math. (1997), 155-160. - [Er97e] Erdős, Paul, Some of my favourite unsolved problems. Math. Japon. (1997), 527-537. - [Er98] Erdős, Paul, Some of my new and almost new problems and results in combinatorial number theory. Number theory (Eger, 1996) (1998), 169-180. - [ESS95] Erdős, P. and Sárközy, A. and Sós, V. T., On product representations of powers. I. European J. Combin. (1995), 567-588. - [Er38] P. Erdős, On sequences of integers no one of which divides the product of two others and on related problems. Tomsk. Gos. Univ. Ucen Zap. (1938), 74-82. - [Ta24] Tao, T., On product representations of squares. arXiv:2405.11610 (2024).
Quoted from FormalConjectures/ErdosProblems/121.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/121.
The file states 5 research or textbook statements: 5 solved.
Erdos121.erdos_121
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos121.lean#L87.
Let \(F_{k}(N)\) be the size of the largest \(A\subseteq \{1,\ldots,N\}\) such that the product of no \(k\) many distinct elements of \(A\) is a square. Is \(F_5(N)=(1-o(1))N\)?
Conjectured by Erdős, Sós, and Sárközy [ESS95], who proved \(F_2(N)=\left(\frac{6}{\pi^2}+o(1)\right)N\), \(F_3(N) = (1-o(1))N\), and also established asymptotics for \(F_k(N)\) for all even \(k\geq 4\) (in particular \(F_k(N)\asymp N/\log N\) for all even \(k\geq 4\)). Erdős [Er38] earlier proved that \(F_4(N)=o(N)\) - indeed, if \(\lvert A\rvert \gg N\) and \(A\subseteq \{1,\ldots,N\}\) then there is a non-trivial solution to \(ab=cd\) with \(a,b,c,d\in A\).
This problem was answered in the negative by Tao [Ta24], who proved that for any \(k\geq 4\) there is some constant \(c_k>0\) such that \(F_k(N) \leq (1-c_k+o(1))N\).
See also 888.
theorem erdos_121 : ¬ (fun N : ℕ => (F 5 N : ℝ)) ~[atTop] fun N : ℕ => (N : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/121.lean, line 69.
Erdos121.erdos_121.variants.odd
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos121.lean#L87.
More generally, is \(F_{2k+1}(N)=(1-o(1))N\)? This is false for all \(k \geq 2\) by Tao's theorem [Ta24].
theorem erdos_121.variants.odd : ¬ ∀ k : ℕ, 1 ≤ k →
(fun N : ℕ => (F (2 * k + 1) N : ℝ)) ~[atTop] fun N : ℕ => (N : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/121.lean, line 77.
Erdos121.erdos_121.variants.tao
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos121.lean#L87.
Tao [Ta24] proved that for any \(k\geq 4\) there is some constant \(c_k>0\) such that \(F_k(N) \leq (1-c_k+o(1))N\).
theorem erdos_121.variants.tao (k : ℕ) (hk : 4 ≤ k) :
∃ c : ℝ, 0 < c ∧ ∀ᶠ N : ℕ in atTop, (F k N : ℝ) ≤ (1 - c) * N
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/121.lean, line 86.
Erdos121.erdos_121.variants.three
Solved: stated here without proof.
Erdős, Sós, and Sárközy [ESS95] proved \(F_3(N) = (1-o(1))N\).
theorem erdos_121.variants.three : (fun N : ℕ => (F 3 N : ℝ)) ~[atTop] fun N : ℕ => (N : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/121.lean, line 92.
Erdos121.erdos_121.variants.two
Solved: stated here without proof.
Erdős, Sós, and Sárközy [ESS95] proved \(F_2(N)=\left(\frac{6}{\pi^2}+o(1)\right)N\).
theorem erdos_121.variants.two :
(fun N : ℕ => (F 2 N : ℝ)) ~[atTop] fun N : ℕ => 6 / Real.pi ^ 2 * N
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/121.lean, line 97.
Sources
TheoremErdős Problem 123#
References: - erdosproblems.com/123 - [ChYu23b] Chen, Yong-Gao and Yu, Wang-Xing, On {\(d\)}-complete sequences of integers, {II}. Acta Arith. (2023), 161--181. - [Er92b] Erdős, Paul, Some of my favourite problems in various branches of combinatorics. Matematiche (Catania) (1992), 231-240. - [Er97] Erdős, Paul, Problems in number theory. New Zealand J. Math. (1997), 155-160. - [Er97e] Erdős, Paul, Some of my favourite unsolved problems. Math. Japon. (1997), 527-537. - [ErLe96] Erdős, P. and Lewin, Mordechai, \(d\)-complete sequences of integers. Math. Comp. (1996), 837-840. - [MaCh16] Ma, Mi-Mi and Chen, Yong-Gao, On {\(d\)}-complete sequences of integers. J. Number Theory (2016), 1--12.
Quoted from FormalConjectures/ErdosProblems/123.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/123.
The file states 4 research or textbook statements: 1 open and 3 solved.
Erdos123.erdos_123
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/a28a04b6b8ce43d5260a7466677c1f23833bfc38/src/latest/ErdosProblems/Erdos123.lean.
Let \(a, b, c\) be three integers which are pairwise coprime. Is every large integer the sum of distinct integers of the form \(a^k b^l c^m\) (\(k, l, m ≥ 0\)), none of which divide any other?
Equivalently: is the set \(\{a^k b^l c^m : k, l, m \geq 0\}\) d-complete?
Note: For this not to reduce to the two-integer case, we need the integers to be greater than one and distinct.
The prize of $250 is offered by Erdős in [Er97] and [Er97e] for a 'proof or disproof'.
The main problem was resolved in the affirmative by GPT 5.6 (prompted by Snyder).
This was formalized in Lean by Alexeev.
theorem erdos_123 : ∀ a > 1, ∀ b > 1, ∀ c > 1, PairwiseCoprime a b c →
IsDComplete (↑(powers a) * ↑(powers b) * ↑(powers c))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/123.lean, line 92.
Erdos123.erdos_123.variants.erdos_lewin_3_5_7
Solved: stated here without proof.
Erdős and Lewin [ErLe96] proved this conjecture when \(a = 3\), \(b = 5\), and \(c = 7\).
theorem erdos_123.variants.erdos_lewin_3_5_7 :
IsDComplete (↑(powers 3) * ↑(powers 5) * ↑(powers 7))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/123.lean, line 99.
Erdos123.erdos_123.variants.powers_2_3
Solved: stated here without proof.
A simpler case: the set of numbers of the form \(2^k 3^l\) (\(k, l ≥ 0\)) is d-complete.
This was initially conjectured by Erdős in 1992, who called it a "nice and difficult" problem, but it was quickly proven by Jansen and others using a simple inductive argument: - If \(n = 2m\) is even, apply the inductive hypothesis to \(m\) and double all summands. - If \(n\) is odd, let \(3^k\) be the largest power of \(3\) with \(3^k ≤ n\), and apply the inductive hypothesis to \(n - 3^k\) (which is even).
theorem erdos_123.variants.powers_2_3 : IsDComplete (↑(powers 2) * ↑(powers 3))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/123.lean, line 112.
Erdos123.erdos_123.variants.powers_2_3_5_snug
Open: stated without proof.
In [Er92b] Erdős makes the stronger conjecture (for \(a=2\), \(b=3\), and \(c=5\)) that, for any \(\epsilon>0\), all large integers \(n\) can be written as the sum of distinct integers \(b_1\lt \cdots \lt b_t\) of the form \(2^k3^l5^m\) where \(b_t<(1+\epsilon)b_1\).
theorem erdos_123.variants.powers_2_3_5_snug :
∀ ε > 0, ∀ᶠ n in atTop,
∃ A : Finset ℕ, (A : Set ℕ) ⊆ ↑(powers 2) * ↑(powers 3) * ↑(powers 5) ∧ IsSnug ε A ∧
∑ x ∈ A, x = n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/123.lean, line 120.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.