Erdős Problem 89 to Erdős Problem 99
TheoremErdős Problem 89#
References: - erdosproblems.com/89 - [Er46] Erdős, Paul. On sets of distances of \(n\) points. Amer. Math. Monthly 53 (1946), 248--250. - [GuKa15] Guth, Larry and Katz, Nets Hawk. On the Erdős distinct distances problem in the plane. Ann. of Math. (2) 181 (2015), 155--190. - [Mo52] Moser, Leo. On the different distances determined by \(n\) points. Amer. Math. Monthly 59 (1952), 85--91.
AI disclosure
Lean 4 code in this file was drafted with assistance from OpenAI Codex. The mathematical content and references are the author's own work.
Quoted from FormalConjectures/ErdosProblems/89.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/89.
The file states 3 research or textbook statements: 1 open and 2 solved. It also has 1 test statement, counted here but not shown.
Erdos89.erdos_89
Open: stated without proof.
Erdős [Er46] asked whether every set of \(n\) distinct points in \(\mathbb{R}^2\) determines \(\gg \frac{n}{\sqrt{\log n}}\) many distinct distances.
theorem erdos_89 :
(fun (n : ℕ) => n/(n : ℝ).log.sqrt) =O[atTop]
(fun n => (minimalDistinctDistances ℝ² n : ℝ))
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/89.lean, line 50.
Erdos89.erdos_89.variants.n_dvd_log_n
Solved: stated here without proof.
Guth and Katz [GuKa15] proved that there are always \(\gg \frac{n}{\log n}\) many distinct distances.
theorem erdos_89.variants.n_dvd_log_n :
(fun (n : ℕ) => n/(n : ℝ).log) =O[atTop]
(fun n => (minimalDistinctDistances ℝ² n : ℝ))
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/89.lean, line 60.
Erdos89.erdos_89.variants.grid_upper_bound
Solved: stated here without proof.
The square grid construction, going back to Erdős and Moser, shows that \(\frac{n}{\sqrt{\log n}}\) is the correct order if the conjecture is true: there are configurations whose number of distinct distances is \(O(\frac{n}{\sqrt{\log n}})\).
theorem erdos_89.variants.grid_upper_bound :
(fun n => (minimalDistinctDistances ℝ² n : ℝ)) =O[atTop]
(fun (n : ℕ) => n/(n : ℝ).log.sqrt)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/89.lean, line 72.
Sources
TheoremErdős Problem 90: The unit distance problem#
Reference: erdosproblems.com/90
The conjecture asks whether every set of \(n\) points in \(\mathbb{R}^2\) determines at most \(n^{1 + O(1/\log\log n)}\) unit distances. It was disproved in May 2026: an internal model at OpenAI produced a construction beating the conjectured bound, with the proof digested and human-verified in two arXiv papers:
- W. Sawin, An explicit lower bound for the unit distance problem (2026), giving \(u(n) \ge n^{1.014114}/C\) for infinitely many \(n\);
- N. Alon, T. F. Bloom, W. T. Gowers, D. Litt, W. Sawin, A. Shankar, J. Tsimerman, V. Wang and M. Matchett Wood, Remarks on the disproof of the unit distance conjecture (2026), giving the qualitative form \(u(n) \ge n^{1+\varepsilon}\) for some \(\varepsilon > 0\).
This file records the main statement (
erdos_90), the two constructive disproof variants, the logical implications between them, and the load-bearing reductions of Sawin's proof (sawin_lattice_reductionandsawin_totally_real_tower) as further benchmark challenges.
Quoted from FormalConjectures/ErdosProblems/90.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/90.
The file states 5 research or textbook statements: 5 solved. It also has 3 test statements, counted here but not shown.
Erdos90.erdos_90
Solved: stated here without proof.
Does every set of \(n\) distinct points in \(\mathbb{R}^2\) contain at most \(n^{1+O(\frac{1}{\log\log n})}\) many pairs which are distance \(1\) apart?
This was disproved by an internal model at OpenAI, which constructed (for infinitely many \(n\)) a set \(P\) of \(n\) points in \(\mathbb{R}^2\) such that the number of unit distance pairs in \(P\) is at least \(n^{1+c}\), where \(c > 0\) is an absolute constant.
theorem erdos_90 : ¬ ∃ (O : ℕ → ℝ) (hO : O =O[atTop] (fun n => 1 / (n : ℝ).log.log)),
(fun n => (maxUnitDistances n : ℝ)) =ᶠ[atTop] fun (n : ℕ) => (n : ℝ) ^ (1 + O n)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/90.lean, line 86.
Erdos90.erdos_90.variants.polynomial_lower_bound
Solved: stated here; a Lean proof is at https://github.com/plby/Erdos90/blob/2062b0e6c9770c81e397bfe41148e90b92ca0567/src/submission/Solution.lean#L6.
Constructive form of the disproof. There is an absolute constant \(c > 0\) such that infinitely many \(n\) admit a configuration realising at least \(n^{1+c}\) unit distances.
This is the qualitative content of Theorem 1.1 of Alon–Bloom–Gowers–Litt–Sawin–Shankar– Tsimerman–Wang–Matchett Wood, Remarks on the disproof of the unit distance conjecture (2026). An explicit bound \(c \ge 0.014114\) is given by Sawin, An explicit lower bound for the unit distance problem (2026); see
erdos_90.variants.sawin_explicitbelow.
theorem erdos_90.variants.polynomial_lower_bound :
∃ c > (0 : ℝ),
{n : ℕ | (n : ℝ) ^ (1 + c) ≤ (maxUnitDistances n : ℝ)}.Infinite
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/90.lean, line 103.
Erdos90.erdos_90.variants.sawin_explicit
Solved: stated here without proof.
Sawin's explicit exponent. The constructive disproof can be realised with \(c \ge 0.014114\) (absorbing the implicit constant \(C\) of Sawin's Theorem 1 into a slightly smaller exponent for all large enough \(n\)). Reference: Theorem 1 of Sawin, arXiv:2605.20579 (2026).
theorem erdos_90.variants.sawin_explicit :
{n : ℕ | (n : ℝ) ^ (1.014114 : ℝ) ≤ (maxUnitDistances n : ℝ)}.Infinite
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/90.lean, line 115.
Erdos90.sawin_lattice_reduction
Solved: stated here without proof.
Sawin's Lemma 2: lattice geometry of unit distances (Sawin, arXiv:2605.20579).
Let \(d \ge 1\), \(R > 1\), and suppose \(\Lambda \subset \mathbb{R}^{2d}\) is an additive subgroup all of whose nonzero vectors have norm at least \(\rho > 0\) (so \(\Lambda\) is a lattice; Sawin takes \(\rho\) to be the norm of a shortest nonzero vector of \(\Lambda\)), equipped with an additive embedding \(\pi : \Lambda \to \mathbb{R}^2\). Suppose \(S \subseteq \Lambda\) is a finite set of "matching" vectors satisfying \(\|v\| \le 1\) and \(\|\pi v\| = 1\) for every \(v \in S\). Then there is a finite point set \(U \subset \mathbb{R}^2\) of size \(\#U \le (2R/\rho + 1)^{2d}\) whose unit-distance density is at least \((1 - 1/R)^{2d}\,\#S\), i.e. \((1-1/R)^{2d}\,\#S\,\#U \le \#\{(u_1, u_2) \in U^2 : |u_1 - u_2| = 1\}\). The right-hand side counts ordered pairs, so it equals twice
unitDistNum U.This pure geometry-of-numbers reduction is the elementary heart of the disproof.
theorem sawin_lattice_reduction
(d : ℕ) (hd : 1 ≤ d) (R : ℝ) (hR : 1 < R)
(Λ : Submodule ℤ (EuclideanSpace ℝ (Fin (2*d))))
(ρ : ℝ) (hρ : 0 < ρ) (hΛ : ∀ v : Λ, v ≠ 0 → ρ ≤ ‖(v : EuclideanSpace ℝ (Fin (2*d)))‖)
(π : Λ →+ ℝ²) (hπ : Function.Injective π)
(S : Finset Λ)
(hS_norm : ∀ v ∈ S, ‖(v : EuclideanSpace ℝ (Fin (2*d)))‖ ≤ 1)
(hS_proj : ∀ v ∈ S, ‖π v‖ = 1) :
∃ U : Finset ℝ², 0 < U.card ∧ (U.card : ℝ) ≤ (2 * R / ρ + 1) ^ (2*d) ∧
((1 : ℝ) - 1/R) ^ (2*d) * (S.card : ℝ) * (U.card : ℝ) ≤
2 * (unitDistNum U : ℝ)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/90.lean, line 168.
Erdos90.sawin_totally_real_tower
Solved: stated here; a Lean proof is at https://github.com/n-yamaguchi-0729/SawinTotallyRealTowers/blob/3a455e1aa9140dbbe7b7d68f508392a69c86d0f4/Lean4/SawinTotallyRealTowers/SawinTotallyRealTower.lean#L31.
Sawin's Lemmas 11–12 / Remarks Proposition 2.3: the totally real tower.
There exist \(rdBound : \mathbb{R}\) and a single infinite set \(Q\) of rational primes \(q \equiv 1 \pmod 4\) such that for every \(N\) one can find a totally real number field \(F/\mathbb{Q}\) of degree \(\ge N\) with bounded root discriminant \(|disc F|^{1/[F:\mathbb{Q}]} \le rdBound\) in which every prime \(q \in Q\) splits completely.
The load-bearing feature is the quantifier order: \(Q\) is fixed before \(F\), so the same primes split completely in fields of unbounded degree. (For a single fixed \(F\), Chebotarev already gives infinitely many completely split primes \(\equiv 1 \pmod 4\), so a per-field statement would be vacuous.) This uniform splitting in an unbounded tower is the key arithmetic input to the disproof. It is proved as Lemmas 11–12 of Sawin, arXiv:2605.20579, and as Proposition 2.3 of the Remarks paper, via the Golod–Shafarevich inequality for pro-\(2\) groups together with the Hajir–Maire–Ramakrishna (2003) tower construction.
A "completely split" rational prime \(q\) in \(F\) is one for which \((q)\) is the product of exactly \([F:\mathbb{Q}]\) distinct maximal ideals.
theorem sawin_totally_real_tower :
∃ (rdBound : ℝ) (Q : Set ℕ), Q.Infinite ∧ (∀ q ∈ Q, q.Prime ∧ q % 4 = 1) ∧
∀ N : ℕ, ∃ (F : Type) (_ : Field F) (_ : CharZero F) (_ : NumberField F)
(_ : IsTotallyReal F),
N ≤ Module.finrank ℚ F ∧
(|(NumberField.discr F : ℝ)|) ^ ((1 : ℝ) / Module.finrank ℚ F) ≤ rdBound ∧
∀ q ∈ Q, ∃ (factors : Finset (Ideal (𝓞 F))),
factors.card = Module.finrank ℚ F ∧
∀ p ∈ factors, p.IsMaximal ∧ (q : 𝓞 F) ∈ p
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/90.lean, line 204.
Sources
TheoremErdős Problem 91#
Reference: - [Er87b] Erdős, P., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985) (1987), 167-177. - [Ko24c] Z. Kovács, A note on Erdős's mysterious remark. arXiv:2412.05190 (2024). - erdosproblems.com/91
Quoted from FormalConjectures/ErdosProblems/91.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/91.
The file states 8 research or textbook statements: 1 open and 7 solved. It also has 6 test statements, counted here but not shown.
Erdos91.erdos_91
Open: stated without proof.
Suppose \(A\subset \mathbb{R}^2\) has \(\lvert A\rvert=n\) and minimises the number of distinct distances between points in \(A\). Prove that for large \(n\) there are at least two (and probably many) such \(A\) which are non-similar.
theorem erdos_91 :
∀ᶠ n : ℕ in atTop, ¬ UniqueMinimizer n
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/91.lean, line 150.
Erdos91.erdos_91.variants.three
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/cd3cf0b176e95209584bf35555a7c0e501255f6e/erdos-91/Solution.lean#L159.
For \(n = 3\) the equilateral triangle is the only such set.
theorem erdos_91.variants.three : UniqueMinimizer 3
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/91.lean, line 161.
Erdos91.erdos_91.variants.four
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/cd3cf0b176e95209584bf35555a7c0e501255f6e/erdos-91/Solution.lean#L162.
For \(n=4\) the square or two equilateral triangles sharing an edge give two non-similar examples.
theorem erdos_91.variants.four : ¬ UniqueMinimizer 4
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/91.lean, line 172.
Erdos91.erdos_91.variants.five
Solved: stated here without proof.
For \(n = 5\) the regular pentagon is the unique such set (which has two distinct distances). Erdős mysteriously remarks in [Er90] this was proved by 'a colleague'. (In [Er87b] this is described as 'a colleague from Zagreb (unfortunately I do not have his letter)'.) A published proof of this fact is provided by Kovács [Ko24c].
theorem erdos_91.variants.five : UniqueMinimizer 5
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/91.lean, line 183.
Erdos91.erdos_91.variants.six
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/cd3cf0b176e95209584bf35555a7c0e501255f6e/erdos-91/Solution.lean#L165.
In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for \(n = 6\).
theorem erdos_91.variants.six: ¬ UniqueMinimizer 6
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/91.lean, line 192.
Erdos91.erdos_91.variants.seven
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/cd3cf0b176e95209584bf35555a7c0e501255f6e/erdos-91/Solution.lean#L168.
In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for \(n = 7\).
theorem erdos_91.variants.seven: ¬ UniqueMinimizer 7
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/91.lean, line 202.
Erdos91.erdos_91.variants.eight
Solved: stated here without proof.
In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for \(n = 8\).
theorem erdos_91.variants.eight: ¬ UniqueMinimizer 8
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/91.lean, line 210.
Erdos91.erdos_91.variants.nine
Solved: stated here without proof.
In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for \(n = 9\).
theorem erdos_91.variants.nine: ¬ UniqueMinimizer 9
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/91.lean, line 218.
Sources
TheoremErdős Problem 92#
Both questions here are disproved, by way of Erdős Problem 90. The source says so directly: this is a stronger form of the unit distance conjecture, so the disproof of that conjecture disproves these too. See
FormalConjectures.ErdosProblems.«90».Reference: erdosproblems.com/92
Quoted from FormalConjectures/ErdosProblems/92.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/92.
The file states 2 research or textbook statements: 2 solved. It also has 1 test statement, counted here but not shown.
Erdos92.erdos_92.variants.weak
Solved: stated here without proof.
Is it true that \(f(n)\leq n^{o(1)}\)?
The source records this as disproved: "This is a stronger form of the unit distance conjecture (see [90]). As such the recent disproof of [90] also disproves this." That disproof is
Erdos90.erdos_90, which this repository already records asresearch solvedwith the answerFalse.
theorem erdos_92.variants.weak : ¬ ∃ o : ℕ → ℝ,
o =o[atTop] (1 : ℕ → ℝ) ∧ ∀ n, (f n : ℝ) ≤ n^(o n)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/92.lean, line 95.
Erdos92.erdos_92.variants.strong
Solved: stated here without proof.
Or even \(f(n) < n^{c/\log\log n}\) for some constant \(c > 0\)?
Also disproved, and by the weak form rather than separately: since \(c/\log\log n \to 0\), the bound \(n^{c/\log\log n}\) is of the form \(n^{o(1)}\), so this statement implies
erdos_92.variants.weakand is false whenever that one is.
theorem erdos_92.variants.strong :
¬ ∃ c > 0, ∀ᶠ n in atTop, (f n : ℝ) ≤ n^(c / (n : ℝ).log.log)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/92.lean, line 107.
Sources
TheoremErdős Problem 93#
References: - erdosproblems.com/93 - [Er46b] Erdős, P., On sets of distances of {\(n\)} points. Amer. Math. Monthly (1946), 248--250. - [Er57] Erdős, Paul, Some unsolved problems. Michigan Math. J. (1957), 291-300. - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Er75f] Erdős, Paul, On some problems of elementary and combinatorial geometry. Ann. Mat. Pura Appl. (4) (1975), 99-108. - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79. - [Er87b] Erdős, P., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985) (1987), 167-177. - [Er90] Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467-478. - [Er92e] Erdős, Pál, Some Unsolved problems in Geometry, Number Theory and Combinatorics. Eureka (1992), 44-48. - [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186. - [Er97e] Erdős, Paul, Some of my favourite unsolved problems. Math. Japon. (1997), 527-537. - [Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10. - [Al63] Altman, E., On a problem of P. Erdős. Amer. Math. Monthly (1963), 148-157.
Quoted from FormalConjectures/ErdosProblems/93.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/93.
The file states 1 research or textbook statement: 1 solved.
Erdos93.erdos_93
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos93.lean.
If \(n\) distinct points in \(\mathbb{R}^2\) form a convex polygon then they determine at least \(\lfloor \frac{n}{2}\rfloor\) distinct distances.
Solved by Altman [Al63].
theorem erdos_93 (A : Finset ℝ²) (hA : ConvexIndep (A : Set ℝ²)) :
A.card / 2 ≤ distinctDistances A
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/93.lean, line 61.
Sources
TheoremErdős Problem 94#
References: - erdosproblems.com/94 - [Er92e] Erdős, Pál, Some Unsolved problems in Geometry, Number Theory and Combinatorics. Eureka (1992), 44-48. - [Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67. - [LeTh95] Lefmann, Hanno and Thiele, Torsten, Point sets with distinct distances. Combinatorica (1995), 379-408.
Quoted from FormalConjectures/ErdosProblems/94.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/94.
The file states 3 research or textbook statements: 1 open and 2 solved. It also has 1 test statement, counted here but not shown.
Erdos94.erdos_94
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos94.lean.
Suppose \(n\) points in \(\mathbb{R}^2\) determine a convex polygon and the set of distances between them is \(\{u_1,\ldots,u_t\}\). Suppose \(u_i\) appears as the distance between \(f(u_i)\) many pairs of points. Then
\[\sum_i f(u_i)^2 \ll n^3.\]In [Er97c] Erdős claims that Fishburn solved this, but gives no reference.
theorem erdos_94 : ∃ C > (0 : ℝ), ∀ P : Finset ℝ², ConvexIndep (P : Set ℝ²) →
∑ u ∈ distanceSet P, (distanceMultiplicity P u : ℝ) ^ 2 ≤ C * (P.card : ℝ) ^ 3
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/94.lean, line 54.
Erdos94.erdos_94.variants.no_three_on_a_line
Solved: stated here without proof.
Lefmann and Theile [LeTh95] prove a stronger version of this question, that
\[\sum_i f(u_i)^2 \ll n^3\]under the weaker assumption that no three points are on a line.
theorem erdos_94.variants.no_three_on_a_line : ∃ C > (0 : ℝ), ∀ P : Finset ℝ²,
NonTrilinear (P : Set ℝ²) →
∑ u ∈ distanceSet P, (distanceMultiplicity P u : ℝ) ^ 2 ≤ C * (P.card : ℝ) ^ 3
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/94.lean, line 72.
Erdos94.erdos_94.variants.regular_ngon
Open: stated without proof.
Erdős and Fishburn also make the stronger conjecture that \(\sum f(u_i)^2\) is maximal for the regular \(n\)-gon (for large enough \(n\)).
theorem erdos_94.variants.regular_ngon : ∀ᶠ n : ℕ in atTop, ∀ P : Finset ℝ²,
P.card = n → ConvexIndep (P : Set ℝ²) →
∑ u ∈ distanceSet P, (distanceMultiplicity P u : ℝ) ^ 2 ≤
∑ u ∈ distanceSet (regularNGon n), (distanceMultiplicity (regularNGon n) u : ℝ) ^ 2
Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/94.lean, line 82.
Sources
TheoremErdős Problem 95#
References: - erdosproblems.com/95 - [Er92e] Erdős, Pál, Some Unsolved problems in Geometry, Number Theory and Combinatorics. Eureka (1992), 44-48. - [Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186. - [Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67. - [Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10. - [Al63] Altman, E., On a problem of P. Erdős. Amer. Math. Monthly (1963), 148-157. - [GuKa15] Guth, Larry and Katz, Nets Hawk, On the Erdős distinct distances problem in the plane. Ann. of Math. (2) (2015), 155-190.
Quoted from FormalConjectures/ErdosProblems/95.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/95.
The file states 2 research or textbook statements: 2 solved.
Erdos95.erdos_95
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos95.lean#L1005.
Let \(x_1,\ldots,x_n\in\mathbb{R}^2\) determine the set of distances \(\{u_1,\ldots,u_t\}\). Suppose \(u_i\) appears as the distance between \(f(u_i)\) many pairs of points. Then for all \(\epsilon>0\)
\[\sum_i f(u_i)^2 \ll_\epsilon n^{3+\epsilon}.\]The case when the points determine a convex polygon was solved by Altman [Al63]. Note it is trivial that \(\sum f(u_i)=\binom{n}{2}\).
Solved by Guth and Katz [GuKa15] who proved the upper bound
\[\sum_i f(u_i)^2 \ll n^3\log n.\]See also 94.
theorem erdos_95 : ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, 0 < C ∧ ∀ P : Finset ℝ²,
∑ u ∈ distanceSet P, (distanceMultiplicity P u : ℝ) ^ 2 ≤
C * (P.card : ℝ) ^ (3 + ε)
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/95.lean, line 60.
Erdos95.erdos_95.variants.guth_katz
Solved: stated here without proof.
Guth and Katz [GuKa15] proved the upper bound \(\sum_i f(u_i)^2 \ll n^3\log n\).
theorem erdos_95.variants.guth_katz : ∃ C : ℝ, 0 < C ∧ ∀ P : Finset ℝ², 2 ≤ P.card →
∑ u ∈ distanceSet P, (distanceMultiplicity P u : ℝ) ^ 2 ≤
C * (P.card : ℝ) ^ 3 * Real.log P.card
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/95.lean, line 67.
Sources
TheoremErdős Problem 96#
Reference: erdosproblems.com/96
Quoted from FormalConjectures/ErdosProblems/96.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/96.
The file states 1 research or textbook statement: 1 open. It also has 1 test statement, counted here but not shown.
Erdos96.erdos_96
Open: stated without proof.
If \(n\) points in \(\mathbb{R}^2\) form a convex polygon then there are \(O(n)\) many pairs which are distance \(1\) apart.
theorem erdos_96 :
(fun n => (maxConvexUnitDistances n : ℝ)) =O[atTop] fun n => (n : ℝ)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/96.lean, line 65.
Sources
TheoremErdős Problem 97#
Reference: erdosproblems.com/97
Quoted from FormalConjectures/ErdosProblems/97.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/97.
The file states 5 research or textbook statements: 2 open and 3 solved.
Erdos97.erdos_97
Open: stated without proof.
Does every convex polygon have a vertex with no other 4 vertices equidistant from it?
theorem erdos_97 :
∀ A : Finset ℝ², A.Nonempty → ConvexIndep A → ¬HasNEquidistantProperty 4 A
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/97.lean, line 79.
Erdos97.erdos_97.variants.three_equidistant
Solved: stated here without proof.
Erdős originally conjectured this (in [Er46b]) with no 3 vertices equidistant, but Danzer found a convex polygon on 9 points such that every vertex has three vertices equidistant from it (but this distance depends on the vertex). Danzer's construction is explained in [Er87b].
[Er46b] Erdős, P., On sets of distances of \(n\) points. Amer. Math. Monthly (1946), 248-250. [Er87b] Erdős, P., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985), 167-177.
theorem erdos_97.variants.three_equidistant :
∃ A : Finset ℝ², A.Nonempty ∧ ConvexIndep A ∧ HasNEquidistantProperty 3 A
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/97.lean, line 93.
Erdos97.erdos_97.variants.k_equidistant
Open: stated without proof.
Erdős also conjectured that there is a \(k\) for which every convex polygon has a vertex with no other \(k\) vertices equidistant from it.
theorem erdos_97.variants.k_equidistant :
∃ k : ℕ, ∀ A : Finset ℝ², A.Nonempty → ConvexIndep A → ¬HasNEquidistantProperty k A
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/97.lean, line 112.
Erdos97.erdos_97.variants.three_unit_distance
Solved: stated here without proof.
Fishburn and Reeds [FiRe92] have found a convex polygon on 20 points such that every vertex has three vertices equidistant from it (and this distance is the same for all vertices).
[FiRe92] Fishburn, P. C. and Reeds, J. A., Unit distances between vertices of a convex polygon. Comput. Geom. (1992), 81-91.
theorem erdos_97.variants.three_unit_distance :
∃ A : Finset ℝ², A.Nonempty ∧ ConvexIndep A ∧ HasNUnitDistanceProperty 3 A
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/97.lean, line 123.
Erdos97.erdos_97.variants.three_unit_distance_cut_min
Solved: stated here without proof.
Fishburn and Reeds [FiRe92] also proved that the smallest \(n\) for which there exists a convex \(n\)-gon and a cut \(\{A, B\}\) of its vertices such that \(|\{b \in B : d(a, b) = 1\}| ≥ 3\) for all \(a \in A\), and \(|\{a \in A : d(a, b) = 1\}| ≥ 3\) for all \(b \in B\), is \(n = 20\).
theorem erdos_97.variants.three_unit_distance_cut_min :
sInf {n : ℕ | ∃ (V : Finset ℝ²) (A B : Finset ℝ²),
n = V.card ∧ ConvexIndep V ∧ A.Nonempty ∧ B.Nonempty ∧ IsCut V A B ∧
HasNUnitDistancePointsOn 3 B A ∧ HasNUnitDistancePointsOn 3 A B} = 20
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/97.lean, line 140.
Sources
TheoremErdős Problem 98#
References: - [Er75f] Erdős, Paul, On some problems of elementary and combinatorial geometry. Ann. Mat. Pura Appl. (4) (1975), 99-108. - [Er83c] Erdős, Paul, Combinatorial problems in geometry. Math. Chronicle (1983), 35-54. - [Er87b] Erdős, P., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985) (1987), 167-177. - [Er90] Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467-478. - [Er92b] Erdős, Paul, Some of my favourite problems in various branches of combinatorics. Matematiche (Catania) (1992), 231-240. - [EFPR93] Erdős, Paul and Füredi, Zoltán and Pach, János and Ruzsa, Imre Z., The grid revisited. Discrete Math. (1993), 189-196. - [Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269. - [Er97e] Erdős, Paul, Some of my favourite unsolved problems. Math. Japon. (1997), 527-537. - erdosproblems.com/98
Quoted from FormalConjectures/ErdosProblems/98.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/98.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos98.erdos_98
Open: stated without proof.
Let \(h(n)\) be such that any \(n\) points in \(\mathbb{R}^2\), with no three on a line and no four on a circle, determine at least \(h(n)\) distinct distances. Does \(h(n)/n\to \infty\)?
theorem erdos_98 :
Tendsto (fun n : ℕ ↦ ((h n : ℝ) / (n : ℝ))) atTop atTop
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/98.lean, line 70.
Erdos98.erdos_98.variants.upper_bound
Solved: stated here without proof.
Erdős could not even prove \(h(n)\geq n\). Pach has shown \(h(n) < n^{\log_2 3}\). Erdős, Füredi, and Pach [EFPR93] have improved this to \(h(n) < n\exp(c\sqrt{\log n})\) for some constant \(c>0\).
theorem erdos_98.variants.upper_bound :
∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
(h n : ℝ) < (n : ℝ) * Real.exp (c * Real.sqrt (Real.log (n : ℝ)))
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/98.lean, line 80.
Sources
TheoremErdős Problem 99#
References: * erdosproblems.com/99 * [BeFo99] Bezdek, Andr\'{a}s and Fodor, Ferenc, Minimal diameter of certain sets in the plane. J. Combin. Theory Ser. A (1999), 105-111. * [Er94b] Erd\H{o}s, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269.
Quoted from FormalConjectures/ErdosProblems/99.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/99.
The file states 1 research or textbook statement: 1 open.
Erdos99.erdos_99
Open: stated without proof.
For sufficiently large n, is it the case that any set of n points with minimum distance \(1\) that minimizes diameter must contain an equilateral triangle of side length 1?
theorem erdos_99 :
∀ᶠ n in Filter.atTop, ∀ A : Finset ℝ²,
A.card = n → HasMinDist1 A →
(IsMinOn (fun B: Finset ℝ² => diam (B : Set ℝ²)) {B : Finset ℝ² | B.card = n ∧ HasMinDist1 B} A) →
∃ᵉ (p ∈ A) (q ∈ A) (r ∈ A), FormsEquilateralTriangle p q r
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/99.lean, line 48.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.