Erdős Problem 1027 to Erdős Problem 1051
TheoremErdős Problem 1027#
References: - erdosproblems.com/1027 - [Er64e] Erdős, P., On a combinatorial problem. II. Acta Math. Acad. Sci. Hungar. (1964), 445-447. - [Er71] Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109.
Quoted from FormalConjectures/ErdosProblems/1027.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/1027.
The file states 1 research or textbook statement: 1 solved.
Erdos1027.erdos_1027
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1027.lean#L209.
Let \(c>0\), and let \(n\) be sufficiently large depending on \(c\). Suppose that \(\mathcal{F}\) is a family of at most \(c2^n\) many finite sets of size \(n\). Let \(X=\cup_{A\in \mathcal{F}}A\).
Must there exist \(\gg_c 2^{\lvert X\rvert}\) many sets \(B\subset X\) which intersect every set in \(\mathcal{F}\), yet contain none of them?
The existence of a single such \(B\) is equivalent to \(\mathcal{F}\) being \(2\)-chromatic (or having property B), see 901.
This is true, and a proof was given in the comment section by Koishi Chan.
theorem erdos_1027 : ∀ c : ℝ, 0 < c → ∃ δ : ℝ, 0 < δ ∧
∀ᶠ n : ℕ in atTop, ∀ (α : Type) [DecidableEq α] (F : Finset (Finset α)),
(∀ A ∈ F, A.card = n) → (F.card : ℝ) ≤ c * 2 ^ n →
δ * 2 ^ (groundSet F).card ≤ (goodSets F).card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1027.lean, line 62.
Sources
TheoremErdős Problem 1028#
References: - erdosproblems.com/1028 - [Er63d] Erdős, Pál, On combinatorial questions connected with a theorem of Ramsey and van der Waerden. Mat. Lapok (1963), 29-37. - [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. - [ErSp71] Erdős, P. and Spencer, J., Imbalances in \(k\)-colorations. Networks (1971/72), 379-385.
Quoted from FormalConjectures/ErdosProblems/1028.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/1028.
The file states 4 research or textbook statements: 4 solved.
Erdos1028.erdos_1028
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1028.lean.
Let
\[H(n)=\min_f \max_{X\subseteq \{1,\ldots,n\}} \left\lvert \sum_{x\lt y\in X} f(x,y)\right\rvert,\]where \(f\) ranges over all functions \(f:\{1,\ldots,n\}^2\to \{-1,1\}\). Estimate \(H(n)\).
Erdős [Er63d] proved
\[\frac{n}{4}\leq H(n) \ll n^{3/2}.\]Erdős and Spencer [ErSp71] proved that \(H(n)\gg n^{3/2}\).
theorem erdos_1028 :
(fun n => (H n : ℝ)) =Θ[atTop]
fun n : ℕ => (n : ℝ) ^ (3 / 2 : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1028.lean, line 61.
Erdos1028.erdos_1028.variants.lower_bound
Solved: stated here without proof.
Erdős [Er63d] proved
\[\frac{n}{4}\leq H(n) \ll n^{3/2}.\]
theorem erdos_1028.variants.lower_bound :
∀ᶠ n : ℕ in atTop, (n : ℝ) / 4 ≤ (H n : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1028.lean, line 70.
Erdos1028.erdos_1028.variants.upper_bound
Solved: stated here without proof.
Erdős [Er63d] proved
\[\frac{n}{4}\leq H(n) \ll n^{3/2}.\]
theorem erdos_1028.variants.upper_bound :
(fun n => (H n : ℝ)) ≪ (fun n : ℕ => (n : ℝ) ^ (3 / 2 : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1028.lean, line 78.
Erdos1028.erdos_1028.variants.erdos_spencer
Solved: stated here without proof.
Erdős and Spencer [ErSp71] proved that \(H(n)\gg n^{3/2}\).
theorem erdos_1028.variants.erdos_spencer :
(fun n : ℕ => (n : ℝ) ^ (3 / 2 : ℝ)) ≪ (fun n => (H n : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1028.lean, line 84.
Sources
TheoremErdős Problem 1029#
References: - erdosproblems.com/1029 - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350. - [ErSz35] Erdős, P. and Szekeres, G., A combinatorial problem in geometry. Compos. Math. (1935), 463-470. - [Sp75] Spencer, J., Ramsey's theorem - a new lower bound. J. Combin. Theory Ser. A (1975), 108-115.
Quoted from FormalConjectures/ErdosProblems/1029.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/1029.
The file states 1 research or textbook statement: 1 open.
Erdos1029.erdos_1029
Open: stated without proof.
If \(R(k)\) is the Ramsey number for \(K_k\), the minimal \(n\) such that every \(2\)-colouring of the edges of \(K_n\) contains a monochromatic copy of \(K_k\), then
\[\frac{R(k)}{k2^{k/2}}\to \infty.\]In [Er93] Erdős offers $100 for a proof of this and $1000 for a disproof, but says 'this last offer is to some extent phoney: I am sure that this is true (but I have been wrong before).'
theorem erdos_1029 :
Tendsto (fun k : ℕ ↦ (SimpleGraph.diagonalRamsey k : ℝ) /
((k : ℝ) * (2 : ℝ) ^ ((k : ℝ) / 2))) atTop atTop
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1029.lean, line 48.
Sources
TheoremErdős Problem 1030#
References: - erdosproblems.com/1030 - [BEFS89] Burr, S. and Erdős, P. and Faudree, R. J. and Schelp, R. H., On the difference between consecutive Ramsey numbers. Utilitas Math. (1989), 115-118.
Quoted from FormalConjectures/ErdosProblems/1030.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/1030.
The file states 1 research or textbook statement: 1 open.
Erdos1030.erdos_1030
Open: stated without proof.
Let \(R(k,l)\) be the usual Ramsey number: the smallest \(n\) such that if the edges of \(K_n\) are coloured red and blue then there exists either a red \(K_k\) or a blue \(K_l\).
Prove the existence of some \(c>0\) such that
\[\lim_{k\to \infty}\frac{R(k+1,k)}{R(k,k)}> 1+c.\]A problem of Erdős and Sós.
theorem erdos_1030 :
∃ c > (0 : ℝ), ∃ L : ℝ,
Tendsto (fun k : ℕ ↦
(SimpleGraph.classicalRamsey (k + 1) k : ℝ) /
(SimpleGraph.classicalRamsey k k : ℝ)) atTop (nhds L) ∧
L > 1 + c
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1030.lean, line 45.
Sources
TheoremErdős Problem 1032#
References: - erdosproblems.com/1032 - [Er93] Erdős, P., Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. 16 (1993), 333-350. - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999). - [Di52] Dirac, G. A., A property of \(4\)-chromatic graphs and some remarks on critical graphs. J. London Math. Soc. 27 (1952), 85-92. - [Si72] Simonovits, M., On colour-critical graphs. Studia Sci. Math. Hungar. 7 (1972), 67-81. - [To72] Toft, B., Two theorems on critical \(4\)-chromatic graphs. Studia Sci. Math. Hungar. 7 (1972), 83-89. - [Ma15] Markström, K. (ed.), Problem collection from the IML programme: Graphs, Hypergraphs, and Computing. arXiv:1511.00270 (2015). Problem 5.1 (M. Simonovits).
See also erdosproblems.com/917 and erdosproblems.com/944.
Quoted from FormalConjectures/ErdosProblems/1032.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/1032.
The file states 4 research or textbook statements: 2 open and 2 solved.
Erdos1032.erdos_1032
Open: stated without proof.
We say that a graph is \(4\)-chromatic critical if it has chromatic number \(4\), and removing any edge decreases the chromatic number to \(3\).
Is there, for arbitrarily large \(n\), a \(4\)-chromatic critical graph on \(n\) vertices with minimum degree \(\gg n\)?
This is a question of Erdős [Er93, p. 341] (see also [Va99, 3.60]). We read \(\gg n\) as \(\geq cn\) for a fixed constant \(c > 0\).
theorem erdos_1032 :
∃ c : ℝ, 0 < c ∧ ∃ᶠ n : ℕ in atTop,
∃ G : SimpleGraph (Fin n), IsKCritical G 4 ∧ c * (n : ℝ) ≤ (G.minDegree : ℝ)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1032.lean, line 71.
Erdos1032.erdos_1032.variants.five
Open: stated without proof.
Is there, for arbitrarily large \(n\), a \(5\)-chromatic critical graph on \(n\) vertices with minimum degree \(\gg n\)?
This problem is also open for \(5\)-chromatic critical graphs.
theorem erdos_1032.variants.five :
∃ c : ℝ, 0 < c ∧ ∃ᶠ n : ℕ in atTop,
∃ G : SimpleGraph (Fin n), IsKCritical G 5 ∧ c * (n : ℝ) ≤ (G.minDegree : ℝ)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1032.lean, line 84.
Erdos1032.erdos_1032.variants.dirac_six
Solved: stated here without proof.
Dirac gave an example of a \(6\)-chromatic critical graph with minimum degree \(>n/2\).
Dirac's graphs join two disjoint odd cycles of length \(n/2\) [Di52], [Ma15]. Here we state that there are such graphs for infinitely many \(n\).
theorem erdos_1032.variants.dirac_six :
∃ᶠ n : ℕ in atTop,
∃ G : SimpleGraph (Fin n), IsKCritical G 6 ∧ (n : ℝ) / 2 < (G.minDegree : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1032.lean, line 97.
Erdos1032.erdos_1032.variants.simonovits_toft
Solved: stated here without proof.
Simonovits [Si72] and Toft [To72] independently constructed \(4\)-chromatic critical graphs with minimum degree \(\gg n^{1/3}\).
We state this as in [Ma15, Problem 5.1]: there are \(4\)-critical graphs on \(n\) vertices with minimum degree at least \(c n^{1/3}\) for infinitely many \(n\), for a fixed constant \(c > 0\).
theorem erdos_1032.variants.simonovits_toft :
∃ c : ℝ, 0 < c ∧ ∃ᶠ n : ℕ in atTop,
∃ G : SimpleGraph (Fin n),
IsKCritical G 4 ∧ c * (n : ℝ) ^ ((1 : ℝ) / 3) ≤ (G.minDegree : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1032.lean, line 111.
Sources
TheoremErdős Problem 1033#
References: - erdosproblems.com/1033 - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79. - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350. - [ErLa85] Erdős, Paul and Laskar, Renu, A note on the size of a chordal subgraph. Congr. Numer. (1985), 81--86. - [Fa88] Fan, Genghua, Degree sum for a triangle in a graph. J. Graph Theory (1988), 249--263.
Quoted from FormalConjectures/ErdosProblems/1033.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/1033.
The file states 4 research or textbook statements: 4 solved.
Erdos1033.erdos_1033
Solved: stated here without proof.
Let \(h(n)\) be such that every graph on \(n\) vertices with \(>n^2/4\) many edges contains a triangle whose vertices have degrees summing to at least \(h(n)\). Estimate \(h(n)\). In particular, is it true that
\[h(n)\geq (2(\sqrt{3}-1)-o(1))n?\]A conjecture of Bollobás and Erdős.
The answer is no. A blow-up of the butterfly graph, posted on the Erdős problems forum in June and July 2026 and written up in this note, gives arbitrarily large graphs with more than \(n^2/4\) edges in which every triangle has degree sum at most \(1.464n\), which is less than \(2(\sqrt{3}-1)n\). Estimating the optimal value of \(h(n)\) is still open.
theorem erdos_1033 :
¬ ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
n ^ 2 < 4 * #G.edgeFinset →
∃ t, G.IsNClique 3 t ∧
(2 * (Real.sqrt 3 - 1) - ε) * n ≤ ∑ v ∈ t, (G.degree v : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1033.lean, line 56.
Erdos1033.erdos_1033.variants.three_halves
Solved: stated here without proof.
In [Er82e] it is asked whether \(h(n)\geq \frac{3}{2}n\). The answer is no, since the construction of Erdős and Laskar [ErLa85] gives \(h(n) \leq 2(\sqrt{3}-1)n+O(1)\) and \(2(\sqrt{3}-1) < \frac{3}{2}\).
theorem erdos_1033.variants.three_halves :
¬ ∀ n : ℕ, ∀ (G : SimpleGraph (Fin n)) [DecidableRel G.Adj], n ^ 2 < 4 * #G.edgeFinset →
∃ t, G.IsNClique 3 t ∧ 3 * n ≤ 2 * ∑ v ∈ t, G.degree v
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1033.lean, line 69.
Erdos1033.erdos_1033.variants.fan
Solved: stated here without proof.
Fan [Fa88] proved that \(h(n) \geq \frac{21}{16}n\): every graph on \(n\) vertices with \(>n^2/4\) edges contains a triangle whose degrees sum to at least \(\frac{21}{16}n\).
theorem erdos_1033.variants.fan (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
(hG : n ^ 2 < 4 * #G.edgeFinset) :
∃ t, G.IsNClique 3 t ∧ 21 * n ≤ 16 * ∑ v ∈ t, G.degree v
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1033.lean, line 79.
Erdos1033.erdos_1033.variants.erdos_laskar
Solved: stated here without proof.
Erdős and Laskar [ErLa85] gave a construction showing that \(h(n) \leq 2(\sqrt{3}-1)n+O(1)\): for all large \(n\) there is a graph on \(n\) vertices with \(>n^2/4\) edges in which every triangle has degree sum at most \(2(\sqrt{3}-1)n+O(1)\). The construction is made explicit in [Fa88].
theorem erdos_1033.variants.erdos_laskar :
∃ C : ℝ, ∀ᶠ n : ℕ in atTop, ∃ G : SimpleGraph (Fin n), n ^ 2 < 4 * #G.edgeFinset ∧
∀ t, G.IsNClique 3 t → ∑ v ∈ t, (G.degree v : ℝ) ≤ 2 * (Real.sqrt 3 - 1) * n + C
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1033.lean, line 91.
Sources
TheoremErdős Problem 1034#
References: - erdosproblems.com/1034 - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350. - [MaTa25] Ma, Jie and Tang, Quanyu, On Erdős problem #1034. staff.ustc.edu.cn/~jiema/Erdos-1034.pdf
Quoted from FormalConjectures/ErdosProblems/1034.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/1034.
The file states 4 research or textbook statements: 4 solved.
Erdos1034.erdos_1034
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1034.lean.
Let \(G\) be a graph on \(n\) vertices with \(>n^2/4\) many edges. Must there be a triangle \(T\) in \(G\) and vertices \(y_1,\ldots,y_t\), where \(t>(\frac{1}{2}-o(1))n\), such that every \(y_i\) is joined to at least two vertices of \(T\)?
A conjecture of Erdős and Faudree; a stronger version of [905].
This has been solved in the negative by Ma and Tang [MaTa25], who construct a graph with \(n\) vertices and \(>n^2/4\) edges in which every triangle has at most \((2-(5/2)^{1/2}+o(1))n\) vertices adjacent to at least two of its vertices (note that \(2-(5/2)^{1/2}\approx 0.4189\)).
theorem erdos_1034 :
¬ ∀ ε : ℝ, 0 < ε → ∀ᶠ (n : ℕ) in atTop, ∀ G : SimpleGraph (Fin n),
(n : ℝ) ^ 2 / 4 < (G.edgeSet.ncard : ℝ) →
∃ T : Finset (Fin n), G.IsNClique 3 T ∧ ∃ Y : Finset (Fin n),
JoinedToTwo G T Y ∧ (1 / 2 - ε) * (n : ℝ) < (Y.card : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1034.lean, line 57.
Erdos1034.erdos_1034.variants.lower_bound
Solved: stated here without proof.
Erdős and Faudree asked about the threshold \(h(n)\) such that every graph with \(n\) vertices and \(>n^2/4\) edges contained a triangle and \(h(n)\) other vertices which are connected to at least two vertices of the triangle. The fact that every graph with \(>n^2/4\) edges contains a book of size \(n/6\) shows that
\[(1/6-o(1))n \leq h(n).\]
theorem erdos_1034.variants.lower_bound (ε : ℝ) (hε : 0 < ε) :
∀ᶠ (n : ℕ) in atTop, ∀ G : SimpleGraph (Fin n),
(n : ℝ) ^ 2 / 4 < (G.edgeSet.ncard : ℝ) →
∃ T : Finset (Fin n), G.IsNClique 3 T ∧ ∃ Y : Finset (Fin n),
JoinedToTwo G T Y ∧ (1 / 6 - ε) * (n : ℝ) ≤ (Y.card : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1034.lean, line 72.
Erdos1034.erdos_1034.variants.upper_bound
Solved: stated here without proof.
The construction of Ma and Tang [MaTa25] of a graph with \(n\) vertices and \(>n^2/4\) edges in which every triangle has at most \((2-(5/2)^{1/2}+o(1))n\) vertices adjacent to at least two of its vertices shows that, for the threshold \(h(n)\) of
erdos_1034.variants.lower_bound,\[h(n) \leq (2-(5/2)^{1/2}+o(1))n.\]
theorem erdos_1034.variants.upper_bound (ε : ℝ) (hε : 0 < ε) :
∀ᶠ (n : ℕ) in atTop, ∃ G : SimpleGraph (Fin n),
(n : ℝ) ^ 2 / 4 < (G.edgeSet.ncard : ℝ) ∧
∀ T : Finset (Fin n), G.IsNClique 3 T → ∀ Y : Finset (Fin n),
JoinedToTwo G T Y → (Y.card : ℝ) ≤ (2 - Real.sqrt (5 / 2) + ε) * (n : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1034.lean, line 86.
Erdos1034.erdos_1034.variants.k4_free
Solved: stated here without proof.
Erdős suggested that the answer is different if \(G\) has no \(K_4\). In the comments Ma and Tang sketch a proof that the conjecture remains false even if we assume that \(G\) contains no \(K_4\), constructing a graph with \(n\) vertices, \(>n^2/4\) edges, and no \(K_4\), in which every triangle has at most \((2\sqrt{3}-3+o(1))n\) vertices adjacent to at least two of its vertices (note that \(2\sqrt{3}-3\approx 0.464\)).
theorem erdos_1034.variants.k4_free (ε : ℝ) (hε : 0 < ε) :
∀ᶠ (n : ℕ) in atTop, ∃ G : SimpleGraph (Fin n), G.CliqueFree 4 ∧
(n : ℝ) ^ 2 / 4 < (G.edgeSet.ncard : ℝ) ∧
∀ T : Finset (Fin n), G.IsNClique 3 T → ∀ Y : Finset (Fin n),
JoinedToTwo G T Y → (Y.card : ℝ) ≤ (2 * Real.sqrt 3 - 3 + ε) * (n : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1034.lean, line 101.
Sources
TheoremErdős Problem 1035#
References: - erdosproblems.com/1035 - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350.
Quoted from FormalConjectures/ErdosProblems/1035.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/1035.
The file states 1 research or textbook statement: 1 open.
Erdos1035.erdos_1035
Open: stated without proof.
Is there a constant \(c > 0\) such that every graph on \(2^n\) vertices with minimum degree \(> (1-c) \cdot 2^n\) contains the \(n\)-dimensional hypercube \(Q_n\)?
This is Erdős's question [Er93, p. 345].
See also [576] for the extremal number of edges that guarantee a \(Q_n\).
theorem erdos_1035 :
∃ c > 0, ∀ n : ℕ, ∀ (G : SimpleGraph (Fin (2 ^ n))) [DecidableRel G.Adj],
(∀ v, (G.degree v : ℝ) > (1 - c) * 2 ^ n) →
(SimpleGraph.hypercube n).IsContained G
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1035.lean, line 42.
Sources
TheoremErdős Problem 1036#
References: - erdosproblems.com/1036 - [AlHa91] Alon, N. and Hajnal, A., Ramsey graphs contain many distinct induced subgraphs. Graphs Combin. (1991), 1-6. - [ErHa89b] Erdős, P. and Hajnal, A., On the number of distinct induced subgraphs of a graph. Discrete Math. (1989), 145-154. - [Sh98] Shelah, Saharon, Erdős and Rényi conjecture. J. Combin. Theory Ser. A (1998), 179-185.
Quoted from FormalConjectures/ErdosProblems/1036.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/1036.
The file states 3 research or textbook statements: 3 solved.
Erdos1036.erdos_1036
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1036.lean.
Let \(G\) be a graph on \(n\) vertices which does not contain a trivial (empty or complete) graph on more than \(c\log n\) vertices. Must \(G\) contain at least \(2^{\Omega_c(n)}\) many induced subgraphs which are not pairwise isomorphic?
This is true, and was proved by Shelah [Sh98].
theorem erdos_1036 :
∀ c : ℝ, 0 < c → ∃ δ : ℝ, 0 < δ ∧ ∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph (Fin n),
G.IsCRamsey c →
HasManyNonIsomorphicInducedSubgraphs G ((2 : ℝ) ^ (δ * (n : ℝ)))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1036.lean, line 66.
Erdos1036.erdos_1036.variants.alon_hajnal
Solved: stated here without proof.
Alon and Hajnal [AlHa91] proved that \(G\) must contain at least
\[\exp\left(n(\log n)^{-O(\log\log n)}\right)\]many non-isomorphic induced subgraphs.
theorem erdos_1036.variants.alon_hajnal :
∀ c : ℝ, 0 < c → ∃ C : ℝ, 0 < C ∧ ∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph (Fin n),
G.IsCRamsey c →
HasManyNonIsomorphicInducedSubgraphs G
(Real.exp ((n : ℝ) * Real.log (n : ℝ) ^ (-(C * Real.log (Real.log (n : ℝ))))))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1036.lean, line 78.
Erdos1036.erdos_1036.variants.erdos_hajnal
Solved: stated here without proof.
Erdős and Hajnal [ErHa89b] proved that if neither \(G\) nor its complement contains a balanced complete bipartite graph \(K_{k,k}\) on more than \(c\log n\) vertices (as a not necessarily induced subgraph) then \(G\) contains at least \(2^{\Omega_c(n)}\) many non-isomorphic induced subgraphs.
theorem erdos_1036.variants.erdos_hajnal :
∀ c : ℝ, 0 < c → ∃ δ : ℝ, 0 < δ ∧ ∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph (Fin n),
NoLargeBiclique G (c * Real.log (n : ℝ)) →
HasManyNonIsomorphicInducedSubgraphs G ((2 : ℝ) ^ (δ * (n : ℝ)))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1036.lean, line 91.
Sources
TheoremErdős Problem 1037#
References: - erdosproblems.com/1037 - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350.
Quoted from FormalConjectures/ErdosProblems/1037.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/1037.
The file states 2 research or textbook statements: 2 solved.
Erdos1037.erdos_1037
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1037.lean.
Let \(G\) be a graph on \(n\) vertices in which every degree occurs at most twice, and the number of distinct degrees is \(>(\frac{1}{2}+\epsilon)n\). Must \(G\) contain a trivial (empty or complete) subgraph of size 'much larger' than \(\log n\)?
A question of Chen and Erdős.
The answer is no - Cambie, Chan, and Hunter have in the comment section given a simple construction of a graph on \(n\) vertices with at least \(\frac{3}{4}n\) distinct degrees, every degree appears at most twice, and the largest trivial subgraph has size \(O(\log n)\).
theorem erdos_1037 :
¬ ∀ ε : ℝ, 0 < ε → ∀ C : ℝ, ∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph (Fin n),
(∀ d : ℕ, {v : Fin n | (G.neighborSet v).ncard = d}.ncard ≤ 2) →
((1 / 2 + ε) * (n : ℝ) <
((Set.range fun v : Fin n => (G.neighborSet v).ncard).ncard : ℝ)) →
∃ s : Set (Fin n), G.IsHomogeneous s ∧ (C * Real.log (n : ℝ) < (s.ncard : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1037.lean, line 48.
Erdos1037.erdos_1037.variants.cambie_chan_hunter
Solved: stated here without proof.
Cambie, Chan, and Hunter have in the comment section given a simple construction of a graph on \(n\) vertices with at least \(\frac{3}{4}n\) distinct degrees, every degree appears at most twice, and the largest trivial subgraph has size \(O(\log n)\).
theorem erdos_1037.variants.cambie_chan_hunter :
∃ C : ℝ, ∀ᶠ n : ℕ in atTop, ∃ G : SimpleGraph (Fin n),
(∀ d : ℕ, {v : Fin n | (G.neighborSet v).ncard = d}.ncard ≤ 2) ∧
(3 / 4 * (n : ℝ) ≤
((Set.range fun v : Fin n => (G.neighborSet v).ncard).ncard : ℝ)) ∧
∀ s : Set (Fin n), G.IsHomogeneous s → ((s.ncard : ℝ) ≤ C * Real.log (n : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1037.lean, line 62.
Sources
TheoremErdős Problem 1038#
Reference: - erdosproblems.com/1038 - [Tao25] Tao, Terence. Sublevel Sets of Logarithmic Potentials. Terry Tao’s Blog, Dec. 2025 (https://terrytao.wordpress.com/wp-content/uploads/2025/12/erdos-1038-1.pdf) - [EHP58] Erdős, P., Herzog, F., Piranian, G. Metric properties of polynomials. J. Analyse Math. 6 (1958), 125--148.
Quoted from FormalConjectures/ErdosProblems/1038.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/1038.
The file states 9 research or textbook statements: 1 open, 3 solved and 5 textbook results.
Erdos1038.erdos_1038.parts.i
Open: stated without proof.
What is the infimum of
|{x ∈ ℝ : |f x| < 1}|over all nonconstant monic polynomialsfsuch that all of its roots are real and contained in[-1,1]?
theorem erdos_1038.parts.i : erdos_1038.parts.i.answer =
⨅ f : {f : Polynomial ℝ // f.Monic ∧ f ≠ 1 ∧
(f.roots.filter fun x => x ∈ Set.Icc (-1 : ℝ) 1).card = f.natDegree},
volume {x | |f.1.eval x| < 1}
Category research open; AMS 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1038.lean, line 44.
Erdos1038.erdos_1038.parts.ii
Solved: stated here without proof.
The supremum of
|{x ∈ ℝ : |f x| < 1}|over all monic polynomialsfsuch that all of its roots are real and contained in[-1,1]is2 * 2 ^ (1 / 2). This is proved in [Tao25].
theorem erdos_1038.parts.ii : 2 * 2 ^ (1 / 2 : ℝ) =
⨆ f : {f : Polynomial ℝ // f.Monic ∧
(f.roots.filter fun x => x ∈ Set.Icc (-1 : ℝ) 1).card = f.natDegree},
volume {x | |f.1.eval x| < 1}
Category research solved; AMS 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1038.lean, line 54.
Erdos1038.erdos_1038.variants.inf_upperBound
Solved: stated here without proof.
The infimum of
|{x ∈ ℝ : |f x| < 1}|over all nonconstant monic polynomialsfsuch that all of its roots are real and contained in[-1,1]is< 1.835.
theorem erdos_1038.variants.inf_upperBound : ⨅ f : {f : Polynomial ℝ // f.Monic ∧ f ≠ 1 ∧
(f.roots.filter fun x => x ∈ Set.Icc (-1 : ℝ) 1).card = f.natDegree},
volume {x | |f.1.eval x| < 1} < 1.835
Category research solved; AMS 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1038.lean, line 63.
Erdos1038.erdos_1038.variants.inf_lowerBound
Solved: stated here without proof.
The infimum of
|{x ∈ ℝ : |f x| < 1}|over all nonconstant monic polynomialsfsuch that all of its roots are real and contained in[-1,1]is≥ 2 ^ (4 / 3) - 1.
theorem erdos_1038.variants.inf_lowerBound : 2 ^ (4 / 3 : ℝ) - 1 ≤
⨅ f : {f : Polynomial ℝ // f.Monic ∧ f ≠ 1 ∧
(f.roots.filter fun x => x ∈ Set.Icc (-1 : ℝ) 1).card = f.natDegree},
volume {x | |f.1.eval x| < 1}
Category research solved; AMS 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1038.lean, line 71.
Erdos1038.erdos_1038.variants.quadratic_sublevel_formula
Textbook result, proved here.
For a monic quadratic with roots at distance at most two, the sublevel measure is \(2\sqrt{1+d^2}\), where \(2|d|\) is the distance between the roots. This gives the degree-two case of the sublevel-set problem in [Tao25].
theorem erdos_1038.variants.quadratic_sublevel_formula (m d : ℝ) (hd : |d| ≤ 1) :
volume {x : ℝ | |(x - m) ^ 2 - d ^ 2| < 1} =
ENNReal.ofReal (2 * Real.sqrt (1 + d ^ 2))
Category textbook; AMS 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1038.lean, line 82.
Erdos1038.erdos_1038.variants.quadratic_upperBound
Textbook result, proved here.
The degree-two case of the supremum bound in [Tao25]: if \(a,b\in[-1,1]\), the sublevel set of \((x-a)(x-b)\) has measure at most \(2\sqrt{2}\).
theorem erdos_1038.variants.quadratic_upperBound (a b : ℝ) (ha : |a| ≤ 1) (hb : |b| ≤ 1) :
volume {x : ℝ | |(x-a)*(x-b)| < 1} ≤ ENNReal.ofReal (2 * Real.sqrt 2)
Category textbook; AMS 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1038.lean, line 118.
Erdos1038.erdos_1038.variants.quadratic_extremizer
Textbook result, proved here.
The admissible quadratic \(x^2-1\), with roots \(-1\) and \(1\), attains the supremum value \(2\sqrt{2}\) in [Tao25].
theorem erdos_1038.variants.quadratic_extremizer :
volume {x : ℝ | |x ^ 2 - 1| < 1} = ENNReal.ofReal (2 * Real.sqrt 2)
Category textbook; AMS 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1038.lean, line 136.
Erdos1038.erdos_1038.variants.sup_lowerBound
Textbook result, proved here.
The lower half of
erdos_1038.parts.ii: the supremum is at least \(2\sqrt{2}\), because the admissible polynomial \(x^2-1\) has sublevel measure exactly \(2\sqrt{2}\). The matching upper bound is proved in [Tao25].
theorem erdos_1038.variants.sup_lowerBound : 2 * 2 ^ (1 / 2 : ℝ) ≤
⨆ f : {f : Polynomial ℝ // f.Monic ∧
(f.roots.filter fun x => x ∈ Set.Icc (-1 : ℝ) 1).card = f.natDegree},
volume {x | |f.1.eval x| < 1}
Category textbook; AMS 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1038.lean, line 146.
Erdos1038.erdos_1038.variants.inf_lt_two
Textbook result, proved here.
The infimum in
erdos_1038.parts.iis strictly less than \(2\), as observed in [EHP58]: for \(f(x)=(x+1)(x-1)^3\) the sublevel set \(\{x : |f(x)| < 1\}\) is contained in \((-1.108,-0.835)\cup(0,1.718)\), whose total length is \(1.991\).
theorem erdos_1038.variants.inf_lt_two : ⨅ f : {f : Polynomial ℝ // f.Monic ∧ f ≠ 1 ∧
(f.roots.filter fun x => x ∈ Set.Icc (-1 : ℝ) 1).card = f.natDegree},
volume {x | |f.1.eval x| < 1} < 2
Category textbook; AMS 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1038.lean, line 164.
Sources
TheoremErdős Problem 1041#
Reference: erdosproblems.com/1041
Quoted from FormalConjectures/ErdosProblems/1041.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/1041.
The file states 2 research or textbook statements: 2 solved.
Erdos1041.exists_connected_component_contains_two_roots
Solved: stated here without proof.
Erdős–Herzog–Piranian Component Lemma (Metric Properties of Polynomials, 1958): If \(f\) is a monic degree \(n\) polynomial with all roots in the unit disk, then some connected component of \(\{z \mid |f(z)| < 1\}\) contains at least two roots with multiplicity.
See p. 139, above Problem 5: [EHP58] Erdős, P. and Herzog, F. and Piranian, G., Metric properties of polynomials. J. Analyse Math. (1958), 125-148.
theorem exists_connected_component_contains_two_roots :
∃ C, C ⊆ {z | ‖f.eval z‖ < 1} ∧ IsConnected C ∧
2 ≤ (f.roots.filter (· ∈ C)).card
Category research solved; AMS 32 Several complex variables and analytic spaces. Declared in FormalConjectures/ErdosProblems/1041.lean, line 57.
Erdos1041.erdos_1041
Solved: stated here; a Lean proof is at https://github.com/wcook04/plectis-erdos-lean/blob/587c48f213106c20ba2cdf3d585700c1394fc44f/verification/FC1041HausdorffCounterexample/lean/ErdosProblems/Erdos1041/Counterexample/HausdorffLength.lean#L449-L454.
Let
\[ f(z) = \prod_{i=1}^{n} (z - z_i) \in \mathbb{C}[x] \]with \(|z_i| < 1\) for all \(i\).
Conjecture: Must there always exist a path of length less than 2 in
\[ \{ z \in \mathbb{C} \mid |f(z)| < 1 \} \]which connects two of the roots of \(f\)?
The answer is negative. ani gave a counterexample of degree seven on the Erdős problems forum on 7 September 2026. The linked formalisation proves, for the member \(s = 10^{-6}\) of ani's family, that every connected subset of \(\{ z \mid |f(z)| < 1 \}\) containing two distinct roots has one-dimensional Hausdorff measure greater than \(2\).
theorem erdos_1041 :
¬ ∀ (n : ℕ) (f : ℂ[X]), n ≥ 2 → f.natDegree = n → f.Monic →
f.rootSet ℂ ⊆ Metric.ball 0 1 →
∃ (z₁ z₂ : ℂ) (h : ({z₁, z₂} : Multiset ℂ) ≤ f.roots) (γ : Path z₁ z₂),
Set.range γ ⊆ { z : ℂ | ‖f.eval z‖ < 1 } ∧ length (Set.range γ) < 2
Category research solved; AMS 32 Several complex variables and analytic spaces. Declared in FormalConjectures/ErdosProblems/1041.lean, line 82.
Sources
TheoremErdős Problem 1043#
References: - erdosproblems.com/1043 - [EHP58] Erdős, P. and Herzog, F. and Piranian, G., Metric properties of polynomials. J. Analyse Math. (1958), 125-148. - [Po59] Pommerenke, Ch., On some problems by Erdős, Herzog and Piranian. Michigan Math. J. (1959), 221-225. - [Po61] Pommerenke, Ch., On metric properties of complex polynomials. Michigan Math. J. (1961), 97-115.
Quoted from FormalConjectures/ErdosProblems/1043.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/1043.
The file states 2 research or textbook statements: 2 solved.
Erdos1043.erdos_1043
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1043.lean.
Erdős Problem 1043: Let \(f\in \mathbb{C}[x]\) be a monic polynomial. Must there exist a straight line \(\ell\) such that the projection of
\[\{ z: \lvert f(z)\rvert\leq 1\}\]onto \(\ell\) has measure at most \(2\)?
Pommerenke [Po61] proved that the answer is no.
The projection onto the line \(\ell = \mathbb{R} u\) is measured with the Lebesgue measure of that line, so
volumeof the projected set is its length.This was formalized in Lean by Alexeev using Aristotle.
theorem erdos_1043 :
¬ ∀ (f : ℂ[X]), f.Monic → f.degree ≥ 1 →
∃ (u : ℂ), ‖u‖ = 1 ∧
volume ((ℝ ∙ u).orthogonalProjectionOnto '' levelSet f) ≤ 2
Category research solved; AMS 28 Measure and integration, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1043.lean, line 60.
Erdos1043.erdos_1043.variants.weak
Solved: stated here without proof.
On the other hand, Pommerenke also proved there always exists a line such that the projection has measure at most 3.3.
theorem erdos_1043.variants.weak :
∀ (f : ℂ[X]), f.Monic → f.degree ≥ 1 →
∃ (u : ℂ), ‖u‖ = 1 ∧
volume ((ℝ ∙ u).orthogonalProjectionOnto '' levelSet f) ≤ 3.3
Category research solved; AMS 28 Measure and integration, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1043.lean, line 71.
Sources
TheoremErdős Problem 1044#
References: - erdosproblems.com/1044 - [EHP58] Erdős, P. and Herzog, F. and Piranian, G., Metric properties of polynomials. J. Analyse Math. (1958), 125-148. - [Ta26] Tang, Quanyu, On Erdős Problem 1044 (2026), github.com/QuanyuTang/erdos-problem-1044.
Quoted from FormalConjectures/ErdosProblems/1044.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/1044.
The file states 4 research or textbook statements: 1 open and 3 solved.
Erdos1044.erdos_1044
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1044.lean.
Let \(f(z)=\prod_{i=1}^n(z-z_i)\in\mathbb{C}[x]\) where \(\lvert z_i\rvert\leq 1\) for all \(i\). If \(\Lambda(f)\) is the maximum of the lengths of the boundaries of the connected components of
\[ \{ z: \lvert f(z)\rvert<1\} \]then determine the infimum of \(\Lambda(f)\).
A problem of Erdős, Herzog, and Piranian [EHP58].
This has been resolved by Tang, who proved that the infimum of \(\Lambda(f)\) over all such \(f\) is \(2\).
theorem erdos_1044 :
IsGLB {L : ℝ≥0∞ | ∃ f : ℂ[X], IsAdmissible f ∧ maxBoundaryLength f = L} erdos_1044.answer
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1044.lean, line 71.
Erdos1044.erdos_1044.variants.infimum_eq_two
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1044.lean.
This has been resolved by Tang, who proved that the infimum of \(\Lambda(f)\) over all such \(f\) is \(2\).
theorem erdos_1044.variants.infimum_eq_two :
IsGLB {L : ℝ≥0∞ | ∃ f : ℂ[X], IsAdmissible f ∧ maxBoundaryLength f = L} 2
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1044.lean, line 81.
Erdos1044.erdos_1044.variants.fixed_degree
Open: stated without proof.
Tang also suggests that, if the degree \(n\) is fixed, then the infimum over all such \(f\) of degree \(n\) is attained by \(f_n(z)=z^n-1\).
theorem erdos_1044.variants.fixed_degree (n : ℕ) (hn : 0 < n) :
IsLeast {L : ℝ≥0∞ | ∃ f : ℂ[X], IsAdmissible f ∧ f.natDegree = n ∧ maxBoundaryLength f = L}
(maxBoundaryLength (X ^ n - 1))
Category research open; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1044.lean, line 90.
Erdos1044.erdos_1044.variants.fixed_degree_of_le_two
Solved: stated here without proof.
Tang also suggests that, if the degree \(n\) is fixed, then the infimum over all such \(f\) of degree \(n\) is attained by \(f_n(z)=z^n-1\) (and proves this for \(n=1\) and \(n=2\)).
theorem erdos_1044.variants.fixed_degree_of_le_two (n : ℕ) (hn : n = 1 ∨ n = 2) :
IsLeast {L : ℝ≥0∞ | ∃ f : ℂ[X], IsAdmissible f ∧ f.natDegree = n ∧ maxBoundaryLength f = L}
(maxBoundaryLength (X ^ n - 1))
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1044.lean, line 100.
Sources
TheoremErdős Problem 1046#
References: - erdosproblems.com/1046 - [EHP58] Erdős, P. and Herzog, F. and Piranian, G., Metric properties of polynomials. J. Analyse Math. (1958), 125-148. - [Po59] Pommerenke, Ch., On some problems by Erdős, Herzog and Piranian. Michigan Math. J. (1959), 221-225. - [BPS02] Barnard, Roger W. and Pearce, Kent and Solynin, Alexander Yu., An isoperimetric inequality for logarithmic capacity. Ann. Acad. Sci. Fenn. Math. (2002), 419-436. - [Po28] Pólya, G., Beitrag zur Verallgemeinerung des Verzerrungssatzes auf mehrfach zusammenhängende Gebiete. S.-B. Preuss. Akad. Wiss. (1928), 280-282. - [Ra95] Ransford, Thomas, Potential theory in the complex plane. London Mathematical Society Student Texts 28, Cambridge University Press (1995).
Quoted from FormalConjectures/ErdosProblems/1046.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/1046.
The file states 3 research or textbook statements: 3 solved.
Erdos1046.erdos_1046
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1046.lean#L329.
Let \(f\in \mathbb{C}[x]\) be a monic polynomial and
\[E=\{ z: \lvert f(z)\rvert <1\}.\]If \(E\) is connected then is \(E\) contained in a disc of radius \(2\)?
A problem of Erdős, Herzog, and Piranian [EHP58], who also ask, if \(\{ z: \lvert f(z)\rvert\leq 1\}\) is connected, then what are the least possible diameter and greatest possible width of this set, and conjecture the answer is \(2\) in both cases. Their guess that the width is always at most \(2\) is false, as Pommerenke [Po59] gave an example with width \(>\sqrt{3}2^{1/3}\approx 2.18\).
The condition that \(E\) is connected is equivalent to \(E\) containing all zeros of \(f'\).
The answer is yes, and in fact the centre of this disc can be taken to be \(\frac{z_1+\cdots+z_n}{n}\), where the \(z_i\) are the roots of \(f\), as shown by Pommerenke [Po59].
theorem erdos_1046 : ∀ f : ℂ[X], f.Monic → IsConnected (lemniscate f) →
∃ c : ℂ, lemniscate f ⊆ ball c 2
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1046.lean, line 68.
Erdos1046.erdos_1046.variants.centroid
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1046.lean#L321.
Pommerenke [Po59] showed that the centre of the disc can be taken to be the centroid \(\frac{z_1+\cdots+z_n}{n}\) of the roots \(z_i\) of \(f\).
theorem erdos_1046.variants.centroid : ∀ f : ℂ[X], f.Monic → IsConnected (lemniscate f) →
lemniscate f ⊆ ball (f.roots.sum / f.natDegree) 2
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1046.lean, line 79.
Erdos1046.erdos_1046.variants.diameter
Solved: stated here without proof.
Erdős, Herzog, and Piranian [EHP58] conjecture that if \(\{ z: \lvert f(z)\rvert\leq 1\}\) is connected then its diameter is at least \(2\).
The answer is yes, and connectedness is not needed. For monic \(f\) of degree \(n \geq 1\) the set \(\{ z: \lvert f(z)\rvert\leq 1\}\) has logarithmic capacity \(1\) [Ra95, Theorem 5.2.5], and Pólya [Po28] proved \(\mathrm{cap}(E) \leq \frac{1}{2}\operatorname{diam}(E)\) for every compact \(E \subseteq \mathbb{C}\), see [BPS02, (1.2)]. Hence the diameter is at least \(2\).
theorem erdos_1046.variants.diameter : ∀ f : ℂ[X], f.Monic →
IsConnected (closedLemniscate f) → 2 ≤ Metric.ediam (closedLemniscate f)
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1046.lean, line 93.
Sources
TheoremErdős Problem 1047#
References: - erdosproblems.com/1047 - [EHP58] Erdős, P. and Herzog, F. and Piranian, G., Metric properties of polynomials. J. Analyse Math. (1958), 125-148. - [Go66] Goodman, A. W., On the convexity of the level curves of a polynomial. Proc. Amer. Math. Soc. (1966), 358-361. - [Po61] Pommerenke, Ch., On metric properties of complex polynomials. Michigan Math. J. (1961), 97-115.
Quoted from FormalConjectures/ErdosProblems/1047.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/1047.
The file states 6 research or textbook statements: 6 solved.
Erdos1047.erdos_1047
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/latest/ErdosProblems/Erdos1047.lean.
Let \(f\in \mathbb{C}[x]\) be a monic polynomial with \(m\) distinct roots, and let \(c>0\) be a constant small enough such that \(\{ z: \lvert f(z)\rvert\leq c\}\) has \(m\) distinct connected components.
Must all these components be convex?
A question of Grunsky, which was reported by Erdős, Herzog, and Piranian [EHP58].
The answer is no, as shown by Pommerenke [Po61], who showed that, if \(k\) is sufficiently large, and \(f(z)=z^k(z-a)\) where \(a\) is sufficiently close to \((1+\frac{1}{k})k^{\frac{1}{k+1}}\), then \(\{ z: \lvert f(z)\rvert\leq 1\}\) has two components, and the component which contains \(0\) is not convex.
This was formalized in Lean by Alexeev using Aristotle.
theorem erdos_1047 :
¬ ∀ (f : ℂ[X]) (m : ℕ) (c : ℝ), f.Monic → (f.rootSet ℂ).ncard = m → 0 < c →
(componentsIn (sublevelSet f c)).ncard = m →
∀ t ∈ componentsIn (sublevelSet f c), Convex ℝ t
Category research solved; AMS 30 Functions of a complex variable, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1047.lean, line 68.
Erdos1047.erdos_1047.variants.pommerenke
Solved: stated here without proof.
The answer is no, as shown by Pommerenke [Po61], who showed that, if \(k\) is sufficiently large, and \(f(z)=z^k(z-a)\) where \(a\) is sufficiently close to \((1+\frac{1}{k})k^{\frac{1}{k+1}}\), then \(\{ z: \lvert f(z)\rvert\leq 1\}\) has two components, and the component which contains \(0\) is not convex.
theorem erdos_1047.variants.pommerenke :
∀ᶠ k : ℕ in Filter.atTop, ∃ δ : ℝ, 0 < δ ∧ ∀ a : ℝ,
(1 + 1 / (k : ℝ)) * (k : ℝ) ^ ((1 : ℝ) / ((k : ℝ) + 1)) < a →
a < (1 + 1 / (k : ℝ)) * (k : ℝ) ^ ((1 : ℝ) / ((k : ℝ) + 1)) + δ →
(componentsIn (sublevelSet (X ^ k * (X - C (a : ℂ))) 1)).ncard = 2 ∧
¬ Convex ℝ (connectedComponentIn (sublevelSet (X ^ k * (X - C (a : ℂ))) 1) 0)
Category research solved; AMS 30 Functions of a complex variable, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1047.lean, line 81.
Erdos1047.erdos_1047.variants.goodman
Solved: stated here without proof.
Goodman [Go66] proved that one of the three components of
\[\{ z: \lvert (z^2+1)(z-2)^2\rvert < 5^{3/2}/4\}\]is not convex.
theorem erdos_1047.variants.goodman :
(componentsIn (strictSublevelSet ((X ^ 2 + 1) * (X - C 2) ^ 2)
((5 : ℝ) ^ ((3 : ℝ) / 2) / 4))).ncard = 3 ∧
∃ t ∈ componentsIn (strictSublevelSet ((X ^ 2 + 1) * (X - C 2) ^ 2)
((5 : ℝ) ^ ((3 : ℝ) / 2) / 4)), ¬ Convex ℝ t
Category research solved; AMS 30 Functions of a complex variable, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1047.lean, line 95.
Erdos1047.erdos_1047.variants.goodman_simple_roots
Solved: stated here without proof.
Goodman [Go66] constructed an example with simple roots, of degree \(4\).
theorem erdos_1047.variants.goodman_simple_roots :
∃ (f : ℂ[X]) (c : ℝ), f.Monic ∧ f.natDegree = 4 ∧ (f.rootSet ℂ).ncard = 4 ∧ 0 < c ∧
(componentsIn (sublevelSet f c)).ncard = 4 ∧
∃ t ∈ componentsIn (sublevelSet f c), ¬ Convex ℝ t
Category research solved; AMS 30 Functions of a complex variable, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1047.lean, line 106.
Erdos1047.erdos_1047.variants.referee
Solved: stated here without proof.
The referee of the paper [Go66] also gave the example of \(\lvert z(z^5-1)\rvert< 5\cdot 6^{-6/5}\).
theorem erdos_1047.variants.referee :
(componentsIn (strictSublevelSet (X * (X ^ 5 - 1))
(5 * (6 : ℝ) ^ (-(6 : ℝ) / 5)))).ncard = 6 ∧
∃ t ∈ componentsIn (strictSublevelSet (X * (X ^ 5 - 1))
(5 * (6 : ℝ) ^ (-(6 : ℝ) / 5))), ¬ Convex ℝ t
Category research solved; AMS 30 Functions of a complex variable, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1047.lean, line 116.
Erdos1047.erdos_1047.variants.max_non_convex_components
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-1047-max-nonconvex-components/blob/87cc8666968b8228778fae5c5e54465128a864f6/lean/Erdos1047MaxNonConvexFC.lean#L31160-L31164.
Goodman raises the question of the maximum number of non-convex components of \(\{ z: \lvert f(z)\rvert < c\}\) that are possible as a function of the degree of \(f\), where \(f\) ranges over all monic polynomials of degree \(n\) and \(c\) over all positive constants.
The maximum is \(0\) for \(n \le 1\), \(1\) for \(n = 2\), \(2\) for \(n = 3\), and \(n\) for \(n \ge 4\).
theorem erdos_1047.variants.max_non_convex_components (n : ℕ) :
IsGreatest {k : ℕ | ∃ (f : ℂ[X]) (c : ℝ), f.Monic ∧ f.natDegree = n ∧ 0 < c ∧
{t ∈ componentsIn (strictSublevelSet f c) | ¬ Convex ℝ t}.ncard = k}
(erdos_1047.variants.max_non_convex_components.answer n)
Category research solved; AMS 30 Functions of a complex variable, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1047.lean, line 136.
Sources
TheoremErdős Problem 1048#
References: - erdosproblems.com/1048 - [EHP58] Erdős, P. and Herzog, F. and Piranian, G., Metric properties of polynomials. J. Analyse Math. (1958), 125-148. - [Po61] Pommerenke, Ch., On metric properties of complex polynomials. Michigan Math. J. (1961), 97-115.
Quoted from FormalConjectures/ErdosProblems/1048.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/1048.
The file states 8 research or textbook statements: 8 solved.
Erdos1048.erdos_1048
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1048.lean.
If \(f\in \mathbb{C}[x]\) is a monic polynomial with all roots satisfying \(\lvert z\rvert \leq r\) for some \(0 < r < 2\), then must
\[\{ z: \lvert f(z)\rvert <1\}\]have a connected component with diameter \(>2-r\)?
A problem of Erdős, Herzog, and Piranian [EHP58].
Pommerenke [Po61] proved the answer is no for \(r>1\), showing that if \(f(z)=z^n-r^n\) then \(\{ z: \lvert f(z)\rvert \leq 1\}\) has \(n\) connected components, all with diameter \(\to 0\) as \(n\to \infty\).
theorem erdos_1048 :
¬ ∀ (r : ℝ) (f : ℂ[X]), 0 < r → r < 2 → f.Monic → f.degree ≥ 1 → (∀ z ∈ f.roots, ‖z‖ ≤ r) →
∃ z ∈ openLevelSet f, ENNReal.ofReal (2 - r) <
Metric.ediam (connectedComponentIn (openLevelSet f) z)
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1048.lean, line 56.
Erdos1048.erdos_1048.variants.pommerenke_ncard_components
Solved: stated here without proof.
Pommerenke [Po61] proved the answer is no for \(r>1\), showing that if \(f(z)=z^n-r^n\) then \(\{ z: \lvert f(z)\rvert \leq 1\}\) has \(n\) connected components, all with diameter \(\to 0\) as \(n\to \infty\).
theorem erdos_1048.variants.pommerenke_ncard_components (r : ℝ) (hr : 1 < r) (n : ℕ) (hn : 1 ≤ n)
(f : ℂ[X]) (hf : f = (X : ℂ[X]) ^ n - C ((r : ℂ) ^ n)) :
{C : Set ℂ | ∃ z ∈ levelSet f, C = connectedComponentIn (levelSet f) z}.ncard = n
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1048.lean, line 68.
Erdos1048.erdos_1048.variants.pommerenke_diam_tendsto_zero
Solved: stated here without proof.
Pommerenke [Po61] proved the answer is no for \(r>1\), showing that if \(f(z)=z^n-r^n\) then \(\{ z: \lvert f(z)\rvert \leq 1\}\) has \(n\) connected components, all with diameter \(\to 0\) as \(n\to \infty\).
theorem erdos_1048.variants.pommerenke_diam_tendsto_zero (r : ℝ) (hr : 1 < r) (ε : ℝ)
(hε : 0 < ε) :
∀ᶠ n : ℕ in Filter.atTop, ∀ f : ℂ[X], f = (X : ℂ[X]) ^ n - C ((r : ℂ) ^ n) →
∀ z ∈ levelSet f,
Metric.ediam (connectedComponentIn (levelSet f) z) < ENNReal.ofReal ε
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1048.lean, line 79.
Erdos1048.erdos_1048.variants.r_le_one
Solved: stated here without proof.
On the other hand, if \(0\lt r\leq 1\), then the answer is yes, as also shown by Pommerenke [Po61].
theorem erdos_1048.variants.r_le_one (r : ℝ) (hr₀ : 0 < r) (hr₁ : r ≤ 1) (f : ℂ[X])
(hmonic : f.Monic) (hdeg : f.degree ≥ 1) (hroots : ∀ z ∈ f.roots, ‖z‖ ≤ r) :
∃ z ∈ openLevelSet f, ENNReal.ofReal (2 - r) <
Metric.ediam (connectedComponentIn (openLevelSet f) z)
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1048.lean, line 90.
Erdos1048.erdos_1048.variants.diam_ge_two
Solved: stated here without proof.
If \(0\leq r\leq 1/2\) then the component which contains \(0\) must have diameter \(\geq 2\), which \(f(z)=z^n\) shows is best possible.
theorem erdos_1048.variants.diam_ge_two (r : ℝ) (hr₀ : 0 ≤ r) (hr₁ : r ≤ 1 / 2) (f : ℂ[X])
(hmonic : f.Monic) (hdeg : f.degree ≥ 1) (hroots : ∀ z ∈ f.roots, ‖z‖ ≤ r) :
2 ≤ Metric.ediam (connectedComponentIn (levelSet f) 0)
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1048.lean, line 101.
Erdos1048.erdos_1048.variants.diam_ge_two_is_best
Solved: stated here without proof.
If \(0\leq r\leq 1/2\) then the component which contains \(0\) must have diameter \(\geq 2\), which \(f(z)=z^n\) shows is best possible.
theorem erdos_1048.variants.diam_ge_two_is_best (n : ℕ) (hn : 1 ≤ n) :
Metric.ediam (connectedComponentIn (levelSet ((X : ℂ[X]) ^ n)) 0) = 2
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1048.lean, line 111.
Erdos1048.erdos_1048.variants.diam_gt_inv_r
Solved: stated here without proof.
If \(1/2\lt r\leq \frac{\sqrt{5}-1}{2}\) then the component which contains \(0\) must have diameter \(>1/r\).
theorem erdos_1048.variants.diam_gt_inv_r (r : ℝ) (hr₀ : 1 / 2 < r)
(hr₁ : r ≤ (Real.sqrt 5 - 1) / 2) (f : ℂ[X]) (hmonic : f.Monic) (hdeg : f.degree ≥ 1)
(hroots : ∀ z ∈ f.roots, ‖z‖ ≤ r) :
ENNReal.ofReal (1 / r) < Metric.ediam (connectedComponentIn (levelSet f) 0)
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1048.lean, line 120.
Erdos1048.erdos_1048.variants.diam_gt_two_sub_sq
Solved: stated here without proof.
If \(\frac{\sqrt{5}-1}{2}\leq r\leq 1\) then the component which contains \(0\) must have diameter \(>2-r^2\).
theorem erdos_1048.variants.diam_gt_two_sub_sq (r : ℝ) (hr₀ : (Real.sqrt 5 - 1) / 2 ≤ r)
(hr₁ : r ≤ 1) (f : ℂ[X]) (hmonic : f.Monic) (hdeg : f.degree ≥ 1)
(hroots : ∀ z ∈ f.roots, ‖z‖ ≤ r) :
ENNReal.ofReal (2 - r ^ 2) < Metric.ediam (connectedComponentIn (levelSet f) 0)
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1048.lean, line 131.
Sources
TheoremErdős Problem 1049#
References: - erdosproblems.com/1049 - [Er48] Erdős, P., On arithmetical properties of Lambert series. J. Indian Math. Soc. (N.S.) (1948), 63-66.
Quoted from FormalConjectures/ErdosProblems/1049.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/1049.
The file states 3 research or textbook statements: 1 open, 1 solved and 1 textbook result.
Erdos1049.erdos_1049
Open: stated without proof.
Let \(t>1\) be a rational number. Is \(\sum_{n=1}^\infty\frac{1}{t^n-1}=\sum_{n=1}^\infty \frac{\tau(n)}{t^n}\) irrational, where \(\tau(n)\) counts the divisors of \(n\)?
A conjecture of Chowla.
theorem erdos_1049 :
∀ t : ℚ, t > 1 → Irrational (∑' n : ℕ+, 1 / ((t : ℝ) ^ (n : ℕ) - 1))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1049.lean, line 43.
Erdos1049.erdos_1049.variants.geq_2_integer
Solved: stated here; a Lean proof is at https://github.com/wcook04/plectis-erdos-lean/blob/c4eab2571b4692ee9c08d3ec138176f7fbfa09a9/verification/FCMergedIntegerAdapters/research/adapters/FormalConjecturesAdapter.lean#L96-L107.
Erdős [Er48] proved that this is true if \(t\geq 2\) is an integer.
theorem erdos_1049.variants.geq_2_integer :
∀ t : ℤ, t ≥ 2 → Irrational (∑' n : ℕ+, 1 / ((t : ℝ) ^ (n : ℕ) - 1))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1049.lean, line 53.
Erdos1049.lambert_series_eq_num_divisor_sum
Textbook result, proved here.
The classical Lambert series identity: \(\sum_{n=1}^\infty \frac{1}{t^n - 1} = \sum_{n=1}^\infty \frac{\tau(n)}{t^n}\), where \(\tau(n)\) counts the divisors of \(n\).
theorem lambert_series_eq_num_divisor_sum : ∀ t : ℚ,
∑' n : ℕ+, 1 / ((t : ℝ) ^ (n : ℕ) - 1) =
∑' n : ℕ+, (n : ℕ).divisors.card / ((t : ℝ) ^ (n : ℕ))
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1049.lean, line 250.
Sources
TheoremErdős Problem 1050#
References: - erdosproblems.com/1050 - [Bo91] Borwein, Peter B., On the irrationality of {\(\sum(1/(q^n+r))\)}. J. Number Theory (1991), 253--259. - [Bo92] Borwein, Peter B., On the irrationality of certain series. Math. Proc. Camb. Phil. Soc. (1992), 141--146. - [Er48] Erdős, P., On arithmetical properties of Lambert series. J. Indian Math. Soc. (N.S.) (1948), 63-66. - [Er88c] Erdős, P., On the irrationality of certain series: problems and results. New advances in transcendence theory (Durham, 1986) (1988), 102-109.
Is \(\sum_{n=1}^\infty \frac{1}{2^n - 3}\) irrational?
The answer is yes, proved by P. B. Borwein [Bo91] (with a cleaner self-contained proof in [Bo92]), specialized to \(q = 2\), \(r = -3\).
A formal Lean proof is given in an external repository,
gotrevor/lean-gallery, formalized by Trevor Morris with Claude Code and Harmonic's Aristotle.
Quoted from FormalConjectures/ErdosProblems/1050.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/1050.
The file states 4 research or textbook statements: 1 open and 3 solved.
Erdos1050.erdos_1050
Solved: stated here; a Lean proof is at https://github.com/gotrevor/lean-gallery/blob/main/LeanGallery/NumberTheory/Erdos1050/Statement.lean.
Erdős Problem 1050. The series \(\sum_{n=1}^\infty \frac{1}{2^n - 3}\) is irrational.
The source sum runs over \(n \ge 1\); as a
tsumoverℕ(which starts at \(0\)) it is reindexed \(n \mapsto n + 1\), i.e. \(\sum_{n=0}^\infty 1/(2^{n+1} - 3)\).
theorem erdos_1050 : Irrational (∑' n : ℕ, (1 : ℝ) / ((2 : ℝ) ^ (n + 1) - 3))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1050.lean, line 52.
Erdos1050.erdos_1050.variants.two_pow_sub_one
Solved: stated here; a Lean proof is at https://github.com/gotrevor/lean-gallery/blob/main/LeanGallery/NumberTheory/Erdos1050/Variants.lean.
Erdős Problem 1050, variant [Er48]. Erdős proved that the related series \(\sum_{n=1}^\infty \frac{1}{2^n - 1}\) (which equals the Lambert series \(\sum_n \frac{\tau(n)}{2^n}\), where \(\tau\) is the divisor function) is irrational. This is the \(q = 2\), \(r = -1\) case of Borwein's general theorem
Erdos1050.erdos_1050.variants.borweinbelow.
theorem erdos_1050.variants.two_pow_sub_one :
Irrational (∑' n : ℕ, (1 : ℝ) / ((2 : ℝ) ^ (n + 1) - 1))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1050.lean, line 63.
Erdos1050.erdos_1050.variants.borwein
Solved: stated here; a Lean proof is at https://github.com/gotrevor/lean-gallery/blob/main/LeanGallery/NumberTheory/Erdos1050/Variants.lean.
Erdős Problem 1050, variant [Bo91]. Borwein's general theorem: for every integer \(q \ge 2\) and rational \(r \ne 0\) with \(r \ne -q^n\) for all \(n \ge 1\), the series \(\sum_{n=1}^\infty \frac{1}{q^n + r}\) is irrational. Problem 1050 is the case \(q = 2\), \(r = -3\); the [Er48] variant is \(q = 2\), \(r = -1\).
theorem erdos_1050.variants.borwein (q : ℤ) (hq : 2 ≤ q) (r : ℚ) (hr : r ≠ 0)
(hne : ∀ n : ℕ, 1 ≤ n → r ≠ -((q : ℚ) ^ n)) :
Irrational (∑' n : ℕ, (1 : ℝ) / ((q : ℝ) ^ (n + 1) + (r : ℝ)))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1050.lean, line 74.
Erdos1050.erdos_1050.variants.transcendental
Open: stated without proof.
Erdős Problem 1050, variant [Er88c] (open). Erdős conjectured that \(\sum_{n=1}^\infty \frac{1}{2^n + t}\) is transcendental for every integer \(t \ne 0\) — strictly stronger than the irrationality established by Borwein [Bo91]. This remains open.
Two exclusions make the series well-posed and the claim non-vacuous, exactly as in Borwein's theorem: \(t \ne -2^n\) for all \(n \ge 1\) (so no denominator vanishes), and \(t \ne 0\) (at \(t = 0\) the series is the rational \(\sum_{n \ge 1} 2^{-n} = 1\), hence not transcendental).
theorem erdos_1050.variants.transcendental :
∀ t : ℤ, t ≠ 0 → (∀ n : ℕ, 1 ≤ n → t ≠ -(2 : ℤ) ^ n) →
Transcendental ℚ (∑' n : ℕ, (1 : ℝ) / ((2 : ℝ) ^ (n + 1) + (t : ℝ)))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1050.lean, line 87.
Sources
TheoremErdős Problem 1051#
References: - erdosproblems.com/1051 - [BKKKZ26] K. Barreto, J. Kang, S.-H. Kim, V. Kovač, and S. Zhang, Irrationality of rapidly converging series: a problem of Erdős and Graham. arXiv:2601.21442 (2026). - [Er88c] Erdős, P., On the irrationality of certain series: problems and results. New advances in transcendence theory (Durham, 1986) (1988), 102-109. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Fe26] T. Feng et al, Semi-Autonomous Mathematics Discovery with Gemini: A Case Study on the Erdős Problems. arXiv:2601.22401 (2026).
Quoted from FormalConjectures/ErdosProblems/1051.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/1051.
The file states 2 research or textbook statements: 2 solved.
Erdos1051.erdos_1051
Solved: stated here; a Lean proof is at https://www.erdosproblems.com/forum/thread/1051.
Is it true that if \(a_0 < a_1 < a_2 < \cdots\) is a strictly increasing sequence of integers with \(\liminf a_n^{1/2^n} > 1\), then the series \(\sum_{n=0}^\infty \frac{1}{a_n \cdot a_{n+1}}\) is irrational?
This was solved in the affirmative by Aletheia [Fe26]. This was extended by Barreto, Kang, Kim, Kovač, and Zhang [BKKKZ26], who essentially give a complete answer: if \(\phi=\frac{1+\sqrt{5}}{2}\) is the golden ratio and \(1\leq a_1 < a_2 < \cdots\) is a monotonically increasing sequence of integers such that \(\limsup a_n^{1/\phi^{n}}=\infty\) then \(\sum_{n=1}^\infty \frac{1}{a_na_{n+1}}\) is irrational. Conversely, for any \(1 < C < \infty\) there exists a sequence of integers \(1\leq a_1\lt \cdots\) such that \(\lim a_n^{1/\phi^{n}}=C\) where this infinite sum is a rational number.
(Further, more general, results are available in [BKKKZ26].)
This was formalized in Lean by Baretto.
theorem erdos_1051 :
∀ (a : ℕ → ℤ), StrictMono a → GrowthCondition a →
Irrational (ErdosSeries a)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1051.lean, line 73.
Erdos1051.erdos_1051.variants.rapid_growth
Solved: stated here without proof.
Erdős [Er88c] notes that if the sequence grows rapidly to infinity (specifically, if \(a_{n+1} \geq C \cdot a_n^2\) for some constant \(C > 0\)), then the series is irrational.
theorem erdos_1051.variants.rapid_growth (a : ℕ → ℤ) (h_mono : StrictMono a)
(h_rapid : ∃ C > 0, ∀ n, (a (n + 1) : ℝ) ≥ C * (a n : ℝ) ^ 2) :
Irrational (ErdosSeries a)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1051.lean, line 83.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.