Erdős Problem 1072 to Erdős Problem 1094
TheoremErdős Problem 1072#
Reference: erdosproblems.com/1072
Quoted from FormalConjectures/ErdosProblems/1072.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/1072.
The file states 3 research or textbook statements: 3 open.
Erdos1072.erdos_1072.parts.i
Open: stated without proof.
Is it true that there are infinitely many \(p\) for which \(f(p) = p − 1\)?
theorem erdos_1072.parts.i : Set.Infinite {p | p.Prime ∧ f p = p - 1}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1072.lean, line 38.
Erdos1072.erdos_1072.parts.ii
Open: stated without proof.
Is it true that \(f(p)/p \to 0\) for \(p \to \infty\) in a density 1 subset of the primes?
theorem erdos_1072.parts.ii :
∃ (P : Set ℕ), P ⊆ {p | p.Prime} ∧ P.HasDensity 1 {p | p.Prime} ∧
Tendsto (fun p => (f p / p : ℝ)) (atTop ⊓ principal P) (𝓝 0)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1072.lean, line 43.
Erdos1072.erdos_1072.variants.littleo
Open: stated without proof.
Erdős, Hardy, and Subbarao [HaSu02], believed that the number of \(p \le x\) for which \(f(p)=p−1\) is \(o(x/\log x)\).
[HaSu02] Hardy, G. E. and Subbarao, M. V., A modified problem of Pillai and some related questions. Amer. Math. Monthly (2002), 554--559.
theorem erdos_1072.variants.littleo :
(fun x ↦ (({p | p.Prime ∧ f p = p - 1} ∩ Icc 0 x).ncard : ℝ)) =o[atTop]
(fun x ↦ x / Real.log x)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1072.lean, line 55.
Sources
TheoremErdős Problem 1073#
Reference: erdosproblems.com/1073
Quoted from FormalConjectures/ErdosProblems/1073.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/1073.
The file states 1 research or textbook statement: 1 open.
Erdos1073.erdos_1073
Open: stated without proof.
Is it true that \(A(x) \le x^{o(1)}\)?
theorem erdos_1073 :
∃ (o : ℕ → ℝ), o =o[atTop] (1 : ℕ → ℝ) ∧ ∀ x, A x ≤ x ^ (o x)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1073.lean, line 39.
Sources
TheoremErdős Problem 1074#
Reference: erdosproblems.com/1074
Quoted from FormalConjectures/ErdosProblems/1074.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/1074.
The file states 7 research or textbook statements: 5 open and 2 solved. It also has 5 test statements, counted here but not shown.
Erdos1074.erdos_1074.parts.i
Open: stated without proof.
Let \(S\) be the set of all \(m\geq 1\) such that there exists a prime \(p\not\equiv 1\pmod{m}\) such that \(m! + 1 \equiv 0\pmod{p}\). Does
\[ \lim\frac{|S\cap[1, x]|}{x} \]exist?
theorem erdos_1074.parts.i : ∃ c, EHSNumbers.HasDensity c
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1074.lean, line 60.
Erdos1074.erdos_1074.parts.ii
Open: stated without proof.
Let \(S\) be the set of all \(m\geq 1\) such that there exists a prime \(p\not\equiv 1\pmod{m}\) such that \(m! + 1 \equiv 0\pmod{p}\). What is
\[ \lim\frac{|S\cap[1, x]|}{x}? \]
theorem erdos_1074.parts.ii : EHSNumbers.HasDensity erdos_1074.parts.ii.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1074.lean, line 71.
Erdos1074.erdos_1074.parts.iii
Open: stated without proof.
Similarly, if \(P\) is the set of all primes \(p\) such that there exists an \(m\) with \(p\not\equiv 1\pmod{m}\) such that \(m! + 1 \equiv 0\pmod{p}\), then does
\[ \lim\frac{|P\cap[1, x]|}{\pi(x)} \]exist?
theorem erdos_1074.parts.iii : ∃ c, PillaiPrimes.HasDensity c {p | p.Prime}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1074.lean, line 81.
Erdos1074.erdos_1074.parts.iv
Open: stated without proof.
Similarly, if \(P\) is the set of all primes \(p\) such that there exists an \(m\) with \(p\not\equiv 1\pmod{m}\) such that \(m! + 1 \equiv 0\pmod{p}\), then what is
\[ \lim\frac{|P\cap[1, x]|}{\pi(x)}? \]
theorem erdos_1074.parts.iv :
PillaiPrimes.HasDensity erdos_1074.parts.iv.answer {p | p.Prime}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1074.lean, line 92.
Erdos1074.erdos_1074.variants.EHSNumbers_infinite
Solved: stated here; a Lean proof is at https://github.com/mzhorvath1/formal-conjectures/blob/3dec597bd1a73778760b761712a1fc5fb24bc5d7/FormalConjectures/ErdosProblems/1074.lean#L99.
Erdős, Hardy, and Subbarao proved that \(S\) is infinite.
Formal proof linked here provided by AlphaProof.
theorem erdos_1074.variants.EHSNumbers_infinite : EHSNumbers.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1074.lean, line 111.
Erdos1074.erdos_1074.variants.PillaiPrimes_infinite
Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_Erdos1074_erdos_1074_variants_PillaiPrimes_infinite.lean#L178.
Erdős, Hardy, and Subbarao proved that \(P\) is infinite.
theorem erdos_1074.variants.PillaiPrimes_infinite : PillaiPrimes.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1074.lean, line 117.
Erdos1074.erdos_1074.variants.EHSNumbers_one
Open: stated without proof.
Regarding the first question, Hardy and Subbarao computed all EHS numbers up to \(2^{10}\), and write "...if this trend conditions we expect [the limit] to be around 0.5, if it exists. The frequency with which the EHS numbers occur - most often in long sequences of consecutive integers - makes us believe that their asymptotic density exists and is unity. Erdős, though initially hesitant, later agreed with this view." That is, the conjecture is that \(S\) has density \(1\).
theorem erdos_1074.variants.EHSNumbers_one : EHSNumbers.HasDensity 1
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1074.lean, line 138.
Sources
TheoremErdős Problem 1075#
References: - erdosproblems.com/1075 - [Er64f] Erdős, P., On extremal problems of graphs and generalized graphs. Israel J. Math. (1964), 183--190.
Quoted from FormalConjectures/ErdosProblems/1075.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/1075.
The file states 1 research or textbook statement: 1 open.
Erdos1075.erdos_1075
Open: stated without proof.
Let \(r\geq 3\). There exists \(c_r>r^{-r}\) such that, for any \(\epsilon>0\), if \(n\) is sufficiently large, the following holds. Any \(r\)-uniform hypergraph on \(n\) vertices with at least \((1+\epsilon)(n/r)^r\) many edges contains a subgraph on \(m\) vertices with at least \(c_rm^r\) edges, where \(m=m(n)\to \infty\) as \(n\to \infty\).
theorem erdos_1075 :
∀ r : ℕ, 3 ≤ r → ∃ c : ℝ, (r : ℝ)⁻¹ ^ r < c ∧
∀ ε : ℝ, 0 < ε → ∃ m : ℕ → ℕ, Tendsto m atTop atTop ∧
∀ᶠ n : ℕ in atTop, ∀ H : Finset (Finset (Fin n)),
H.IsUniform r → (1 + ε) * ((n : ℝ) / r) ^ r ≤ H.card →
∃ S : Finset (Fin n), S.card = m n ∧
c * (S.card : ℝ) ^ r ≤ (H.hypergraphInduce S).card
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1075.lean, line 42.
Sources
TheoremErdős Problem 1077#
Reference: erdosproblems.com/1077
Quoted from FormalConjectures/ErdosProblems/1077.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/1077.
The file states 1 research or textbook statement: 1 solved.
Erdos1077.erdos_1077
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/dfe2d78128b493c572cf525b1b8edf4897fb7664/src/latest/ErdosProblems/Erdos1077.lean#L265.
We call a graph \(D\)-balanced (or \(D\)-almost-regular) if the maximum degree is at most \(D\) times the minimum degree.
Let \(ε, α > 0\) and \(D\) and \(n\) be sufficiently large. If \(G\) is a graph on \(n\) vertices with at least \(n^{1+α}\) edges, then must \(G\) contain a \(D\)-balanced subgraph on \(m > n^{1-α}\) vertices with at least \(εm^{1+α}\) edges?
theorem erdos_1077 :
¬ ∀ ε > (0 : ℝ), ε < 1 → ∀ α > (0 : ℝ), α < 1 → ∀ᶠ D in atTop, ∀ᶠ n in atTop,
∀ G : SimpleGraph (Fin n), G.edgeSet.ncard > (n : ℝ) ^ (1 + α) →
∃ (H : Subgraph G),
letI m := H.verts.ncard
IsBalanced H.coe D ∧
m > (n : ℝ) ^ (1 - α) ∧
H.edgeSet.ncard > ε * m ^ (1 + α)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1077.lean, line 44.
Sources
TheoremErdős Problem 1079#
References: - erdosproblems.com/1079 - [Er75] Erdős, P., Some recent progress on extremal problems in graph theory. Congr. Numer. (1975), 3-14. - [BoTh81] Bollobás, Béla and Thomason, Andrew, Dense neighbourhoods and Turán's theorem. J. Combin. Theory Ser. B (1981), 111--114. - [Bo83b] Bondy, J. A., Large dense neighbourhoods and Turán's theorem. J. Combin. Theory Ser. B (1983), 109--111.
Quoted from FormalConjectures/ErdosProblems/1079.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/1079.
The file states 2 research or textbook statements: 2 solved.
Erdos1079.erdos_1079
Solved: stated here without proof.
Let \(r\geq 4\). If \(G\) is a graph on \(n\) vertices with at least \(\mathrm{ex}(n;K_r)\) edges then must \(G\) contain a vertex with degree \(d\gg_r n\) whose neighbourhood contains at least \(\mathrm{ex}(d;K_{r-1})\) edges?
As Erdős [Er75] says 'if true this would be a nice generalisation of Turán's theorem'. This is true (unless \(G\) it itself the Turán graph), and was proved by Bollobás and Thomason [BoTh81]. Bondy [Bo83b] showed that if \(G\) has \(>\mathrm{ex}(n;K_r)\) edges then the corresponding vertex can be chosen to be of maximum degree in \(G\).
The number of edges in the neighbourhood of \(v\) is the number of edges of \(G\) both of whose endpoints are adjacent to \(v\). Graphs on a single vertex are excluded, since there every degree is \(0\).
theorem erdos_1079 : ∀ r : ℕ, 4 ≤ r → ∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 2 ≤ n →
∀ G : SimpleGraph (Fin n), extremalNumber n (completeGraph (Fin r)) ≤ G.edgeSet.ncard →
∃ v : Fin n, c * n ≤ G.degree v ∧
extremalNumber (G.degree v) (completeGraph (Fin (r - 1))) ≤
{e ∈ G.edgeSet | ∀ x ∈ e, G.Adj v x}.ncard
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1079.lean, line 55.
Erdos1079.erdos_1079.variants.bondy
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1079.lean#L424.
Bondy's strengthening [Bo83b]: if \(G\) has more than \(\mathrm{ex}(n;K_r)\) edges then some vertex \(v\) of maximum degree has \(d(v) \geq n/2\) and its neighbourhood contains more than \(\mathrm{ex}(d(v);K_{r-1})\) edges.
theorem erdos_1079.variants.bondy (r n : ℕ) (hr : 4 ≤ r) (G : SimpleGraph (Fin n))
[DecidableRel G.Adj]
(hG : extremalNumber n (completeGraph (Fin r)) < G.edgeSet.ncard) :
∃ v : Fin n, G.degree v = G.maxDegree ∧ n ≤ 2 * G.degree v ∧
extremalNumber (G.degree v) (completeGraph (Fin (r - 1))) <
{e ∈ G.edgeSet | ∀ x ∈ e, G.Adj v x}.ncard
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1079.lean, line 70.
Sources
TheoremErdős Problem 1080#
References: - erdosproblems.com/1080 - [DeSz92] de Caen, D. and Székely, L. A., The maximum size of {\(4\)}- and {\(6\)}-cycle free bipartite graphs on {\(m,n\)} vertices. (1992), 135--142. - [Er75] Erdős, P., Some recent progress on extremal problems in graph theory. Congr. Numer. (1975), 3-14. - [LUW94] Lazebnik, F. and Ustimenko, V. A. and Woldar, A. J., New constructions of bipartite graphs on {\(m,n\)} vertices with many edges and without small cycles. J. Combin. Theory Ser. B (1994), 111--117.
Quoted from FormalConjectures/ErdosProblems/1080.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/1080.
The file states 1 research or textbook statement: 1 solved.
Erdos1080.erdos_1080
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1080.lean.
Let \(G\) be a bipartite graph on \(n\) vertices such that one part has \(\lfloor n^{2/3}\rfloor\) vertices. Is there a constant \(c>0\) such that if \(G\) has at least \(cn\) edges then \(G\) must contain a \(C_6\)?
The answer is no, as shown by De Caen and Székely [DeSz92], who in fact show a stronger result. Let \(f(n,m)\) be the maximum number of edges of a bipartite graph between \(n\) and \(m\) vertices which does not contain either a \(C_4\) or \(C_6\). A positive answer to this question would then imply \(f(n,\lfloor n^{2/3}\rfloor)\ll n\). De Caen and Székely prove \(n^{10/9}\gg f(n,\lfloor n^{2/3}\rfloor) \gg n^{58/57+o(1)}\) for \(m\sim n^{2/3}\). They also prove more generally that, for \(n^{1/2}\leq m\leq n\), \(f(n,m) \ll (nm)^{2/3},\) which was also proved by Faudree and Simonovits.
This was formalized in Lean by Alexeev using Aristotle.
theorem erdos_1080 :
¬ ∃ c > (0 : ℝ), ∀ (V : Type) [Fintype V] [Nonempty V] (G : SimpleGraph V) (X Y : Set V),
IsBipartition G X Y → X.ncard = ⌊(Fintype.card V : ℝ) ^ (2/3 : ℝ)⌋₊ →
G.edgeSet.ncard ≥ c * Fintype.card V →
∃ (v : V) (walk : G.Walk v v), walk.IsCycle ∧ walk.length = 6
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1080.lean, line 61.
Sources
TheoremErdős Problem 1081#
References: - erdosproblems.com/1081 - [Er76e] Erdős, P., Problems and results on consecutive integers. Publ. Math. Debrecen 23 (1976), 271-282. - [Od81] Odoni, R. W. K., A problem of Erdős on sums of two squarefull numbers. Acta Arith. 39 (1981), 145-162. - [BlGr06] Blomer, V. and Granville, A., Estimates for representation numbers of quadratic forms. Duke Math. J. 135 (2006), 261-302.
Quoted from FormalConjectures/ErdosProblems/1081.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/1081.
The file states 2 research or textbook statements: 2 solved. It also has 1 test statement, counted here but not shown.
Erdos1081.erdos_1081
Solved: stated here without proof.
Let \(A(x)\) count the number of \(n\leq x\) which are the sum of two squarefull numbers (a number \(m\) is squarefull if \(p\mid m\) implies \(p^2\mid m\)). Is it true that
\[A(x) \sim c \frac{x}{\sqrt{\log x}}\]for some \(c>0\)?
Odoni [Od81] proved this is false.
theorem erdos_1081 :
¬ ∃ c > (0 : ℝ),
(fun x : ℝ ↦ (A x : ℝ)) ~[atTop] fun x ↦ c * x / Real.sqrt (Real.log x)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1081.lean, line 67.
Erdos1081.erdos_1081.variants.blomer_granville
Solved: stated here without proof.
Blomer and Granville [BlGr06] proved
\[A(x)= (\log\log x)^{O(1)}\frac{x}{(\log x)^{\alpha}}\]where \(\alpha=1-2^{-1/3}\approx 0.206299\): for some \(C\) and all large \(x\), \(A(x)\) lies between \((\log\log x)^{-C}\) and \((\log\log x)^{C}\) times \(x/(\log x)^{\alpha}\).
theorem erdos_1081.variants.blomer_granville :
∃ C : ℝ, 0 < C ∧ ∀ᶠ x : ℝ in atTop,
x / Real.log x ^ alpha / Real.log (Real.log x) ^ C ≤ A x ∧
(A x : ℝ) ≤ x / Real.log x ^ alpha * Real.log (Real.log x) ^ C
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1081.lean, line 79.
Sources
TheoremErdős Problem 1082#
Reference: erdosproblems.com/1082
Quoted from FormalConjectures/ErdosProblems/1082.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/1082.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos1082.erdos_1082.parts.i
Open: stated without proof.
Let \(A\subset \mathbb{R}^2\) be a set of \(n\) points with no three on a line. Does \(A\) determine at least \(\lfloor n/2\rfloor\) distinct distances?
theorem erdos_1082.parts.i : ∀ (A : Finset ℝ²) (hA_n3c : NonTrilinear (A : Set ℝ²)),
A.card / 2 ≤ distinctDistances A
Category research open; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/1082.lean, line 37.
Erdos1082.erdos_1082.parts.ii
Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/0aca4d71095301c0fd2dca32611b7addb2ea735c/FormalConjectures/ErdosProblems/1082.lean#L291.
Let \(A\subset \mathbb{R}^2\) be a set of \(n\) points with no three on a line. Must there exist a single point from which there are at least \(\lfloor n/2\rfloor\) distinct distances?
This question has been answered negatively by Xichuan in the comments, who gave a set of \(42\) points in \(\mathbb{R}^2\), with no three on a line, such that each point determines only \(20\) distinct distances.
A smaller counterexample has been formalised here: it comprised of \(8\) points, where each point only determines \(3\) distances.
This counterexample has originally been found by Heiko Harborth.
theorem erdos_1082.parts.ii :
¬ ∀ (A : Finset ℝ²) (hA : A.Nonempty) (hA_n3c : NonTrilinear (A : Set ℝ²)),
∃ (a : ℝ²) (ha : a ∈ A), A.card / 2 ≤ distinctDistancesFrom A a
Category research solved; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/1082.lean, line 57.
Sources
TheoremErdős Problem 1083#
References: - erdosproblems.com/1083 - [APST04] Aronov, Boris and Pach, János and Sharir, Micha and Tardos, Gábor, Distinct distances in three and higher dimensions. Combin. Probab. Comput. (2004), 283--293. - [CEGSW90] Clarkson, Kenneth L. and Edelsbrunner, Herbert and Guibas, Leonidas J. and Sharir, Micha and Welzl, Emo, Combinatorial complexity bounds for arrangements of curves and spheres. Discrete Comput. Geom. (1990), 99--160. - [Er46b] Erdős, P., On sets of distances of {\(n\)} points. Amer. Math. Monthly (1946), 248--250. - [SoVu08] Solymosi, József and Vu, Van H., Near optimal bounds for the {E}rdős distinct distances problem in high dimensions. Combinatorica (2008), 113--125.
Quoted from FormalConjectures/ErdosProblems/1083.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/1083.
The file states 1 research or textbook statement: 1 open.
Erdos1083.erdos_1083
Open: stated without proof.
Let \(d\geq 3\), and let \(f_d(n)\) be the minimal \(m\) such that every set of \(n\) points in \(\mathbb{R}^d\) determines at least \(m\) distinct distances. Estimate \(f_d(n)\) - in particular, is it true that
\[f_d(n)=n^{\frac{2}{d}-o(1)}?\]
theorem erdos_1083 :
∀ d : ℕ, 3 ≤ d → ∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧
∀ᶠ n : ℕ in atTop,
(minimalDistinctDistances (ℝ^d) n : ℝ) = (n : ℝ) ^ ((2 : ℝ) / (d : ℝ) - o n)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1083.lean, line 46.
Sources
TheoremErdős Problem 1084#
References: - erdosproblems.com/1084 - [Ha74b] Harborth, Heiko, Lösung zu Problem 664A. Elem. Math. (1974), 14--15.
Let
f_2(n)be the maximum number of pairs of points at distance exactly1among any set ofnpoints inℝ², under the condition that all pairwise distances are at least1.Estimate the growth of
f_2(n).Status: open.
Quoted from FormalConjectures/ErdosProblems/1084.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/1084.
The file states 5 research or textbook statements: 5 solved.
Erdos1084.erdos_1084.variants.upper_d1
Solved: stated here; a Lean proof is at https://github.com/Sanexxxx777/formal-conjectures/blob/9e4f3845be122a8fa3190d38543ebdd0a6f25605/FormalConjectures/ErdosProblems/1084.lean#L232.
It is easy to check that \(f_1(n) = n - 1\).
theorem erdos_1084.variants.upper_d1 : f 1 n = n - 1
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1084.lean, line 54.
Erdos1084.erdos_1084.variants.easy_upper_d2
Solved: stated here without proof.
It is easy to check that \(f_2(n) < 3n\).
theorem erdos_1084.variants.easy_upper_d2 (hn : n ≠ 0) : f 2 n < 3 * n
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1084.lean, line 59.
Erdos1084.erdos_1084.variants.upper_d2
Solved: stated here without proof.
Erdős showed that there is some constant \(c > 0\) such that \(f_2(n) < 3n - c n^{1/2}\).
theorem erdos_1084.variants.upper_d2 : ∃ c > (0 : ℝ), ∀ n > 0, f 2 n < 3 * n - c * sqrt n
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1084.lean, line 64.
Erdos1084.erdos_1084.variants.triangular_optimal_d2
Solved: stated here without proof.
Erdős conjectured that the triangular lattice is best possible in 2D, in particular that \(f_2(3n^2 + 3n + 1) = 9n^2 + 3n\). Harborth [Ha74b] proved this, and more generally \(f_2(n) = \lfloor 3n - \sqrt{12n - 3} \rfloor\) for all \(n \geq 2\).
Note: in [Er75f] is read \(9n^2 + 6n\), but this seems to be a typo.
theorem erdos_1084.variants.triangular_optimal_d2 : f 2 (3 * n ^ 2 + 3 * n + 1) = 9 * n ^ 2 + 3 * n
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1084.lean, line 74.
Erdos1084.erdos_1084.variants.upper_lower_d3
Solved: stated here without proof.
Erdős claims the existence of two constants \(c_1, c_2 > 0\) such that \(6n - c_1 n^{2/3} ≤ f_3(n) \le 6n - c_2 n^{2/3}\).
theorem erdos_1084.variants.upper_lower_d3 :
∃ c₁ : ℝ, ∃ c₂ > (0 : ℝ), ∀ᶠ n in atTop,
6 * n - c₁ * n ^ (2 / 3 : ℝ) ≤ f 3 n ∧ f 3 n ≤ 6 * n - c₂ * n ^ (2 / 3 : ℝ)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1084.lean, line 80.
Sources
TheoremErdős Problem 1085#
Let f_d(n) be minimal such that, in any set of n points in ℝ^d, there exist at most f_d(n) pairs of points which are distance 1 apart. Estimate f_d(n).
Reference: erdosproblems.com/1085
Quoted from FormalConjectures/ErdosProblems/1085.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/1085.
The file states 7 research or textbook statements: 1 open and 6 solved.
Erdos1085.erdos_1085.variants.lower_d2
Solved: stated here without proof.
Erdős showed \(f_2(n) > n^{1+c/\log\log n}\) for some \(c > 0\).
theorem erdos_1085.variants.lower_d2 :
∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (n : ℝ) ^ (1 + c / log (log n)) < f 2 n
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1085.lean, line 45.
Erdos1085.erdos_1085.variants.upper_d2
Solved: stated here without proof.
Spencer, Szemerédi, and Trotter showed \(f_2(n) = O(n^{4/3})\).
theorem erdos_1085.variants.upper_d2 : (fun n ↦ (f 2 n : ℝ)) =O[atTop] (fun n ↦ (n : ℝ) ^ (4/3 : ℝ))
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1085.lean, line 51.
Erdos1085.erdos_1085.variants.lower_d3
Solved: stated here without proof.
Erdős showed \(f_3(n) = Ω(n^{4/3}\log\log n)\).
theorem erdos_1085.variants.lower_d3 :
(fun n : ℕ ↦ (n : ℝ) ^ (4/3 : ℝ) * log (log n)) =O[atTop] (fun n ↦ (f 3 n : ℝ))
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1085.lean, line 56.
Erdos1085.erdos_1085.variants.upper_d3
Open: stated without proof.
Is the \(n^{4/3}\log\log n\) lower bound in 3D also an upper bound?.
theorem erdos_1085.variants.upper_d3 :
(fun n ↦ (f 3 n : ℝ)) =O[atTop] (fun n : ℕ ↦ (n : ℝ) ^ (4/3 : ℝ) * log (log n))
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1085.lean, line 62.
Erdos1085.erdos_1085.variants.lower_d4_lenz
Solved: stated here without proof.
Lenz showed that, for \(d \ge 4\), \(f_d(n) \ge \frac{p - 1}{2p} n^2 - O(1)\) where \(p = \lfloor\frac d2\rfloor\).
theorem erdos_1085.variants.lower_d4_lenz (hd : 4 ≤ d) :
∃ C : ℝ, ∀ n : ℕ, ↑(d / 2 - 1) / (2 * ↑(d / 2)) * n ^ 2 - C ≤ f d n
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1085.lean, line 69.
Erdos1085.erdos_1085.variants.upper_d4_erdos
Solved: stated here without proof.
Erdős showed that, for \(d \ge 4\), \(f_d(n) \le \left(\frac{p - 1}{2p} + o(1)\right) n^2\) where \(p = \lfloor\frac d2\rfloor\).
theorem erdos_1085.variants.upper_d4_erdos (hd : 4 ≤ d) :
∃ g : ℕ → ℝ, Tendsto g atTop (𝓝 0) ∧
∀ n, f d n ≤ (↑(d / 2 - 1) / (2 * ↑(d / 2)) + g n) * n ^ 2
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1085.lean, line 76.
Erdos1085.erdos_1085.variants.upper_lower_d5_odd
Solved: stated here without proof.
Erdős and Pach showed that, for \(d \ge 5\) odd, there exist constants \(c_1(d), c_2(d) > 0\) such that \(\frac{p - 1}{2p} n^2 + c_1 n^{4/3} \le f_d(n) \le \frac{p - 1}{2p} n^2 + c_2 n^{4/3}\) where \(p = \lfloor\frac d2\rfloor\).
theorem erdos_1085.variants.upper_lower_d5_odd (hd : 5 ≤ d) (hd_odd : Odd d) :
∃ c₁ > (0 : ℝ), ∃ c₂ : ℝ, ∀ᶠ n in atTop,
↑(d / 2 - 1) / (2 * ↑(d / 2)) * n ^ 2 + c₁ * n ^ (4 / 3 : ℝ) ≤ f d n ∧
f d n ≤ ↑(d / 2 - 1) / (2 * ↑(d / 2)) * n ^ 2 + c₂ * n ^ (4 / 3 : ℝ)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1085.lean, line 85.
Sources
TheoremErdős Problem 1086#
References: - erdosproblems.com/1086 - [ErPu71] Erdős, P. and Purdy, G., Some extremal problems in geometry. J. Combinatorial Theory Ser. A 10 (1971), 246-252. - [RaSh17] Raz, O. E. and Sharir, M., The number of unit-area triangles in the plane: theme and variations. Combinatorica 37 (2017), 1221-1240. arXiv:1501.00379
Quoted from FormalConjectures/ErdosProblems/1086.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/1086.
The file states 3 research or textbook statements: 1 open and 2 solved. It also has 2 API statements, counted here but not shown.
Erdos1086.erdos_1086
Open: stated without proof.
Let \(g(n)\) be minimal such that any set of \(n\) points in \(\mathbb{R}^2\) contains the vertices of at most \(g(n)\) many triangles with the same area. Estimate \(g(n)\).
Only triangles of positive area are counted.
theorem erdos_1086 : (fun n : ℕ ↦ (g n : ℝ)) =Θ[atTop] erdos_1086.answer
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1086.lean, line 78.
Erdos1086.erdos_1086.variants.erdos_purdy_lower
Solved: stated here without proof.
Erdős and Purdy [ErPu71] proved
\[n^2\log\log n \ll g(n) \ll n^{5/2}.\]This is the lower bound.
theorem erdos_1086.variants.erdos_purdy_lower :
(fun n : ℕ ↦ (n : ℝ) ^ 2 * Real.log (Real.log n)) =O[atTop] fun n : ℕ ↦ (g n : ℝ)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1086.lean, line 88.
Erdos1086.erdos_1086.variants.raz_sharir
Solved: stated here without proof.
The upper bound of Erdős and Purdy [ErPu71] has been improved a number of times. The best known bound is \(g(n) \ll n^{20/9}\) by Raz and Sharir [RaSh17].
theorem erdos_1086.variants.raz_sharir :
(fun n : ℕ ↦ (g n : ℝ)) =O[atTop] fun n : ℕ ↦ (n : ℝ) ^ (20 / 9 : ℝ)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1086.lean, line 97.
Sources
TheoremErdős Problem 1087#
References: - erdosproblems.com/1087 - [ErPu71] Erdős, P. and Purdy, G., Some extremal problems in geometry. J. Combinatorial Theory Ser. A 10 (1971), 246-252.
Quoted from FormalConjectures/ErdosProblems/1087.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/1087.
The file states 3 research or textbook statements: 1 open and 2 solved. It also has 2 API statements, counted here but not shown.
Erdos1087.erdos_1087
Open: stated without proof.
Let \(f(n)\) be minimal such that every set of \(n\) points in \(\mathbb{R}^2\) contains at most \(f(n)\) many sets of four points which are 'degenerate' in the sense that some pair are the same distance apart. Estimate \(f(n)\) - in particular, is it true that \(f(n)\leq n^{3+o(1)}\)?
Here a set of four points is degenerate if two of its six pairwise distances are equal, and \(f(n)\leq n^{3+o(1)}\) is read as \(f(n) \ll n^{3+\varepsilon}\) for every \(\varepsilon > 0\).
theorem erdos_1087 :
∀ ε > (0 : ℝ), (fun n : ℕ ↦ (f n : ℝ)) =O[atTop] fun n : ℕ ↦ (n : ℝ) ^ (3 + ε)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1087.lean, line 76.
Erdos1087.erdos_1087.variants.lower
Solved: stated here without proof.
Erdős and Purdy [ErPu71] proved
\[n^3\log n \ll f(n) \ll n^{7/2}.\]This is the lower bound.
theorem erdos_1087.variants.lower :
(fun n : ℕ ↦ (n : ℝ) ^ 3 * Real.log n) =O[atTop] fun n : ℕ ↦ (f n : ℝ)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1087.lean, line 87.
Erdos1087.erdos_1087.variants.upper
Solved: stated here without proof.
Erdős and Purdy [ErPu71] proved
\[n^3\log n \ll f(n) \ll n^{7/2}.\]This is the upper bound.
theorem erdos_1087.variants.upper :
(fun n : ℕ ↦ (f n : ℝ)) =O[atTop] fun n : ℕ ↦ (n : ℝ) ^ (7 / 2 : ℝ)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1087.lean, line 98.
Sources
TheoremErdős Problem 1088#
Reference: erdosproblems.com/1088
Quoted from FormalConjectures/ErdosProblems/1088.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/1088.
The file states 1 research or textbook statement: 1 open. It also has 1 API statement, counted here but not shown.
Erdos1088.erdos_1088
Open: stated without proof.
Let \(f_d(n)\) be the minimal \(m\) such that any set of \(m\) points in \(\mathbb{R}^d\) contains a set of \(n\) points for which any two determined distances are distinct. Erdős Problem 1088 asks to estimate \(f_d(n)\). In particular, is it true that, for every fixed \(n \geq 3\),
\[ f_d(n) = 2^{o(d)} \]as \(d \to \infty\)?
The little-\(o\) condition is stated after taking the base-\(2\) logarithm.
theorem erdos_1088 :
∀ n ≥ 3,
(fun d : ℕ ↦ Real.logb 2 (f d n : ℝ)) =o[atTop] (fun d : ℕ ↦ (d : ℝ))
Category research open; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/1088.lean, line 73.
Sources
TheoremErdős Problem 1089#
References: - erdosproblems.com/1089 - [Er75f] Erdős, Paul, On some problems of elementary and combinatorial geometry. Ann. Mat. Pura Appl. (4) (1975), 99-108. - [BBS83] Bannai, Eiichi and Bannai, Etsuko and Stanton, Dennis, An upper bound for the cardinality of an \(s\)-distance subset in real Euclidean space. II. Combinatorica (1983), 147-152.
Quoted from FormalConjectures/ErdosProblems/1089.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/1089.
The file states 2 research or textbook statements: 2 solved.
Erdos1089.erdos_1089
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1089.lean#L769.
Let \(g_d(n)\) be minimal such that every collection of \(g_d(n)\) points in \(\mathbb{R}^d\) determines at least \(n\) many distinct distances. Estimate \(g_d(n)\). In particular, does
\[\lim_{d \to \infty} \frac{g_d(n)}{d^{n-1}}\]exist?
A problem of Erdős [Er75f, p.105]. The answer is yes: for \(n \ge 2\),
\[\binom{d+1}{n-1} + 1 \le g_d(n) \le \binom{d+n-1}{n-1} + 1,\]where the upper bound is due to Bannai, Bannai and Stanton [BBS83] and the lower bound to a construction of Aletheia (generalising constructions for Problem 502), so that \(g_d(n) / d^{n-1} \to 1/(n-1)!\) as \(d \to \infty\).
theorem erdos_1089 :
∀ n : ℕ, 2 ≤ n → ∃ L : ℝ,
Tendsto (fun d : ℕ => (g d n : ℝ) / (d : ℝ) ^ (n - 1)) atTop (𝓝 L)
Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1089.lean, line 60.
Erdos1089.erdos_1089.variants.bounds_and_limit
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1089.lean#L769.
For \(n \ge 2\) one has \(\binom{d+1}{n-1} + 1 \le g_d(n) \le \binom{d+n-1}{n-1} + 1\) for all \(d \ge 1\), and \(g_d(n) / d^{n-1} \to 1/(n-1)!\) as \(d \to \infty\).
theorem erdos_1089.variants.bounds_and_limit (n : ℕ) (hn : 2 ≤ n) :
(∀ d, 1 ≤ d → (d + 1).choose (n - 1) + 1 ≤ g d n ∧ g d n ≤ (d + n - 1).choose (n - 1) + 1) ∧
Tendsto (fun d : ℕ => (g d n : ℝ) / (d : ℝ) ^ (n - 1)) atTop
(𝓝 ((1 : ℝ) / (n - 1).factorial))
Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1089.lean, line 72.
Sources
TheoremErdős Problem 1090#
References: - erdosproblems.com/1090 - [Er75f] Erdős, Paul, On some problems of elementary and combinatorial geometry. Ann. Mat. Pura Appl. (4) (1975), 99-108.
Quoted from FormalConjectures/ErdosProblems/1090.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/1090.
The file states 1 research or textbook statement: 1 solved.
Erdos1090.erdos_1090
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1090.lean.
Let \(k\geq 3\). Does there exist a finite set \(A\subset \mathbb{R}^2\) such that, in any \(2\)-colouring of \(A\), there exists a line which contains at least \(k\) points from \(A\), and all the points of \(A\) on the line have the same colour?
Erdős [Er75f] says Graham and Selfridge proved the answer is yes when \(k=3\). Hunter has observed that, for sufficiently large \(n\), a generic projection of \([k]^n\) into \(\mathbb{R}^2\) has this property, by the Hales-Jewett theorem.
theorem erdos_1090 : ∀ (k : ℕ), ∀ (hk : 3 ≤ k),
∃ (A : Finset (Fin 2 → ℝ)), ∀ (C : A → Fin 2),
∃ (S : Finset (Fin 2 → ℝ)), ∃ (hSA : S ⊆ A),
Collinear ℝ (S : Set (Fin 2 → ℝ)) ∧ S.card ≥ k ∧
(∀ y ∈ A, y ∈ affineSpan ℝ (S : Set (Fin 2 → ℝ)) → y ∈ S) ∧
∃ c, ∀ x (hx : x ∈ S), C ⟨x, hSA hx⟩ = c
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1090.lean, line 39.
Sources
TheoremErdős Problem 1092#
References: - Erdős Problem 1092 - [Ro82] V. Rödl, Nearly bipartite graphs with large chromatic number, Combinatorica 2 (1982), 377–383.
Quoted from FormalConjectures/ErdosProblems/1092.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/1092.
The file states 2 research or textbook statements: 2 solved.
Erdos1092.f_asymptotic_2
Solved: stated here without proof.
Is it true that \(f_2(n) \gg n\)? Disproved by Rödl, who showed \(f_r(n) = o(n)\) for all fixed \(r \geq 2\). A conjecture of Erdős, Hajnal, and Szemerédi.
This seems to be closely related to, but distinct from, 744.
Tang notes in the comments that Rödl [Ro82] constructed, for any \(\epsilon>0\) and \(k\), a graph with chromatic number \(\geq k\) such that every graph on \(m\) vertices is bipartite after deleting at most \(\epsilon m\) edges.
theorem f_asymptotic_2 :
¬ ∃ g : ℕ → ℕ, IsAdmissible 2 g ∧
(fun n : ℕ => (n : ℝ)) =O[atTop] (fun n : ℕ => (g n : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1092.lean, line 68.
Erdos1092.f_asymptotic_general
Solved: stated here without proof.
More generally, is \(f_r(n)\gg_r n\) for every \(r \geq 2\)? Disproved by Rödl, who showed \(f_r(n) = o(n)\) for all fixed \(r \geq 2\).
theorem f_asymptotic_general :
¬ ∀ r : ℕ, 2 ≤ r → ∃ g : ℕ → ℕ, IsAdmissible r g ∧
(fun n : ℕ => (n : ℝ)) =O[atTop] (fun n : ℕ => (g n : ℝ))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1092.lean, line 76.
Sources
TheoremErdős Problem 1093#
Reference: erdosproblems.com/1093
Quoted from FormalConjectures/ErdosProblems/1093.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/1093.
The file states 2 research or textbook statements: 2 open.
Erdos1093.erdos_1093.parts.i
Open: stated without proof.
Are there infinitely many binomial coefficients with deficiency 1?
theorem erdos_1093.parts.i :
{x : ℕ × ℕ | let k := x.1; let n := x.2; 2 * k ≤ n ∧ deficiency n k = 1 ∧
∀ p, p.Prime → (p ∣ choose n k) → k < p}.Infinite
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1093.lean, line 46.
Erdos1093.erdos_1093.parts.ii
Open: stated without proof.
Are there only finitely many binomial coefficients with deficiency > 1?
theorem erdos_1093.parts.ii :
{x : ℕ × ℕ | let k := x.1; let n := x.2; 2 * k ≤ n ∧ deficiency n k > 1 ∧
∀ p, p.Prime → (p ∣ choose n k) → k < p}.Finite
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1093.lean, line 55.
Sources
TheoremErdős Problem 1094#
Reference: erdosproblems.com/1094
Quoted from FormalConjectures/ErdosProblems/1094.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/1094.
The file states 1 research or textbook statement: 1 open.
Erdos1094.erdos_1094
Open: stated without proof.
For all \(n\ge 2k\) the least prime factor of \(\binom{n}{k}\) is \(\le\max(n/k,k)\), with only finitely many exceptions.
theorem erdos_1094 :
{(n, k) : ℕ × ℕ | 0 < k ∧ 2 * k ≤ n ∧ (n.choose k).minFac > max (n / k) k}.Finite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1094.lean, line 38.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.