Erdős Problem 200 to Erdős Problem 221
TheoremErdős Problem 200#
Reference: erdosproblems.com/200
Quoted from FormalConjectures/ErdosProblems/200.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/200.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos200.erdos_200
Open: stated without proof.
Does the longest arithmetic progression of primes in \(\{1,\ldots,N\}\) have length \(o(\log N)\)?
theorem erdos_200 :
(fun n => (longestPrimeArithmeticProgressions n : ℝ)) =o[atTop] (fun n => log n)
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/200.lean, line 42.
Erdos200.erdos_200.variants.upper
Solved: stated here without proof.
It follows from the prime number theorem that such a progression has length \(\leq(1+o(1))\log N\).
theorem erdos_200.variants.upper : ∃ (o : ℕ → ℝ) (_ : o =o[atTop] (1 : ℕ → ℝ)),
∀ n, longestPrimeArithmeticProgressions n ≤ (1 + o n) * log n
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/200.lean, line 50.
Sources
TheoremErdős Problem 202#
References: - erdosproblems.com/202 - [BFV13] de la Bretèche, Régis and Ford, Kevin and Vandehey, Joseph, On non-intersecting arithmetic progressions. Acta Arith. (2013), 381-392. - [Ch05] Chen, Yong-Gao, On disjoint arithmetic progressions. Acta Arith. (2005), 143-148. - [Cr03b] Croot, III, Ernest S., On non-intersecting arithmetic progressions. Acta Arith. (2003), 233-238. - [ErSz68] Erdős, P. and Szemerédi, E., On a problem of P. Erdős and S. Stein. Acta Arith. (1968), 85-90. - [PaPh24] Park, Jinyoung and Pham, Huy Tuan, A proof of the Kahn-Kalai conjecture. J. Amer. Math. Soc. (2024), 235-243.
Quoted from FormalConjectures/ErdosProblems/202.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/202.
The file states 2 research or textbook statements: 2 solved.
Erdos202.erdos_202
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos202.lean.
Let \(n_1\lt \cdots < n_r\leq N\) with associated \(a_i\pmod{n_i}\) such that the congruence classes are disjoint (that is, every integer is \(\equiv a_i\pmod{n_i}\) for at most one \(1\leq i\leq r\)). How large can \(r\) be in terms of \(N\)?
Let \(f(N)\) be the maximum possible \(r\), and let \(L(N)=\exp(\sqrt{\log N\log\log N})\).
This was proved by GPT-5.4 Pro (prompted by Ho Boon Suan), using the argument of [BFV13] together with the resolution of the Kahn-Kalai conjecture by Park and Pham [PaPh24], so that
\[f(N)= N L(N)^{-1+o(1)}.\]
theorem erdos_202 : ∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧
∀ᶠ N : ℕ in atTop, (f N : ℝ) = (N : ℝ) * scaleL N ^ (-1 + o N)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/202.lean, line 64.
Erdos202.erdos_202.variants.erdos_szemeredi
Solved: stated here without proof.
Erdős and Stein conjectured that \(f(N)=o(N)\), which was proved by Erdős and Szemerédi [ErSz68].
theorem erdos_202.variants.erdos_szemeredi :
(fun N => (f N : ℝ)) =o[atTop] (fun N : ℕ => (N : ℝ))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/202.lean, line 72.
Sources
TheoremErdős Problem 203#
Reference: erdosproblems.com/203
Quoted from FormalConjectures/ErdosProblems/203.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/203.
The file states 1 research or textbook statement: 1 open.
Erdos203.erdos_203
Open: stated without proof.
Is there an integer \(m\) with \((m, 6) = 1\) such that none of \(2^k \cdot 3^\ell \cdot m + 1\) are prime, for any \(k, \ell \ge 0\)?
theorem erdos_203 : ∃ m, m.Coprime 6 ∧ ∀ k l, ¬ (2^k * 3^l * m + 1).Prime
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/203.lean, line 35.
Sources
TheoremErdős Problem 204#
References: - erdosproblems.com/204 - [Ad25] S. Adenwalla, A Question of Erdős and Graham on Covering Systems. arXiv:2501.15170 (2025).
Quoted from FormalConjectures/ErdosProblems/204.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/204.
The file states 1 research or textbook statement: 1 solved.
Erdos204.erdos_204
Solved: stated here; a Lean proof is at https://github.com/Woett/Lean-files/blob/main/ErdosProblem204.lean.
Are there \(n\) such that there is a covering system with moduli the divisors of \(n\) which is 'as disjoint as possible'?
That is, for all \(d\mid n\) with \(d>1\) there is an associated \(a_d\) such that every integer is congruent to some \(a_d\pmod{d}\), and if there is some integer \(x\) with
\[x\equiv a_d\pmod{d}\textrm{ and }x\equiv a_{d'}\pmod{d'}\]then \((d,d')=1\).
The density of such \(n\) is zero. Erdős and Graham believed that no such \(n\) exist.
Adenwalla [Ad25] has proved there are no such \(n\).
This was formalized by van Doorn in Lean using Aristotle.
theorem erdos_204 : ¬ ∃ (n : ℕ) (a : ℕ → ℤ),
let D := {d : ℕ | d ∣ n ∧ d > 1}
(∀ x : ℤ, ∃ d ∈ D, x ≡ a d [ZMOD d]) ∧
(∀ d ∈ D, ∀ d' ∈ D, d ≠ d' → (∃ x : ℤ, x ≡ a d [ZMOD d] ∧ x ≡ a d' [ZMOD d']) →
Nat.gcd d d' = 1)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/204.lean, line 48.
Sources
TheoremErdős Problem 205#
References: - erdosproblems.com/205 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [Ro34] Romanoff, N. P., Über einige Sätze der additiven Zahlentheorie. Math. Ann. (1934), 668-678.
Quoted from FormalConjectures/ErdosProblems/205.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/205.
The file states 5 research or textbook statements: 1 open and 4 solved.
Erdos205.erdos_205.parts.i
Solved: stated here without proof.
Is it true that all sufficiently large \(n\) can be written as \(2^k+m\) for some \(k\geq 0\), where \(\Omega(m)\lt \log\log m\)? (Here \(\Omega(m)\) is the number of prime divisors of \(m\) counted with multiplicity.)
Barreto and Leeham, using ChatGPT and Aristotle, have proved a negative answer, which was quantified by Tao and Alexeev (see the comments): in fact there are infinitely many \(n\) such that, for all \(k\) with \(2^k\lt n\), \(n-2^k\) has at least
\[\gg \left(\frac{\log n}{\log\log n}\right)^{1/2}\]many prime factors.
theorem erdos_205.parts.i :
¬ ∀ᶠ n : ℕ in atTop, IsRepresentable (fun m => Real.log (Real.log m)) n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/205.lean, line 58.
Erdos205.erdos_205.parts.ii
Solved: stated here without proof.
Is it true that all sufficiently large \(n\) can be written as \(2^k+m\) for some \(k\geq 0\), where \(\Omega(m)\lt \log\log m\)? (Here \(\Omega(m)\) is the number of prime divisors of \(m\) counted with multiplicity.) What about \(\lt \epsilon \log\log m\)?
Barreto and Leeham, using ChatGPT and Aristotle, have proved a negative answer, which was quantified by Tao and Alexeev (see the comments).
theorem erdos_205.parts.ii :
¬ ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
IsRepresentable (fun m => ε * Real.log (Real.log m)) n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/205.lean, line 71.
Erdos205.erdos_205.parts.iii
Solved: stated here without proof.
Is it true that all sufficiently large \(n\) can be written as \(2^k+m\) for some \(k\geq 0\), where \(\Omega(m)\lt \log\log m\)? (Here \(\Omega(m)\) is the number of prime divisors of \(m\) counted with multiplicity.) Or some more slowly growing function?
Barreto and Leeham, using ChatGPT and Aristotle, have proved a negative answer, which was quantified by Tao and Alexeev (see the comments).
theorem erdos_205.parts.iii :
¬ ∃ f : ℕ → ℝ, f =o[atTop] (fun m : ℕ => Real.log (Real.log m)) ∧
∀ᶠ n : ℕ in atTop, IsRepresentable f n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/205.lean, line 85.
Erdos205.erdos_205.variants.many_prime_factors
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos205.lean.
In fact there are infinitely many \(n\) such that, for all \(k\) with \(2^k\lt n\), \(n-2^k\) has at least
\[\gg \left(\frac{\log n}{\log\log n}\right)^{1/2}\]many prime factors.
theorem erdos_205.variants.many_prime_factors : ∃ c > (0 : ℝ),
{n : ℕ | ∀ k : ℕ, 2 ^ k < n →
c * Real.sqrt (Real.log n / Real.log (Real.log n)) ≤ (Ω (n - 2 ^ k) : ℝ)}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/205.lean, line 97.
Erdos205.erdos_205.variants.odd_counterexamples
Open: stated without proof.
The \(n\) constructed in this way are divisible by a large power of \(2\). It remains open whether there exist arbitrarily large odd counterexamples.
theorem erdos_205.variants.odd_counterexamples :
{n : ℕ | Odd n ∧ ¬ IsRepresentable (fun m => Real.log (Real.log m)) n}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/205.lean, line 107.
Sources
TheoremErdős Problem 206#
References: - erdosproblems.com/206 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique (1980). - [Cu22] Curtiss, D. R., On Kellogg's Diophantine Problem. Amer. Math. Monthly (1922), 380-387. - [Er50b] Erdős, Pál, On a Diophantine equation. Mat. Lapok (1950), 192-210. - [Na23] Nathanson, M., Underapproximation by Egyptian fractions. J. Number Theory (2023), 208-234. - [Ch23b] Chu, H. V., A threshold for the best two-term underapproximation by Egyptian fractions. arXiv:2306.12564 (2023). - [Ko24b] Kovač, V., On eventually greedy best underapproximations by Egyptian fractions. arXiv:2406.07218 (2024).
Quoted from FormalConjectures/ErdosProblems/206.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/206.
The file states 1 research or textbook statement: 1 solved.
Erdos206.erdos_206
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/68da20b96673899166e94638f5a7fffeb7231d35/src/latest/ErdosProblems/Erdos206.lean.
Let \(x>0\) be a real number. For any \(n\geq 1\) let
\[R_n(x) = \sum_{i=1}^n\frac{1}{m_i}\lt x\]be the maximal sum of \(n\) distinct unit fractions which is \(\lt x\).
Is it true that, for almost all \(x\), for sufficiently large \(n\), we have
\[R_{n+1}(x)=R_n(x)+\frac{1}{m},\]where \(m\) is minimal such that \(m\) does not appear in \(R_n(x)\) and the right-hand side is \(\lt x\)? (That is, are the best underapproximations eventually always constructed in a 'greedy' fashion?)
Kovač [Ko24b] has proved that this is false - in fact as false as possible: the set of \(x\in (0,\infty)\) for which the best underapproximations are eventually 'greedy' has Lebesgue measure zero.
theorem erdos_206 :
¬ ∀ᵐ x ∂(volume.restrict (Set.Ioi (0 : ℝ))), EventuallyGreedy x
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/206.lean, line 98.
Sources
TheoremErdős Problem 207#
References: - erdosproblems.com/207 - [KSSS22b] Kwan, M. and Sah, A. and Sawhney, M. and Simkin, M., High-girth Steiner triple systems. arXiv:2201.04554 (2022).
Quoted from FormalConjectures/ErdosProblems/207.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/207.
The file states 1 research or textbook statement: 1 solved.
Erdos207.erdos_207
Solved: stated here without proof.
For any \(g\geq 2\), if \(n\) is sufficiently large and \(\equiv 1,3\pmod{6}\) then there exists a 3-uniform hypergraph on \(n\) vertices such that
every pair of vertices is contained in exactly one edge (i.e. the graph is a Steiner triple system) and
for any \(2\leq j\leq g\) any collection of \(j\) edges contains at least \(j+3\) vertices.
Proved by Kwan, Sah, Sawhney, and Simkin [KSSS22b].
theorem erdos_207 :
∀ g : ℕ, 2 ≤ g → ∀ᶠ n : ℕ in atTop,
n % 6 = 1 ∨ n % 6 = 3 → ∃ H : Finset (Finset (Fin n)),
H.IsBlockDesign 2 3 ∧ ∀ E ⊆ H,
2 ≤ E.card → E.card ≤ g → E.card + 3 ≤ (E.biUnion id).card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/207.lean, line 47.
Sources
TheoremErdős Problem 208#
Reference: erdosproblems.com/208
Quoted from FormalConjectures/ErdosProblems/208.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/208.
The file states 3 research or textbook statements: 3 open.
Erdos208.erdos_208.parts.i
Open: stated without proof.
Let \(s_1 < s_2 < \dots\) be the sequence of squarefree numbers. Is it true that for any \(\epsilon > 0\) and large \(n\), \(s_{n+1} - s_n \ll_\epsilon s_n^\epsilon\)?
theorem erdos_208.parts.i :
∀ ε > (0 : ℝ), (fun n => (s (n + 1) - s n : ℝ)) =O[atTop] (fun n => (s n : ℝ)^ε)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/208.lean, line 41.
Erdos208.erdos_208.parts.ii
Open: stated without proof.
Let \(s_1 < s_2 < \dots\) be the sequence of squarefree numbers. Is it true that \(s_{n + 1} - s_n \le (1 + o(1)) \cdot (\pi^2 / 6) \cdot \log (s_n) / \log (\log (s_n))\)?
theorem erdos_208.parts.ii : ∃ (c : ℕ → ℝ), (c =o[atTop] (1 : ℕ → ℝ)) ∧ ∀ᶠ n in atTop,
s (n + 1) - s n ≤ (1 + (c n)) * (π^2 / 6) * log (s n) / log (log (s n))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/208.lean, line 49.
Erdos208.erdos_208.variants.log_bound
Open: stated without proof.
In [Er79] Erdős says perhaps \(s_{n+1} - s_n \ll \log s_n\), but he is 'very doubtful'.
[Er79] Erdős, Paul, Some unconventional problems in number theory. Math. Mag. (1979), 67-70.
theorem erdos_208.variants.log_bound :
(fun n ↦ (s (n + 1) - s n : ℝ)) =O[atTop] fun n ↦ log (s n)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/208.lean, line 59.
Sources
TheoremErdős Problem 209#
References: - erdosproblems.com/209 - [Er84] Erdős, P., Research problems. Period. Math. Hungar. (1984), 101-103. - [ErPu95b] Erdős, Paul and Purdy, George, Extremal problems in combinatorial geometry. Handbook of combinatorics, Vol. 1, 2 (1995), 809-874. - [FuPa84] Füredi, Z. and Palásti, I., Arrangements of lines with a large number of triangles. Proc. Amer. Math. Soc. (1984), 561-566. - [Es16] Escudero, Juan García, Gallai triangles in configurations of lines in the projective plane. C. R. Math. Acad. Sci. Paris (2016), 551-554.
Quoted from FormalConjectures/ErdosProblems/209.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/209.
The file states 1 research or textbook statement: 1 solved.
Erdos209.erdos_209
Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/110d489ed5c07e5b216453e092e9113127c98c9a/problems/209/Erdos209.lean.
Let \(A\) be a finite collection of \(d\geq 4\) non-parallel lines in \(\mathbb{R}^2\) such that there are no points where at least four lines from \(A\) meet. Must there exist a 'Gallai triangle' (or 'ordinary triangle'): three lines from \(A\) which intersect in three points, and each of these intersection points only intersects two lines from \(A\)?
Füredi and Palásti [FuPa84] showed this is false when \(d\geq 4\) is not divisible by \(9\). Escudero [Es16] showed this is false for all \(d\geq 4\).
theorem erdos_209 :
¬ ∀ d : ℕ, 4 ≤ d → ∀ A : Finset (AffineSubspace ℝ ℝ²), A.card = d →
(∀ L ∈ A, IsLine L) →
((A : Set (AffineSubspace ℝ ℝ²)).Pairwise fun L₁ L₂ => ¬ L₁ ∥ L₂) →
(∀ p : ℝ², pointMultiplicity A p ≤ 3) →
HasGallaiTriangle A
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/209.lean, line 66.
Sources
TheoremErdős Problem 210#
References: - erdosproblems.com/210 - [Mo51] Motzkin, T. S., The lines and planes connecting the points of a finite set. Transactions of the American Mathematical Society 70 (1951), 451–464. - [KeMo58] Kelly, L. M. and Moser, W. O. J., On the number of ordinary lines determined by n points. Canadian Journal of Mathematics 10 (1958), 210–219. - [CsSa93] Csima, J. and Sawyer, E. T., There exist 6n/13 ordinary points. Discrete & Computational Geometry 9 (1993), 187–202. - [GrTa13] Green, B. and Tao, T., On sets defining few ordinary lines. Discrete & Computational Geometry 50 (2013), 409–468.
Quoted from FormalConjectures/ErdosProblems/210.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/210.
The file states 10 research or textbook statements: 10 solved. It also has 23 API statements, counted here but not shown.
Erdos210.erdos_210.parts.i
Solved: stated here without proof.
Let \(f(n)\) be the sharp guarantee such that, for any \(n\) points in \(\mathbb R^2\), not all on a line, there are at least \(f(n)\) lines which contain exactly two points (called ordinary lines). Does \(f(n)\to\infty\)? That \(f(n)\to\infty\) was proved by Motzkin [Mo51].
theorem erdos_210.parts.i : Tendsto f atTop atTop
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/210.lean, line 52.
Erdos210.erdos_210.lower_bound
Solved: stated here without proof.
Kelly and Moser [KeMo58] proved that \(f(n)\geq 3n/7\) for all \(n\). Only \(n\geq3\) have noncollinear configurations.
theorem erdos_210.lower_bound : ∀ n : ℕ, 3 ≤ n → 3 * n ≤ 7 * f n
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/210.lean, line 58.
Erdos210.erdos_210.variants.csima_sawyer
Solved: stated here without proof.
Csima and Sawyer [CsSa93] proved \(f(n)\geq6n/13\) when \(n\geq8\).
theorem erdos_210.variants.csima_sawyer : ∀ n : ℕ, 8 ≤ n → 6 * n ≤ 13 * f n
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/210.lean, line 63.
Erdos210.erdos_210.variants.green_tao
Solved: stated here without proof.
Green and Tao [GrTa13] proved \(f(n)\geq n/2\) for sufficiently large \(n\).
theorem erdos_210.variants.green_tao : ∀ᶠ n : ℕ in atTop, n ≤ 2 * f n
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/210.lean, line 68.
Erdos210.erdos_210.variants.green_tao_odd
Solved: stated here without proof.
Green and Tao [GrTa13] proved \(f(n)\geq3\lfloor n/4\rfloor\) for sufficiently large odd \(n\) [GrTa13, Theorem 2.2].
theorem erdos_210.variants.green_tao_odd :
∀ᶠ n : ℕ in atTop, Odd n → 3 * (n / 4) ≤ f n
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/210.lean, line 74.
Erdos210.erdos_210.variants.even_upper_bound
Solved: stated here without proof.
Green and Tao [GrTa13, Proposition 2.1] give configurations attaining \(n/2\) ordinary lines for sufficiently large even \(n\).
theorem erdos_210.variants.even_upper_bound :
∀ᶠ n : ℕ in atTop, Even n → 2 * f n ≤ n
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/210.lean, line 81.
Erdos210.erdos_210.variants.seven
Solved: stated here without proof.
Kelly and Moser [KeMo58] give a seven-point configuration with three ordinary lines, attaining their lower bound at \(n=7\).
theorem erdos_210.variants.seven : f 7 = 3
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/210.lean, line 88.
Erdos210.erdos_210.variants.sylvester_gallai
Proved here.
The Sylvester–Gallai theorem states that \(f(n)\geq1\).
theorem erdos_210.variants.sylvester_gallai {n : ℕ} (hn : 3 ≤ n) : 1 ≤ f n
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/210.lean, line 151.
Erdos210.erdos_210.upper_bound
Proved here.
An explicit near-pencil gives the linear upper bound \(f(n)\leq n\).
theorem erdos_210.upper_bound {n : ℕ} (hn : 3 ≤ n) : f n ≤ n
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/210.lean, line 278.
Erdos210.erdos_210.parts.ii
Solved: stated here without proof.
How fast does \(f(n)\) tend to infinity? Kelly–Moser [KeMo58] and the near-pencil construction show that its growth is linear.
theorem erdos_210.parts.ii :
(fun n : ℕ => (f n : ℝ)) =Θ[atTop] (fun n : ℕ => (n : ℝ))
Category research solved; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/210.lean, line 285.
Sources
TheoremErdős Problem 211#
References: - erdosproblems.com/211 - [Be83] Beck, József, On the lattice property of the plane and some problems of Dirac, Motzkin and Erdős in combinatorial geometry. Combinatorica (1983), 281-297. - [SzTr83] Szemerédi, Endre and Trotter, Jr., William T., Extremal problems in discrete geometry. Combinatorica (1983), 381-392. - [Er84] Erdős, P., Research problems. Period. Math. Hungar. (1984), 101-103. - [BGS74] Burr, Stefan A. and Grünbaum, Branko and Sloane, N. J. A., The orchard problem. Geometriae Dedicata (1974), 397-424. - [FuPa84] Füredi, Z. and Palásti, I., Arrangements of lines with a large number of triangles. Proc. Amer. Math. Soc. (1984), 561-566.
Quoted from FormalConjectures/ErdosProblems/211.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/211.
The file states 4 research or textbook statements: 1 open and 3 solved. It also has 12 API statements, counted here but not shown.
Erdos211.erdos_211.variants.one_sixth
Open: stated without proof.
Erdős speculates that there are at least \((1+o(1))kn/6\) determined lines [Er84]. The asymptotic bound is uniform over \(1 \leq k < n\).
theorem erdos_211.variants.one_sixth :
∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ (n k : ℕ), N ≤ n → 1 ≤ k → k < n →
∀ s : Finset ℝ², s.card = n →
(∀ L : AffineSubspace ℝ ℝ², IsLine L → (s.filter fun p => p ∈ L).card ≤ n - k) →
(1 - ε) / 6 * (k : ℝ) * (n : ℝ) ≤ ((determinedLines s).card : ℝ)
Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/211.lean, line 67.
Erdos211.erdos_211.variants.sharpness
Solved: stated here without proof.
There are arbitrarily large configurations with no four collinear points and \(\sim n^2/6\) three-point lines, constructed by Burr, Grünbaum, and Sloane [BGS74] and Füredi and Palásti [FuPa84]. The index need not equal the number of points.
theorem erdos_211.variants.sharpness :
∃ s : ℕ → Finset ℝ²,
Tendsto (fun i => (s i).card) atTop atTop ∧
(∀ (i : ℕ) (L : AffineSubspace ℝ ℝ²), IsLine L →
((s i).filter fun p => p ∈ L).card ≤ 3) ∧
Tendsto (fun i =>
(((determinedLines (s i)).filter fun L => ((s i).filter fun p => p ∈ L).card = 3).card : ℝ) /
((s i).card : ℝ) ^ 2) atTop (nhds (1 / 6 : ℝ))
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/211.lean, line 79.
Erdos211.erdos_211
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos211.lean#L900.
Let \(1\leq k\lt n\). Given \(n\) points in \(\mathbb{R}^2\), at most \(n-k\) on any line, there are \(\gg kn\) many lines which contain at least two points. Solved by Beck [Be83] and Szemerédi and Trotter [SzTr83].
theorem erdos_211 : MainBound
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/211.lean, line 266.
Erdos211.erdos_211.variants.quadratic
Proved here.
Given any \(2n\) points with at most \(n\) on a line there are \(\gg n^2\) many lines formed by the points. Solved by Beck [Be83] and Szemerédi and Trotter [SzTr83].
theorem erdos_211.variants.quadratic : QuadraticBound
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/211.lean, line 272.
Sources
TheoremErdős Problem 212#
Reference: erdosproblems.com/212
Quoted from FormalConjectures/ErdosProblems/212.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/212.
The file states 1 research or textbook statement: 1 open.
Erdos212.erdos_212
Open: stated without proof.
Is there a dense subset of ℝ^2 such that all pairwise distances are rational?
theorem erdos_212 :
∃ u : Set ℂ, Dense u ∧ u.Pairwise fun c₁ c₂ => dist c₁ c₂ ∈ Set.range Rat.cast
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/212.lean, line 35.
Sources
TheoremErdős Problem 213#
Reference: erdosproblems.com/213
Quoted from FormalConjectures/ErdosProblems/213.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/213.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos213.erdos_213
Open: stated without proof.
Let \(n \geq 4\). Are there \(n\) points in \(\mathbb{R}^2\), no three on a line and no four on a circle, such that all pairwise distances are integers?
theorem erdos_213 : ∀ n : ℕ, n ≥ 4 → Erdos213For n
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/213.lean, line 47.
Erdos213.erdos_213.variants.KK08
Solved: stated here without proof.
The best construction to date, due to Kreisel and Kurz, has \(n = 7\).
theorem erdos_213.variants.KK08 : Erdos213For 7
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/213.lean, line 53.
Sources
TheoremErdős Problem 214#
References: - erdosproblems.com/214 - [CsTo94] Csizmadia, György and Tóth, Géza, Note on a Ramsey-type problem in geometry. J. Combin. Theory Ser. A (1994), 302-306. - [EGMRSS75] Erdős, P. and Graham, R. L. and Montgomery, P. and Rothschild, B. L. and Spencer, J. and Straus, E. G., Euclidean Ramsey theorems. II. (1975), 529-557. - [Ju79] Juhász, Rozália, Ramsey type theorems in the plane. J. Combin. Theory Ser. A (1979), 152-160.
Quoted from FormalConjectures/ErdosProblems/214.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/214.
The file states 6 research or textbook statements: 6 solved.
Erdos214.erdos_214
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos214.lean.
Let \(S\subset \mathbb{R}^2\) be such that no two points in \(S\) are distance \(1\) apart. Must the complement of \(S\) contain four points which form a unit square?
The answer is yes, proved by Juhász [Ju79], who proved more generally that the complement of \(S\) must contain a congruent copy of any set of four points.
theorem erdos_214 :
∀ S : Set ℝ², UnitDistanceAvoiding S →
∃ p : Fin 4 → ℝ², (∀ i, p i ∈ Sᶜ) ∧ (p ≅ unitSquare)
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/214.lean, line 65.
Erdos214.erdos_214.variants.juhasz
Solved: stated here without proof.
The answer is yes, proved by Juhász [Ju79], who proved more generally that the complement of \(S\) must contain a congruent copy of any set of four points.
theorem erdos_214.variants.juhasz : HasRedCopies 4
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/214.lean, line 75.
Erdos214.erdos_214.variants.egmrss
Solved: stated here without proof.
Erdős, Graham, Montgomery, Rothschild, Spencer, and Straus [EGMRSS75] had earlier showed that \(3\leq k\leq 10^{12}\).
theorem erdos_214.variants.egmrss : 3 ≤ k ∧ k ≤ 10 ^ 12
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/214.lean, line 83.
Erdos214.erdos_214.variants.juhasz_twelve_points
Solved: stated here without proof.
Juhász [Ju79] also improved the upper bound to \(k\leq 11\).
theorem erdos_214.variants.juhasz_twelve_points : ¬ HasRedCopies 12
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/214.lean, line 90.
Erdos214.erdos_214.variants.csizmadia_toth
Solved: stated here without proof.
The upper bound was improved further by Csizmadia and Tóth [CsTo94] to \(k\leq 7\).
theorem erdos_214.variants.csizmadia_toth : ¬ HasRedCopies 8
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/214.lean, line 97.
Erdos214.erdos_214.variants.bounds
Solved: stated here without proof.
The best known bounds currently are
\[4\leq k\leq 7.\]
theorem erdos_214.variants.bounds : 4 ≤ k ∧ k ≤ 7
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/214.lean, line 105.
Sources
TheoremErdős Problem 215#
References: - erdosproblems.com/215 - [Er83c] Erdős, Paul, Combinatorial problems in geometry. Math. Chronicle (1983), 35-54. - [JaMa02] Jackson, Steve and Mauldin, R. Daniel, Sets meeting isometric copies of the lattice \(\mathbb{Z}^2\) in exactly one point. Proc. Natl. Acad. Sci. USA (2002), 15883-15887.
Quoted from FormalConjectures/ErdosProblems/215.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/215.
The file states 1 research or textbook statement: 1 solved.
Erdos215.erdos_215
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos215.lean#L55.
Does there exist \(S\subseteq \mathbb{R}^2\) such that every set congruent to \(S\) (that is, \(S\) after some translation and rotation) contains exactly one point from \(\mathbb{Z}^2\)?
An old question of Steinhaus. Erdős was 'almost certain that such a set does not exist'.
In fact, such a set does exist, as proved by Jackson and Mauldin [JaMa02]. Their construction depends on the axiom of choice.
The plane is identified with \(\mathbb{C}\): the sets congruent to \(S\) are the sets \(uS + t\) with \(\lvert u\rvert = 1\) and \(t \in \mathbb{C}\), and \(\mathbb{Z}^2\) is the set of Gaussian integers.
theorem erdos_215 : ∃ S : Set ℂ, ∀ u t : ℂ, ‖u‖ = 1 →
∃! z : ℂ, z ∈ (fun w => u * w + t) '' S ∧ ∃ a b : ℤ, z = a + b * Complex.I
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/215.lean, line 49.
Sources
TheoremErdős Problem 217#
Reference: Erdős Problem 217
Quoted from FormalConjectures/ErdosProblems/217.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/217.
The file states 1 research or textbook statement: 1 open.
Erdos217.erdos_217
Open: stated without proof.
For which \(n\) do there exist \(n\) points in \(\mathbb{R}^2\), no three on a line and no four on a circle, that determine \(n-1\) distinct distances whose multiplicities are \(1,2,\ldots,n-1\)? The condition \(n>0\) excludes the empty configuration, since the requested number \(n-1\) of distances is nonnegative.
theorem erdos_217 : erdos_217.answer = {n : ℕ | 0 < n ∧ ∃ P : Finset ℝ²,
P.card = n ∧ InGeneralPosition (P : Set ℝ²) ∧
(distanceSet P).card = n - 1 ∧
(distanceSet P).image (distanceMultiplicity P) = Finset.Icc 1 (n - 1)}
Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/217.lean, line 40.
Sources
TheoremErdős Problem 218#
Reference: erdosproblems.com/218
Quoted from FormalConjectures/ErdosProblems/218.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/218.
The file states 3 research or textbook statements: 3 open.
Erdos218.erdos_218.variants.le
Open: stated without proof.
The set of indices \(n\) for which a prime gap is followed by a larger or equal prime gap has a natural density of \(\frac 1 2\).
theorem erdos_218.variants.le : {n | primeGap n ≤ primeGap (n + 1)}.HasDensity <| 1 / 2
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/218.lean, line 35.
Erdos218.erdos_218.variants.ge
Open: stated without proof.
The set of indices \(n\) for which a prime gap is preceded by a larger or equal prime gap has a natural density of \(\frac 1 2\).
theorem erdos_218.variants.ge : {n | primeGap (n + 1) ≤ primeGap n}.HasDensity <| 1 / 2
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/218.lean, line 43.
Erdos218.erdos_218.variants.infinite_equal_prime_gap
Open: stated without proof.
There are infinitely many indices \(n\) such that the prime gap at \(n\) is equal to the prime gap at \(n+1\). This is equivalent to the existence of infinitely many arithmetic progressions of length \(3\), see
erdos_141.variants.infinite_three.
theorem erdos_218.variants.infinite_equal_prime_gap : {n | primeGap n = primeGap (n + 1)}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/218.lean, line 52.
Sources
TheoremErdős Problem 219#
Reference: erdosproblems.com/219
Quoted from FormalConjectures/ErdosProblems/219.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/219.
The file states 1 research or textbook statement: 1 solved. It also has 2 test statements and 3 API statements, counted here but not shown.
Erdos219.erdos_219
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1268917deaaaa0d674f651287027baa26cea9920/src/latest/ErdosProblems/Erdos219.lean.
Are there arbitrarily long arithmetic progressions of primes? Solution: yes. Ref: Green, Ben and Tao, Terence, The primes contain arbitrarily long arithmetic progressions
theorem erdos_219 : ∀ N : ℕ, ∃ l ∈ primeArithmeticProgressions, N ≤ ENat.card l
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/219.lean, line 81.
Sources
TheoremErdős Problem 220#
References: - erdosproblems.com/220 - [Er40] Erdős, P., The difference of consecutive primes. Duke Math. J. (1940), 438--441. - [Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [MoVa86] Montgomery, H. L. and Vaughan, R. C., On the distribution of reduced residues. Ann. of Math. (2) (1986), 311-333. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.
Quoted from FormalConjectures/ErdosProblems/220.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/220.
The file states 1 research or textbook statement: 1 solved.
Erdos220.erdos_220
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos220.lean#L39.
Let \(n \geq 1\) and
\[A = \{a_1 < \cdots < a_{\phi(n)}\} = \{1 \leq m < n : (m, n) = 1\}.\]Is it true that
\[\sum_{1 \leq k < \phi(n)} (a_{k+1} - a_k)^2 \ll \frac{n^2}{\phi(n)}?\]A problem of Erdős [Er40, Er73, ErGr80], which is discussed in problem B40 of Guy's collection [Gu04]. The answer is yes, as proved by Montgomery and Vaughan [MoVa86], who in fact proved that \(\sum_{1 \leq k < \phi(n)} (a_{k+1} - a_k)^\gamma \ll n^\gamma / \phi(n)^{\gamma - 1}\) for every \(\gamma \geq 1\).
theorem erdos_220 :
∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 1 ≤ n →
(sumSquaredGaps (sortedTotatives n) : ℝ) ≤ C * (n : ℝ) ^ 2 / (n.totient : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/220.lean, line 64.
Sources
TheoremErdős Problem 221#
References: - erdosproblems.com/221 - [Lo54] Lorentz, G. G., On a problem of additive number theory. Proc. Amer. Math. Soc. (1954), 838-841. - [Ru72] Ruzsa, Jr., I., On a problem of P. Erdős. Canad. Math. Bull. (1972), 309-310.
Quoted from FormalConjectures/ErdosProblems/221.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/221.
The file states 1 research or textbook statement: 1 solved.
Erdos221.erdos_221
Solved: stated here; a Lean proof is at https://github.com/Woett/Lean-files/blob/main/ErdosProblem221.lean.
Is there a set \(A\subset\mathbb{N}\) such that, for all large \(N\),
\[\lvert A\cap\{1,\ldots,N\}\rvert \ll N/\log N\]and such that every large integer can be written as \(2^k+a\) for some \(k\geq 0\) and \(a\in A\)?
Lorentz [Lo54] proved there is such a set with, for all large \(N\),
\[\lvert A\cap\{1,\ldots,N\}\rvert \ll \frac{\log\log N}{\log N}N\]The answer is yes, proved by Ruzsa [Ru72].
theorem erdos_221 :
∃ A : Set ℕ,
((fun N => ({a ∈ A | a ≤ N}.ncard : ℝ)) ≪ (fun N => (N : ℝ) / Real.log N)) ∧
∀ᶠ N in atTop, ∃ k a, 0 ≤ k ∧ a ∈ A ∧ N = 2 ^ k + a
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/221.lean, line 47.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.