Erdős Problem 656 to Erdős Problem 677
TheoremErdős Problem 656#
References: - erdosproblems.com/656 - [Er75b] Erdős, Paul, Problems and results in combinatorial number theory. Journées Arithmétiques de Bordeaux (Conf., Univ. Bordeaux, Bordeaux, 1974) (1975), 295-310. - [KMRR24] Kra, B., Moreira, J., Richter, F. K. and Robertson, D., A proof of Erdős's \(B+B+t\) conjecture. Commun. Am. Math. Soc. 4 (2024), 480-494. arXiv:2206.12377
Quoted from FormalConjectures/ErdosProblems/656.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/656.
The file states 1 research or textbook statement: 1 solved.
Erdos656.erdos_656
Solved: stated here without proof.
Let \(A\subset \mathbb{N}\) be a set with positive upper density. Must there exist an infinite set \(B\subseteq A\) and integer \(t\) such that
\[\{b_1+b_2: b_1\neq b_2\in B\}+t\subseteq A?\]Erdős [Er75b] posed this as a candidate for a density version of Hindman's theorem. This is true, and was proved by Kra, Moreira, Richter, and Robertson [KMRR24, Theorem 1.2 (i)], even for sets of positive upper Banach density and with \(t \geq 0\).
The inclusion says that every \(b_1+b_2+t\) is an element of
A, as an integer.
theorem erdos_656 :
∀ A : Set ℕ, 0 < A.upperDensity →
∃ B ⊆ A, B.Infinite ∧ ∃ t : ℤ, ∀ b₁ ∈ B, ∀ b₂ ∈ B, b₁ ≠ b₂ →
∃ a ∈ A, (a : ℤ) = b₁ + b₂ + t
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/656.lean, line 48.
Sources
TheoremErdős Problem 657#
References: - erdosproblems.com/657 - [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. - [Er75f] Erdős, Paul, On some problems of elementary and combinatorial geometry. Ann. Mat. Pura Appl. (4) (1975), 99-108. - [ErPa90] Erdős, P. and Pach, J., Variations on the theme of repeated distances. Combinatorica (1990), 261-269. - [Er97e] Erdős, Paul, Some of my favourite unsolved problems. Math. Japon. (1997), 527-537. - [Du08] Dumitrescu, Adrian, On distinct distances and λ-free point sets. Discrete Math. (2008), 6533-6538.
Quoted from FormalConjectures/ErdosProblems/657.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/657.
The file states 6 research or textbook statements: 2 open and 4 solved.
Erdos657.erdos_657
Open: stated without proof.
Is it true that if \(A\subset \mathbb{R}^2\) is a set of \(n\) points such that every subset of \(3\) points determines \(3\) distinct distances (that is, \(A\) has no isosceles triangles, degenerate ones included) then \(A\) determines at least \(f(n)n\) distinct distances, for some function \(f\) with \(f(n)\to \infty\)?
theorem erdos_657 :
∃ f : ℕ → ℝ, Tendsto f atTop atTop ∧
∀ n : ℕ, ∀ A : Finset ℝ², A.card = n → (A : Set ℝ²).IsIsoscelesFree →
f n * (n : ℝ) ≤ (distinctDistances A : ℝ)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/657.lean, line 51.
Erdos657.erdos_657.variants.higher_dim
Open: stated without proof.
In [Er73] Erdős attributes the problem, more generally in \(\mathbb{R}^k\), to himself and Davies: for every fixed \(k \geq 1\), is there a function \(f\) with \(f(n)\to \infty\) such that every set of \(n\) points in \(\mathbb{R}^k\) with no isosceles triangles determines at least \(f(n)n\) distinct distances?
Here the dimension \(k\) is fixed and \(f\) may depend on \(k\).
theorem erdos_657.variants.higher_dim :
∀ k : ℕ, 1 ≤ k → ∃ f : ℕ → ℝ, Tendsto f atTop atTop ∧
∀ n : ℕ, ∀ A : Finset (ℝ^k), A.card = n → (A : Set (ℝ^k)).IsIsoscelesFree →
f n * (n : ℝ) ≤ (distinctDistances A : ℝ)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/657.lean, line 66.
Erdos657.erdos_657.variants.dim_one
Solved: stated here without proof.
The question on the real line, which Erdős [Er73] said was open, has a positive answer: there is a function \(f\) with \(f(n)\to \infty\) such that every set of \(n\) real numbers with no three-term arithmetic progression determines at least \(f(n)n\) distinct distances. This follows from the lower bound of Dumitrescu [Du08].
On the line, a set has no isosceles triangle exactly when it has no three-term arithmetic progression.
theorem erdos_657.variants.dim_one :
∃ f : ℕ → ℝ, Tendsto f atTop atTop ∧
∀ n : ℕ, ∀ A : Finset ℝ, A.card = n → (A : Set ℝ).IsIsoscelesFree →
f n * (n : ℝ) ≤ (distinctDistances A : ℝ)
Category research solved; AMS 11 Number theory, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/657.lean, line 82.
Erdos657.erdos_657.variants.dim_one_lower
Solved: stated here without proof.
Dumitrescu [Du08] proved that there is a constant \(c > 0\) such that, for all large \(n\), every set of \(n\) real numbers with no three-term arithmetic progression determines at least \(n(\log n)^c\) distinct distances.
theorem erdos_657.variants.dim_one_lower :
∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
∀ A : Finset ℝ, A.card = n → (A : Set ℝ).IsIsoscelesFree →
(n : ℝ) * (Real.log n) ^ c ≤ (distinctDistances A : ℝ)
Category research solved; AMS 11 Number theory, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/657.lean, line 94.
Erdos657.erdos_657.variants.dim_one_upper
Solved: stated here without proof.
As noted in [Du08], Behrend's construction of large sets without three-term arithmetic progressions shows that there is a constant \(C > 0\) such that, for all large \(n\), some set of \(n\) real numbers with no three-term arithmetic progression determines at most \(n 2^{C\sqrt{\log n}}\) distinct distances.
theorem erdos_657.variants.dim_one_upper :
∃ C > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
∃ A : Finset ℝ, A.card = n ∧ (A : Set ℝ).IsIsoscelesFree ∧
(distinctDistances A : ℝ) ≤ (n : ℝ) * (2 : ℝ) ^ (C * √(Real.log n))
Category research solved; AMS 11 Number theory, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/657.lean, line 107.
Erdos657.erdos_657.variants.straus
Solved: stated here without proof.
Straus observed that for every \(k\) there is a set of \(2^k\) points in \(\mathbb{R}^k\) with no isosceles triangles which determines at most \(2^k - 1\) distinct distances.
theorem erdos_657.variants.straus (k : ℕ) :
∃ A : Finset (ℝ^k), A.card = 2 ^ k ∧ (A : Set (ℝ^k)).IsIsoscelesFree ∧
distinctDistances A ≤ 2 ^ k - 1
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/657.lean, line 118.
Sources
TheoremErdős Problem 658#
References: - erdosproblems.com/658 - [Er97e] Erdős, Paul, Some of my favourite unsolved problems. Math. Japon. (1997), 527-537. - [FuKa91] Furstenberg, H. and Katznelson, Y., A density version of the Hales-Jewett Theorem. Journal d'Analyse Mathématique (1991), 64-119. - [So04] Solymosi, J., A Note on a Question of Erdős and Graham. Combinatorics, Probability and Computing (2004), 263–267.
Quoted from FormalConjectures/ErdosProblems/658.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/658.
The file states 1 research or textbook statement: 1 solved.
Erdos658.erdos_658
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos658.lean#L1516.
Let \(\delta>0\) and \(N\) be sufficiently large depending on \(\delta\). Is it true that if \(A\subseteq \{1,\ldots,N\}^2\) has \(\lvert A\rvert \geq \delta N^2\) then \(A\) must contain the vertices of a square?
A problem of Graham, if the square is restricted to be axis-aligned. (It is unclear whether in [Er97e] had this restriction in mind.)
This qualitative statement follows from the density Hales-Jewett theorem proved by Furstenberg and Katznelson [FuKa91]. A quantitative proof (yet with very poor bounds) was given by Solymosi [So04].
The square is taken to be axis-aligned (Graham's version), which implies the version allowing arbitrary squares.
theorem erdos_658 : ∀ δ : ℝ, 0 < δ → ∀ᶠ N : ℕ in atTop,
∀ A : Finset (ℕ × ℕ), A ⊆ Finset.Icc 1 N ×ˢ Finset.Icc 1 N → δ * N ^ 2 ≤ A.card →
∃ a b d : ℕ, 0 < d ∧ (a, b) ∈ A ∧ (a + d, b) ∈ A ∧ (a, b + d) ∈ A ∧ (a + d, b + d) ∈ A
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/658.lean, line 56.
Sources
TheoremErdős Problem 659#
References: - erdosproblems.com/659 - [MoOs06] Moree, Pieter and Osburn, Robert, Two-dimensional lattices with few distances. Enseign. Math. (2) (2006), 361--380 - [ErFi96] Erdős, Paul and Fishburn, Peter, Maximum planar sets that determine {\(k\)} distances. Discrete Math. (1996), 115--125. - Gr26: Benjamin Grayzel, Solution to a Problem of Erdős Concerning Distances and Points
Quoted from FormalConjectures/ErdosProblems/659.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/659.
The file states 1 research or textbook statement: 1 solved.
Erdos659.erdos_659
Solved: stated here without proof.
Is there a set of \(n\) points in \(\mathbb{R}^2\) such that every subset of \(4\) points determines at least \(3\) distances, yet the total number of distinct distances is \(\ll \frac{n}{\sqrt{\log n}}\)?
There does exist such a set: a suitable truncation of the lattice \(\{(a,b\sqrt{2}): a,b\in\mathbb{Z}\}\) suffices. This construction appears to have been first considered by Moree and Osburn \cite{MoOs06}, who proved that it has \(\ll \frac{n}{\sqrt{\log n}}\) many distinct distances. This construction was independently found by Lund and Sheffer, who further noted that this configuration contains no squares or equilateral triangles.
There are only six possible configurations of \(4\) points which determine only \(2\) distances (first noted by Erdős and Fishburn [ErFi96]), and five of them contain either a square or an equilateral triangle. The remaining configuration contains four points from a regular pentagon, and Grayzel [Gr26] (using Gemini) has noted in the comments that this configuration can also be ruled out, thus giving a complete solution to this problem.
Boris Alexeev provides a formalisation of the reduction, which is conditional on Bernays' theorem (assumed as an axiom in the proof to obtain the \(O(n/\sqrt{\log n})\) bound). See the formal proof.
theorem erdos_659 : ∃ A : ℕ → Finset ℝ²,
(∀ n, #(A n) = n ∧ ∀ S ⊆ A n, #S = 4 → 3 ≤ distinctDistances S) ∧
(fun n ↦ distinctDistances (A n)) ≪ fun n ↦ n / sqrt (log n)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/659.lean, line 58.
Sources
TheoremErdős Problem 660#
References: - erdosproblems.com/660 - [Er97e] Erdős, Paul, Some of my favorite problems and results, The mathematics of Paul Erdős, I (1997), 47–67. - [Al63] Altman, E., On a problem of P. Erdős, Amer. Math. Monthly (1963), 148–157. - [Er75f] Erdős, Paul, On some problems of elementary and combinatorial geometry, Ann. Mat. Pura Appl. (4) (1975), 99–108.
Quoted from FormalConjectures/ErdosProblems/660.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/660.
The file states 3 research or textbook statements: 2 open and 1 solved.
Erdos660.erdos_660
Open: stated without proof.
Let \(x_1, \ldots, x_n \in \mathbb{R}^3\) be the vertices of a convex polyhedron. Are there at least
\[(1 - o(1)) \frac{n}{2}\]many distinct distances between the \(x_i\)?
The \((1 - o(1)) \frac{n}{2}\) lower bound is formalised as: for every \(\varepsilon > 0\), every set of \(n\) vertices of a convex polyhedron with \(n\) sufficiently large determines at least \((1 - \varepsilon) \frac{n}{2}\) distinct distances.
theorem erdos_660 :
∀ ε : ℝ, 0 < ε → ∀ᶠ n in Filter.atTop, ∀ P : Finset ℝ³,
P.card = n → IsPolyhedronVertices P →
(1 - ε) * ((n : ℝ) / 2) ≤ (distinctDistances P : ℝ)
Category research open; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/660.lean, line 56.
Erdos660.erdos_660.variants.altman_planar
Solved: stated here without proof.
For the similar problem in \(\mathbb{R}^2\) there are always at least \(n/2\) distances, as proved by Altman [Al63].
theorem erdos_660.variants.altman_planar (n : ℕ) (P : Finset ℝ²)
(hcard : P.card = n) (hconv : ConvexIndependent ℝ ((↑) : ↥(P : Set ℝ²) → ℝ²))
(haff : affineSpan ℝ (P : Set ℝ²) = ⊤) :
n / 2 ≤ distinctDistances P
Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/660.lean, line 67.
Erdos660.erdos_660.variants.Er75f
Open: stated without proof.
In [Er75f] Erdős claims that Altman proved that the vertices determine \(\gg n\) many distinct distances, but gives no reference.
theorem erdos_660.variants.Er75f :
∃ c > (0 : ℝ), ∀ᶠ n in Filter.atTop, ∀ P : Finset ℝ³,
P.card = n → IsPolyhedronVertices P →
c * n ≤ (distinctDistances P : ℝ)
Category research open; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/660.lean, line 78.
Sources
TheoremErdős Problem 661#
References: - erdosproblems.com/661 - [ErPa90] Erdős, P. and Pach, J., Variations on the theme of repeated distances. Combinatorica (1990), 261--269. - [Er92e] Erdős, Pál, Some Unsolved problems in Geometry, Number Theory and Combinatorics. Eureka (1992), 44-48. - [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. - [Er46] Erdős, Paul, On sets of distances of \(n\) points. Amer. Math. Monthly 53 (1946), 248--250.
Quoted from FormalConjectures/ErdosProblems/661.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/661.
The file states 5 research or textbook statements: 2 open, 2 solved and 1 textbook result.
Erdos661.erdos_661
Open: stated without proof.
Are there, for all large \(n\), some points \(x_1,\ldots,x_n,y_1,\ldots,y_n\in \mathbb{R}^2\) such that the number of distinct distances \(d(x_i,y_j)\) is
\[o\left(\frac{n}{\sqrt{\log n}}\right)?\]We require all \(2n\) points to be distinct; without any distinctness one could take all points equal and get a single distance. Writing \(F(n)\) for the minimal number of such distances (
minimalCrossDistances ℝ² n), the question asks whether \(F(n) = o(n / \sqrt{\log n})\). This is equivalent to the existence, for all large \(n\), of configurations whose count is at most \(g(n)\) for some fixed \(g(n) = o(n / \sqrt{\log n})\), since the infimum is attained.The source adds that one can also ask this for points in \(\mathbb{R}^3\). Taken literally, the question is easy there, since a cubic grid of \(2n\) points determines only \(O(n^{2/3})\) distinct distances, so we do not state it.
theorem erdos_661 :
(fun n => (minimalCrossDistances ℝ² n : ℝ)) =o[atTop]
(fun (n : ℕ) => (n : ℝ) / (n : ℝ).log.sqrt)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/661.lean, line 74.
Erdos661.erdos_661.variants.grid_upper_bound
Solved: stated here without proof.
Take \(2n\) points of the smallest square grid with at least \(2n\) points; by [Er46] they determine \(O(n / \sqrt{\log n})\) distinct distances. Splitting them into two halves of \(n\) points shows that \(F(n) = O(n / \sqrt{\log n})\). So the question is whether this trivial bound can be improved by more than a constant factor.
theorem erdos_661.variants.grid_upper_bound :
(fun n => (minimalCrossDistances ℝ² n : ℝ)) =O[atTop]
(fun (n : ℕ) => (n : ℝ) / (n : ℝ).log.sqrt)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/661.lean, line 86.
Erdos661.erdos_661.variants.le_minimalDistinctDistances
Textbook result, proved here.
Every split of a set of \(2n\) points into two halves of \(n\) points gives a configuration for \(F(n)\), and the distances between the halves are among the distances of the whole set. Hence \(F(n) \leq f(2n)\), where \(f(2n)\) is the minimal number of distinct distances determined by \(2n\) points in \(\mathbb{R}^2\).
theorem erdos_661.variants.le_minimalDistinctDistances (n : ℕ) :
minimalCrossDistances ℝ² n ≤ minimalDistinctDistances ℝ² (2 * n)
Category textbook; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/661.lean, line 98.
Erdos661.erdos_661.variants.little_o_distinct_distances
Open: stated without proof.
Let \(F(2n)\) be the minimal number of distinct distances \(d(x_i, y_j)\) for \(2n\) distinct points \(x_1,\ldots,x_n,y_1,\ldots,y_n\in \mathbb{R}^2\), and \(f(2n)\) the minimal number of distinct distances determined by any \(2n\) points in \(\mathbb{R}^2\). Is \(F = o(f)\)?
Here \(F(2n)\) of erdosproblems.com is
minimalCrossDistances ℝ² n(indexed by \(n\) points on each side) and \(f(2n)\) isminimalDistinctDistances ℝ² (2 * n). See also Erdős Problem 89.
theorem erdos_661.variants.little_o_distinct_distances :
(fun n => (minimalCrossDistances ℝ² n : ℝ)) =o[atTop]
(fun n => (minimalDistinctDistances ℝ² (2 * n) : ℝ))
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/661.lean, line 125.
Erdos661.erdos_661.variants.lenz
Solved: stated here without proof.
In \(\mathbb{R}^4\) Lenz observed (as stated on erdosproblems.com/661) that for every \(n\) there are \(2n\) distinct points \(x_1,\ldots,x_n,y_1,\ldots,y_n\in \mathbb{R}^4\) with \(d(x_i,y_j)=1\) for all \(i,j\): take the \(x_i\) on the circle of radius \(1/\sqrt{2}\) about the origin in the plane of the first two coordinates, and the \(y_j\) on the circle of radius \(1/\sqrt{2}\) about the origin in the plane of the last two coordinates.
theorem erdos_661.variants.lenz (n : ℕ) :
∃ A B : Finset (EuclideanSpace ℝ (Fin 4)), #A = n ∧ #B = n ∧ Disjoint A B ∧
∀ x ∈ A, ∀ y ∈ B, dist x y = 1
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/661.lean, line 138.
Sources
TheoremErdős Problem 663#
References: - erdosproblems.com/663 - [BEGL96] Burr, S. A., Erdős, P., Graham, R. L., and Li, W. W.-C., Complete sequences of sets of integer powers. Acta Arith. (1996), 133–138. - [Er97e] Erdős, Paul, Some of my favourite unsolved problems. Math. Japon. (1997), 527–537.
Quoted from FormalConjectures/ErdosProblems/663.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/663.
The file states 1 research or textbook statement: 1 open.
Erdos663.erdos_663
Open: stated without proof.
Let \(k \geq 2\), and let \(q(n,k)\) denote the least prime which does not divide \(\prod_{1 \leq i \leq k}(n+i)\). Is it true that, if \(k\) is fixed and \(n\) is sufficiently large, then \(q(n,k) < (1+o(1))\log n\)?
theorem erdos_663 : ∀ k ≥ 2, ∃ error : ℕ → ℝ,
error =o[atTop] (fun _ ↦ (1 : ℝ)) ∧ ∀ᶠ n in atTop,
let P : ℕ := ∏ i ∈ Finset.Icc 1 k, (n + i)
∃ q : ℕ, q.Prime ∧ ¬ q ∣ P ∧ (∀ p : ℕ, p.Prime → ¬ p ∣ P → q ≤ p) ∧
(q : ℝ) < (1 + error n) * Real.log n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/663.lean, line 43.
Sources
TheoremErdős Problem 664#
References: - erdosproblems.com/664 - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42. - [Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10.
Quoted from FormalConjectures/ErdosProblems/664.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/664.
The file states 3 research or textbook statements: 1 open and 2 solved.
Erdos664.erdos_664
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos664.lean#L214.
Let \(c<1\) be some constant and \(A_1,\ldots,A_m\subseteq \{1,\ldots,n\}\) be such that \(\lvert A_i\rvert >c\sqrt{n}\) for all \(i\) and \(\lvert A_i\cap A_j\rvert\leq 1\) for all \(i\neq j\).
Must there exist some set \(B\) such that \(B\cap A_i\neq \emptyset\) and \(\lvert B\cap A_i\rvert \ll_c 1\) for all \(i\)?
The answer is no, proved by Alon: if \(q\) is a large prime power and \(n=m=q^2+q+1\) then there exist \(A_1,\ldots,A_m\subseteq \{1,\ldots,n\}\) such that \(\lvert A_i\rvert \geq \tfrac{2}{5}\sqrt{n}\) for all \(i\) and \(\lvert A_i\cap A_j\rvert\leq 1\) for all \(i\neq j\), and yet if \(B\) has non-empty intersection with all \(A_i\) then there exists \(A_j\) such that \(\lvert B\cap A_j\rvert \gg \log n\).
theorem erdos_664 :
¬ ∀ c : ℝ, 0 < c → c < 1 → ∃ K : ℕ, ∀ (n m : ℕ) (A : Fin m → Finset (Fin n)),
(∀ i, c * √n < (A i).card) → (∀ i j, i ≠ j → (A i ∩ A j).card ≤ 1) →
∃ B : Finset (Fin n), (∀ i, (B ∩ A i).Nonempty) ∧
∀ i, (B ∩ A i).card ≤ K
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/664.lean, line 53.
Erdos664.erdos_664.variants.two_fifths
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos664.lean#L214.
Alon's counterexample already works for \(c=2/5\).
theorem erdos_664.variants.two_fifths :
¬ ∃ K : ℕ, ∀ (n m : ℕ) (A : Fin m → Finset (Fin n)),
(∀ i, 2 / 5 * √n < (A i).card) → (∀ i j, i ≠ j → (A i ∩ A j).card ≤ 1) →
∃ B : Finset (Fin n), (∀ i, (B ∩ A i).Nonempty) ∧
∀ i, (B ∩ A i).card ≤ K
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/664.lean, line 64.
Erdos664.erdos_664.variants.block_design
Open: stated without proof.
In [Er81] the condition \(\lvert A_i\cap A_j\rvert\leq 1\) for all \(i\neq j\) is replaced by every two points in \(\{1,\ldots,n\}\) being contained in exactly one \(A_i\), that is, \(A_1,\ldots,A_m\) is a pairwise balanced block design. The bound \(\lvert A_i\rvert>c\sqrt{n}\) is kept, only the condition \(c<1\) is omitted. This weaker version remains open, although Alon conjectures the answer there to also be no.
theorem erdos_664.variants.block_design :
∀ c : ℝ, 0 < c → ∃ K : ℕ, ∀ (n m : ℕ) (A : Fin m → Finset (Fin n)),
(∀ i, c * √n < (A i).card) → (∀ x y : Fin n, x ≠ y → ∃! i, x ∈ A i ∧ y ∈ A i) →
∃ B : Finset (Fin n), (∀ i, (B ∩ A i).Nonempty) ∧
∀ i, (B ∩ A i).card ≤ K
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/664.lean, line 79.
Sources
TheoremErdős Problem 665#
References: - erdosproblems.com/665 - [Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10. - [ErLa82] Erdős, P. and Larson, J., On pairwise balanced block designs with the sizes of blocks as uniform as possible. Annals of Discrete Mathematics (1982), 129-134. - [ShSi85] S. S. Shrikhande and N. M. Singhi, On a problem of Erdős and Larson. Combinatorica (1985), 351-358.
Quoted from FormalConjectures/ErdosProblems/665.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/665.
The file states 1 research or textbook statement: 1 open.
Erdos665.erdos_665
Open: stated without proof.
A pairwise balanced design for \(\{1,\ldots,n\}\) is a collection of sets \(A_1,\ldots,A_m\subseteq \{1,\ldots,n\}\) such that \(2\leq \lvert A_i\rvert \lt n\) and every pair of distinct elements \(x,y\in \{1,\ldots,n\}\) is contained in exactly one \(A_i\). Is there a constant \(C>0\) and, for all large \(n\), a pairwise balanced design such that
\[\lvert A_i\rvert > n^{1/2}-C\]for all \(1\leq i\leq m\)?
theorem erdos_665 :
∃ C : ℝ, 0 < C ∧ ∀ᶠ n : ℕ in atTop,
∃ H : Finset (Finset (Fin n)), H.IsPairwiseBalancedDesign ∧
∀ e ∈ H, e.card < n ∧ Real.sqrt n - C < e.card
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/665.lean, line 48.
Sources
TheoremErdős Problem 666#
References: - erdosproblems.com/666 - [BDT93] Brouwer, A. E. and Dejter, I. J. and Thomassen, C., Highly symmetric subgraphs of hypercubes. J. Algebraic Combin. (1993), 25-29. - [Ch92] Chung, Fan R. K., Subgraphs of a hypercube containing no small even cycles. J. Graph Theory (1992), 273-286. - [Er91] Erdős, P., Problems and results in combinatorial analysis and combinatorial number theory. Graph theory, combinatorics, and applications, Vol. 1 (Kalamazoo, MI, 1988) (1991), 397-406.
Quoted from FormalConjectures/ErdosProblems/666.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/666.
The file states 1 research or textbook statement: 1 solved.
Erdos666.erdos_666
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos666.lean.
Let \(Q_n\) be the \(n\)-dimensional hypercube graph (so that \(Q_n\) has \(2^n\) vertices and \(n2^{n-1}\) edges). Is it true that, for every \(\epsilon>0\), if \(n\) is sufficiently large, every subgraph of \(Q_n\) with
\[\geq \epsilon n2^{n-1}\]many edges contains a \(C_6\)?
The answer to this problem is no: Chung [Ch92] and Brouwer, Dejter, and Thomassen [BDT93] constructed an edge-partition of \(Q_n\) into four subgraphs, each containing no \(C_6\).
theorem erdos_666 :
¬ ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop, ∀ H : SimpleGraph (Fin n → Bool), H ≤ hypercube n →
ε * n * 2 ^ (n - 1 : ℕ) ≤ (H.edgeSet.ncard : ℝ) → (cycleGraph 6 ⊑ H)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/666.lean, line 54.
Sources
TheoremErdős Problem 667#
A problem of Erdős, Faudree, Rousseau, and Schelp on the growth exponent of the largest clique that is guaranteed inside a locally dense graph.
References: * erdosproblems.com/667 * [Er97f] P. Erdős, Some unsolved problems. In: Combinatorics, Geometry and Probability (Cambridge, 1993), Cambridge Univ. Press (1997), 1-10. * [EFRS94] P. Erdős, R. J. Faudree, C. C. Rousseau and R. H. Schelp, A local density condition for triangles. Discrete Math. 127 (1994), 153-161.
Quoted from FormalConjectures/ErdosProblems/667.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/667.
The file states 4 research or textbook statements: 1 open, 2 solved and 1 textbook result.
Erdos667.erdos_667
Open: stated without proof.
Let \(p, q \geq 1\) be fixed integers. Define \(H(n) = H(n; p, q)\) to be the largest \(m\) such that any graph on \(n\) vertices where every set of \(p\) vertices spans at least \(q\) edges must contain a complete graph on \(m\) vertices. Is
\[ c(p, q) = \liminf_{n \to \infty} \frac{\log H(n)}{\log n} \]a strictly increasing function of \(q\) for \(1 \leq q \leq \binom{p-1}{2} + 1\)?
A problem of Erdős, Faudree, Rousseau, and Schelp. When \(q = 1\) this corresponds exactly to the classical Ramsey problem, and hence \(\tfrac{1}{p-1} \leq c(p, 1) \leq \tfrac{2}{p+1}\) for \(p \geq 3\). It is easy to see that if \(q = \binom{p-1}{2} + 1\) then \(c(p, q) = 1\).
erdosproblems.com/667 also states that Erdős, Faudree, Rousseau and Schelp showed \(c(p, \binom{p-1}{2}) \leq 1/2\). This cannot hold for all \(p\): for \(p = 6\), \(q = 10\), the complement of a \((6, 10)\)-locally dense graph is \(C_6\)-free, so Bondy–Simonovits together with \(\alpha(F) \geq n^2 / (2e(F) + n)\) gives \(c(6, 10) \geq 2/3\). That remark is therefore not formalised here.
theorem erdos_667 :
∀ p : ℕ, StrictMonoOn (c p) (Set.Icc 1 (Nat.choose (p - 1) 2 + 1))
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/667.lean, line 78.
Erdos667.erdos_667.variants.monotoneOn
Textbook result, stated without proof. A Lean proof is at https://github.com/linrock/math-proofs/blob/d16a9d73d85f1377e83798f5d9585ee4c4140979/erdos-667/Solution.lean#L41.
That \(c(p, q)\) is nondecreasing in \(q\) for fixed \(p\) is a straightforward consequence of the definitions: enlarging \(q\) shrinks the family of \((p, q)\)-locally dense graphs, which can only increase the guaranteed clique size \(H(n)\), and hence the exponent.
theorem erdos_667.variants.monotoneOn (p : ℕ) :
MonotoneOn (c p) (Set.Icc 1 (Nat.choose (p - 1) 2 + 1))
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/667.lean, line 89.
Erdos667.erdos_667.variants.endpoint
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/d16a9d73d85f1377e83798f5d9585ee4c4140979/erdos-667/Solution.lean#L45.
The right endpoint: when \(q = \binom{p-1}{2} + 1\) one has \(c(p, q) = 1\) (stated as "easy to see" on erdosproblems.com/667).
theorem erdos_667.variants.endpoint (p : ℕ) (hp : 2 ≤ p) :
c p (Nat.choose (p - 1) 2 + 1) = 1
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/667.lean, line 100.
Erdos667.erdos_667.variants.ramsey_bounds
Solved: stated here without proof.
The case \(q = 1\) is the classical Ramsey problem, giving the bounds \(\tfrac{1}{p-1} \leq c(p, 1) \leq \tfrac{2}{p+1}\) for \(p \geq 3\). (For \(p = 2\) the condition forces \(G\) to be complete, so \(c(2, 1) = 1\) and the upper bound fails.)
theorem erdos_667.variants.ramsey_bounds (p : ℕ) (hp : 3 ≤ p) :
1 / ((p : ℝ) - 1) ≤ c p 1 ∧ c p 1 ≤ 2 / ((p : ℝ) + 1)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/667.lean, line 110.
Sources
TheoremErdős Problem 668#
References: - erdosproblems.com/668 - A385657 - [AMP25] B. Alexeev, D. Mixon, and H. Parshall, The Erdős unit distance problem for small point sets. arXiv:2412.11914 (2025). - [EHSVZ25] P. Engel, O. Hammond-Lee, Y. Su, D. Varga, and P. Zsámboki, Diverse beam search to find densest-known planar unit distance graphs. arXiv:2406.15317 (2025). - [Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10.
Quoted from FormalConjectures/ErdosProblems/668.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/668.
The file states 3 research or textbook statements: 1 open and 2 solved. It also has 1 test statement, counted here but not shown.
Erdos668.erdos_668.parts.i
Open: stated without proof.
Is it true that the number of incongruent sets of \(n\) points in \(\mathbb{R}^2\) which maximise the number of unit distances tends to infinity as \(n\to\infty\)?
The actual maximal number of unit distances is the subject of Erdős Problem 90.
Two sets of points are congruent if an isometry of the plane maps one onto the other.
theorem erdos_668.parts.i :
∀ m : ℕ, ∀ᶠ n in atTop, ∃ A : Fin m → Finset ℝ²,
(∀ i, (A i).card = n ∧ unitDistNum (A i) = maxUnitDistances n) ∧
∀ i j, i ≠ j → ¬ ∃ f : ℝ² ≃ᵢ ℝ², f '' A i = A j
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/668.lean, line 54.
Erdos668.erdos_668.parts.ii
Solved: stated here without proof.
Is it always \(>1\) for \(n>3\)?
In fact this is \(=1\) also for \(n=4\), the unique example given by two equilateral triangles joined by an edge.
Computational evidence of Engel, Hammond-Lee, Su, Varga, and Zsámboki [EHSVZ25] and Alexeev, Mixon, and Parshall [AMP25] suggests that this count is \(=1\) for various other \(5\leq n\leq 21\) (although these calculations were checking only up to graph isomorphism, rather than congruency).
theorem erdos_668.parts.ii :
¬ ∀ n : ℕ, 3 < n → ∃ A B : Finset ℝ², A.card = n ∧ B.card = n ∧
unitDistNum A = maxUnitDistances n ∧ unitDistNum B = maxUnitDistances n ∧
¬ ∃ f : ℝ² ≃ᵢ ℝ², f '' A = B
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/668.lean, line 72.
Erdos668.erdos_668.variants.four_points
Solved: stated here without proof.
For \(n=4\) there is, up to congruence, exactly one set of points in \(\mathbb{R}^2\) which maximises the number of unit distances: two unit equilateral triangles \(abc\) and \(bcd\) joined by the edge \(bc\), with \(a\neq d\).
theorem erdos_668.variants.four_points :
∃ a b c d : ℝ², dist a b = 1 ∧ dist a c = 1 ∧ dist b c = 1 ∧ dist b d = 1 ∧ dist c d = 1 ∧
({a, b, c, d} : Finset ℝ²).card = 4 ∧
∀ B : Finset ℝ², B.card = 4 →
(unitDistNum B = maxUnitDistances 4 ↔ ∃ f : ℝ² ≃ᵢ ℝ², f '' {a, b, c, d} = B)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/668.lean, line 84.
Sources
TheoremErdős Problem 669#
References: - erdosproblems.com/669 - [BGS74] Burr, Stefan A. and Grünbaum, Branko and Sloane, N. J. A., The orchard problem. Geometriae Dedicata (1974), 397-424. - [Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10.
Quoted from FormalConjectures/ErdosProblems/669.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/669.
The file states 8 research or textbook statements: 2 open and 6 solved. It also has 3 test statements, counted here but not shown.
Erdos669.erdos_669.parts.i
Open: stated without proof.
Let \(F_k(n)\) be minimal such that for any \(n\) points in \(\mathbb{R}^2\) there exist at most \(F_k(n)\) many distinct lines passing through at least \(k\) of the points, and \(f_k(n)\) similarly but with lines passing through exactly \(k\) points.
Estimate \(f_k(n)\) and \(F_k(n)\) - in particular, determine \(\lim F_k(n)/n^2\) and \(\lim f_k(n)/n^2\).
This part asks for \(\lim F_k(n)/n^2\) for \(k \geq 3\) (the case \(k = 2\) is trivial). The original question [Er97f, Problem 16] asks for the limits "if they exist", so the answer allows nonexistence: the answer at \(k\) is
some xif the limit exists and equals \(x\), andnoneotherwise.
theorem erdos_669.parts.i :
∀ k : ℕ, 3 ≤ k → ∀ x : ℝ,
erdos_669.parts.i.answer k = some x ↔
Tendsto (fun n : ℕ => (maxLinesAtLeast k n : ℝ) / (n : ℝ) ^ 2) atTop (𝓝 x)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/669.lean, line 143.
Erdos669.erdos_669.parts.ii
Open: stated without proof.
Let \(F_k(n)\) be minimal such that for any \(n\) points in \(\mathbb{R}^2\) there exist at most \(F_k(n)\) many distinct lines passing through at least \(k\) of the points, and \(f_k(n)\) similarly but with lines passing through exactly \(k\) points.
Estimate \(f_k(n)\) and \(F_k(n)\) - in particular, determine \(\lim F_k(n)/n^2\) and \(\lim f_k(n)/n^2\).
This part asks for \(\lim f_k(n)/n^2\) for \(k \geq 3\) (the case \(k = 2\) is trivial). The original question [Er97f, Problem 16] asks for the limits "if they exist", so the answer allows nonexistence: the answer at \(k\) is
some xif the limit exists and equals \(x\), andnoneotherwise.
theorem erdos_669.parts.ii :
∀ k : ℕ, 3 ≤ k → ∀ x : ℝ,
erdos_669.parts.ii.answer k = some x ↔
Tendsto (fun n : ℕ => (maxLinesExactly k n : ℝ) / (n : ℝ) ^ 2) atTop (𝓝 x)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/669.lean, line 165.
Erdos669.erdos_669.variants.exactly_le_atLeast
Proved here.
Trivially \(f_k(n)\leq F_k(n)\).
theorem erdos_669.variants.exactly_le_atLeast (k n : ℕ) :
maxLinesExactly k n ≤ maxLinesAtLeast k n
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/669.lean, line 175.
Erdos669.erdos_669.variants.k_two
Solved: stated here without proof.
\(f_2(n)=F_2(n)=\binom{n}{2}\).
theorem erdos_669.variants.k_two (n : ℕ) :
maxLinesExactly 2 n = n.choose 2 ∧ maxLinesAtLeast 2 n = n.choose 2
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/669.lean, line 191.
Erdos669.erdos_669.variants.burr_grunbaum_sloane_exactly
Solved: stated here without proof.
The problem with \(k=3\) is the classical 'Orchard problem' of Sylvester. Burr, Grünbaum, and Sloane [BGS74] have proved that
\[f_3(n)=\frac{n^2}{6}-O(n)\]and
\[F_3(n)=\frac{n^2}{6}-O(n).\]This is the statement for \(f_3\).
theorem erdos_669.variants.burr_grunbaum_sloane_exactly :
(fun n : ℕ => (maxLinesExactly 3 n : ℝ) - (n : ℝ) ^ 2 / 6) =O[atTop]
(fun n : ℕ => (n : ℝ))
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/669.lean, line 205.
Erdos669.erdos_669.variants.burr_grunbaum_sloane_atLeast
Solved: stated here without proof.
The problem with \(k=3\) is the classical 'Orchard problem' of Sylvester. Burr, Grünbaum, and Sloane [BGS74] have proved that
\[f_3(n)=\frac{n^2}{6}-O(n)\]and
\[F_3(n)=\frac{n^2}{6}-O(n).\]This is the statement for \(F_3\).
theorem erdos_669.variants.burr_grunbaum_sloane_atLeast :
(fun n : ℕ => (maxLinesAtLeast 3 n : ℝ) - (n : ℝ) ^ 2 / 6) =O[atTop]
(fun n : ℕ => (n : ℝ))
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/669.lean, line 220.
Erdos669.erdos_669.variants.upper_bound
Solved: stated here without proof.
There is a trivial upper bound of \(F_k(n) \leq \binom{n}{2}/\binom{k}{2}\).
theorem erdos_669.variants.upper_bound (k n : ℕ) (hk : 2 ≤ k) :
(maxLinesAtLeast k n : ℝ) ≤ (n.choose 2 : ℝ) / (k.choose 2 : ℝ)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/669.lean, line 229.
Erdos669.erdos_669.variants.limit_le
Solved: stated here without proof.
There is a trivial upper bound of \(F_k(n) \leq \binom{n}{2}/\binom{k}{2}\), and hence
\[\lim F_k(n)/n^2 \leq \frac{1}{k(k-1)}.\]See also 101.
Here the limit is assumed to exist and is called
L.
theorem erdos_669.variants.limit_le (k : ℕ) (hk : 2 ≤ k) (L : ℝ)
(hL : Tendsto (fun n : ℕ => (maxLinesAtLeast k n : ℝ) / (n : ℝ) ^ 2) atTop (𝓝 L)) :
L ≤ 1 / ((k : ℝ) * ((k : ℝ) - 1))
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/669.lean, line 241.
Sources
TheoremErdős Problem 670#
References: - erdosproblems.com/670 - [Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10. - [Ho26] Ho, B. S., Erdős's diameter conjecture for separated distances fails in high dimensions. arXiv:2604.15305 (2026).
Quoted from FormalConjectures/ErdosProblems/670.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/670.
The file states 5 research or textbook statements: 1 open, 3 solved and 1 textbook result.
Erdos670.erdos_670
Open: stated without proof.
Let \(A\subseteq \mathbb{R}^d\) be a set of \(n\) points such that all pairwise distances differ by at least \(1\). Is the diameter of \(A\) at least \((1+o(1))n^2\)?
The quantifiers in the source are ambiguous. Following the remarks on erdosproblems.com, this is the regime where \(d\) is fixed and the \(o(1)\) term tends to \(0\) as \(n \to \infty\), at a rate which may depend on \(d\). The case \(d = 1\) was proved by Erdős (
Erdos670.erdos_670.variants.dim_one), so the question is open for \(d \geq 2\).
theorem erdos_670 :
∀ d : ℕ, 1 ≤ d → ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
∀ A : Finset (EuclideanSpace ℝ (Fin d)), A.card = n → HasSeparatedDistances A →
(1 - ε) * (n : ℝ) ^ 2 ≤ Metric.diam (A : Set (EuclideanSpace ℝ (Fin d)))
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/670.lean, line 54.
Erdos670.erdos_670.variants.dim_one
Solved: stated here without proof.
Erdős [Er97f] proved the claim when \(d = 1\): if \(A\subseteq \mathbb{R}\) is a set of \(n\) points such that all pairwise distances differ by at least \(1\), then the diameter of \(A\) is at least \((1+o(1))n^2\).
theorem erdos_670.variants.dim_one :
∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
∀ A : Finset (EuclideanSpace ℝ (Fin 1)), A.card = n → HasSeparatedDistances A →
(1 - ε) * (n : ℝ) ^ 2 ≤ Metric.diam (A : Set (EuclideanSpace ℝ (Fin 1)))
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/670.lean, line 66.
Erdos670.erdos_670.variants.choose_two
Textbook result, stated without proof. A Lean proof is at https://github.com/veljjanoski/formal-conjectures-proofs/blob/638a2315428e3a1c2f1a784bcaeffea6580d1cbd/FcProofs/Erdos670.lean#L65.
The trivial lower bound: if \(A\subseteq \mathbb{R}^d\) is a set of \(n \neq 2\) points such that all pairwise distances differ by at least \(1\), then the diameter of \(A\) is at least \(\binom{n}{2}\).
For \(n \geq 3\), take a closest pair \(a, b\) and a third point \(c\). Then \(1 \leq \lvert d(a, c) - d(b, c)\rvert \leq d(a, b)\), so every distance is at least \(1\). The \(\binom{n}{2}\) distances are at least \(1\) apart, so the largest one is at least \(\binom{n}{2}\). For \(n = 2\) the hypothesis is vacuous, and two points at distance \(1/2\) show that the bound fails.
theorem erdos_670.variants.choose_two (d : ℕ) (A : Finset (EuclideanSpace ℝ (Fin d)))
(hA : HasSeparatedDistances A) (hn : A.card ≠ 2) :
(A.card.choose 2 : ℝ) ≤ Metric.diam (A : Set (EuclideanSpace ℝ (Fin d)))
Category textbook; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/670.lean, line 83.
Erdos670.erdos_670.variants.ho
Solved: stated here; a Lean proof is at https://github.com/boonsuan/erdos670/blob/c053b2580e0cf7e74c8d905f96feb101061612a3/DiameterConstruction/MainTheorem.lean#L452.
Ho [Ho26] showed that the claim fails if \(n\) grows with \(d\): there exist infinitely many \(n\) and, with \(d = n^2 - n\), a set \(A\subset \mathbb{R}^d\) of \(n\) points such that all pairwise distances differ by at least \(1\), with diameter at most
\[ \left(1-\frac{1}{\pi^2}+o(1)\right)n^2\approx 0.898n^2. \]Ho's construction uses \(n = q + 1\) points in dimension \(q^2 + q = n^2 - n\), for every prime power \(q\).
theorem erdos_670.variants.ho :
∀ ε > (0 : ℝ), ∃ᶠ n : ℕ in atTop,
∃ A : Finset (EuclideanSpace ℝ (Fin (n ^ 2 - n))), A.card = n ∧
HasSeparatedDistances A ∧
Metric.diam (A : Set (EuclideanSpace ℝ (Fin (n ^ 2 - n)))) ≤
(1 - 1 / Real.pi ^ 2 + ε) * (n : ℝ) ^ 2
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/670.lean, line 101.
Erdos670.erdos_670.variants.uniform_in_dim
Solved: stated here without proof.
The version of the problem where the \(o(1)\) term must be uniform in the dimension \(d\) has a negative answer. This follows from
Erdos670.erdos_670.variants.ho(Ho [Ho26]).
theorem erdos_670.variants.uniform_in_dim :
¬ ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ d : ℕ,
∀ A : Finset (EuclideanSpace ℝ (Fin d)), A.card = n → HasSeparatedDistances A →
(1 - ε) * (n : ℝ) ^ 2 ≤ Metric.diam (A : Set (EuclideanSpace ℝ (Fin d)))
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/670.lean, line 114.
Sources
TheoremErdős Problem 672#
Reference: erdosproblems.com/672
Quoted from FormalConjectures/ErdosProblems/672.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/672.
The file states 3 research or textbook statements: 1 open and 2 solved.
Erdos672.erdos_672
Open: stated without proof.
Can the product of an arithmetic progression of positive integers \(n, n + d, ..., n + (k - 1)d\) of length \(k ≥ 4\), with \((n, d) = 1\), be a perfect power?
Erdős believed not, i.e. that
Erdos672With k lholds for all \(k ≥ 4\) and \(l > 1\).
theorem erdos_672 :
∃ᵉ (k ≥ 4) (l > 1), ¬ Erdos672With k l
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/672.lean, line 42.
Erdos672.erdos_672.variants.euler
Solved: stated here; a Lean proof is at https://github.com/herakles-dev/erdos672-four-squares-lean/blob/68adec55180c6103ac5511a5c91c84b25a5044f9/Erdos672/Statement.lean#L41.
According to https://www.erdosproblems.com/672, Euler proved this.
lemma erdos_672.variants.euler :
Erdos672With 4 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/672.lean, line 49.
Erdos672.erdos_672.variants.oblath
Solved: stated here without proof.
According to https://www.erdosproblems.com/672, Obláth proved this.
[Ob51] Oblath, Richard, Eine Bemerkung über Produkte aufeinander folgender Zahlen. J. Indian Math. Soc. (N.S.) (1951), 135-139.
lemma erdos_672.variants.oblath :
Erdos672With 5 2 ∧ Erdos672With 3 3 ∧ Erdos672With 3 4 ∧ Erdos672With 3 5
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/672.lean, line 58.
Sources
TheoremErdős Problem 673#
References: - erdosproblems.com/673 - [Er79e] Erdős, Paul, Some unconventional problems in number theory. Astérisque (1979), 73-82. - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79.
Quoted from FormalConjectures/ErdosProblems/673.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/673.
The file states 4 research or textbook statements: 3 solved and 1 textbook result.
Erdos673.erdos_673.parts.i
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos673.lean#L914.
Let \(1=d_1\lt \cdots \lt d_{\tau(n)}=n\) be the divisors of \(n\) and
\[G(n) = \sum_{1\leq i\lt \tau(n)}\frac{d_i}{d_{i+1}}.\]Is it true that \(G(n)\to \infty\) for almost all \(n\)?
The answer is yes: Tao observed that \(\tau(n/m)/m\leq G(n)\leq \tau(n)\) for any \(m\mid n\) with \(m>1\), so that \(G(n)\) behaves very similarly to \(\tau(n)\). In [Er82e] Erdős recalls this conjecture and observes that it is indeed trivial that \(G(n)\to \infty\) for almost all \(n\).
theorem erdos_673.parts.i : ∀ C : ℝ, {n : ℕ | C < G n}.HasDensity 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/673.lean, line 54.
Erdos673.erdos_673.parts.ii
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos673.lean#L914.
Can one prove an asymptotic formula for \(\sum_{n\leq X}G(n)\)?
Indeed \(\sum_{n\leq X}G(n)\sim X\log X\).
theorem erdos_673.parts.ii :
(fun X : ℕ ↦ ∑ n ∈ Finset.Icc 1 X, G n) ~[atTop] fun X : ℕ ↦ (X : ℝ) * log X
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/673.lean, line 65.
Erdos673.erdos_673.variants.average
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos673.lean#L914.
Erdős writes it is 'easy' to prove \(\frac{1}{X}\sum_{n\leq X}G(n)\to \infty\).
theorem erdos_673.variants.average :
Tendsto (fun X : ℕ ↦ (∑ n ∈ Finset.Icc 1 X, G n) / X) atTop atTop
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/673.lean, line 73.
Erdos673.erdos_673.variants.tao
Textbook result, stated without proof.
Tao observed that, for any divisor \(m\mid n\) with \(m>1\), \(\frac{\tau(n/m)}{m} \leq G(n) \leq \tau(n)\).
theorem erdos_673.variants.tao (n m : ℕ) (hn : 0 < n) (hm : 1 < m) (hmn : m ∣ n) :
((n / m).divisors.card : ℝ) / m ≤ G n ∧ G n ≤ n.divisors.card
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/673.lean, line 80.
Sources
TheoremErdős Problem 674#
References: - erdosproblems.com/674 - [Ko40] Ko, Chao, Note on the Diophantine equation \(x^xy^y=z^z\). J. Chinese Math. Soc. (1940), 31-39.
Quoted from FormalConjectures/ErdosProblems/674.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/674.
The file states 2 research or textbook statements: 2 solved.
Erdos674.erdos_674
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos674.lean.
Are there any integer solutions to \(x^xy^y=z^z\) with \(x,y,z>1\)?
Ko [Ko40] proved there are none if \((x,y)=1\), but there are in fact infinitely many solutions in general - for example, \(x=2^{12}3^6\), \(y = 2^83^8\), and \(z = 2^{11}3^7\).
theorem erdos_674 : solutionSet.Nonempty
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/674.lean, line 45.
Erdos674.erdos_674.variants.infinite
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos674.lean.
There are in fact infinitely many integer solutions to \(x^xy^y=z^z\) with \(x,y,z>1\).
theorem erdos_674.variants.infinite : solutionSet.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/674.lean, line 53.
Sources
TheoremErdős Problem 675#
References: - erdosproblems.com/675 - [Er79] Erdős, Paul, Some unconventional problems in number theory. Math. Mag. (1979), 67-70. - [Ho26] Ho, B. S., A squarefree lower bound for Erdős Problem 675. PDF (2026).
Quoted from FormalConjectures/ErdosProblems/675.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/675.
The file states 5 research or textbook statements: 2 open and 3 solved. It also has 3 test statements, counted here but not shown.
Erdos675.erdos_675.parts.i
Open: stated without proof.
A set \(A \subseteq \mathbb{N}\) has the translation property if, for every \(n\), there is an integer \(t_n \geq 1\) such that, for all \(1 \leq a \leq n\), \(a \in A\) if and only if \(a + t_n \in A\). Does the set of sums of two squares \(\{x^2 + y^2 : x, y \in \mathbb{N}\}\) have the translation property?
theorem erdos_675.parts.i :
HasTranslationProperty {m : ℕ | ∃ x y : ℕ, m = x ^ 2 + y ^ 2}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/675.lean, line 97.
Erdos675.erdos_675.parts.ii
Open: stated without proof.
If we partition all primes into \(P\sqcup Q\), such that each set contains \(\gg x/\log x\) many primes \(\leq x\) for all large \(x\), then can the set of integers only divisible by primes from \(P\) have the translation property?
We read "can" as: is there such a partition for which this set (which contains \(1\)) has the translation property?
theorem erdos_675.parts.ii :
∃ P : Set ℕ, P ⊆ {p : ℕ | p.Prime} ∧
(fun x : ℕ ↦ (x : ℝ) / Real.log x) =O[atTop] (fun x ↦ ((P ∩ Set.Iic x).ncard : ℝ)) ∧
(fun x : ℕ ↦ (x : ℝ) / Real.log x) =O[atTop]
(fun x ↦ ((({p : ℕ | p.Prime} \ P) ∩ Set.Iic x).ncard : ℝ)) ∧
HasTranslationProperty (composedOf P)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/675.lean, line 110.
Erdos675.erdos_675.parts.iii
Solved: stated here without proof.
If \(A\) is the set of squarefree numbers then how fast does the minimal such \(t_n\) grow? Is it true that \(t_n>\exp(n^c)\) for some constant \(c>0\)?
We ask for the inequality for all sufficiently large \(n\), since \(t_1 = 1\).
Ho [Ho26] proved that the answer is yes: for every fixed \(0 < c < 25/72\), \(t_n > \exp(n^c)\) for all sufficiently large \(n\) (Theorem 1.2 and Corollary 3.2); see also the forum discussion.
theorem erdos_675.parts.iii :
∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
Real.exp ((n : ℝ) ^ c) < (minTranslation {m : ℕ | Squarefree m} n : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/675.lean, line 129.
Erdos675.erdos_675.variants.squarefree
Solved: stated here without proof.
Elementary sieve theory implies that the set of squarefree numbers has the translation property (as remarked on erdosproblems.com).
theorem erdos_675.variants.squarefree : HasTranslationProperty {m : ℕ | Squarefree m}
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/675.lean, line 139.
Erdos675.erdos_675.variants.brun
Solved: stated here without proof.
Let \(B \subseteq \mathbb{N}\) be a set of pairwise coprime integers with
\[\sum_{b \in B,\ b < x} \frac{1}{b} = o(\log \log x).\]Then \(A = \{n : b \nmid n \text{ for all } b \in B\}\) has the translation property. As remarked on erdosproblems.com, this follows from Brun's sieve, and Erdős did not know what happens if the condition on the sum is weakened or dropped.
theorem erdos_675.variants.brun (B : Set ℕ) (hB : B.Pairwise Nat.Coprime)
(hsum : (fun x : ℕ ↦ ∑ b ∈ Finset.range x with b ∈ B, (1 : ℝ) / (b : ℝ)) =o[atTop]
fun x : ℕ ↦ Real.log (Real.log (x : ℝ))) :
HasTranslationProperty {n : ℕ | ∀ b ∈ B, ¬ b ∣ n}
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/675.lean, line 151.
Sources
TheoremErdős Problem 676#
References: - erdosproblems.com/676 - [Er79] Erdős, Paul, Some unconventional problems in number theory. Math. Mag. (1979), 67–70. - [Er79d] Erdős, P., Some unconventional problems in number theory. Acta Math. Acad. Sci. Hungar. (1979), 71–80. - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89–115.
Quoted from FormalConjectures/ErdosProblems/676.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/676.
The file states 1 research or textbook statement: 1 open. It also has 3 test statements, counted here but not shown.
Erdos676.erdos_676
Open: stated without proof.
Is every sufficiently large integer of the form \(ap^2+b\) for some prime \(p\) and integers \(a \geq 1\) and \(0 \leq b < p\)?
theorem erdos_676 : ∀ᶠ n in atTop,
∃ a p b : ℕ, p.Prime ∧ 1 ≤ a ∧ b < p ∧ n = a * p ^ 2 + b
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/676.lean, line 84.
Sources
TheoremErdős Problem 677#
Reference: erdosproblems.com/677
Quoted from FormalConjectures/ErdosProblems/677.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/677.
The file states 1 research or textbook statement: 1 open. It also has 1 test statement, counted here but not shown.
Erdos677.erdos_677
Open: stated without proof.
Denote by \(M(n, k)\) the least common multiple of the finite set \(\{n+1, \dotsc, n+k\}\). Is it true that for all \(m \geq n + k\), we get \(M(m, k) \neq M(n, k)\)?
theorem erdos_677 :
∀ (m n k : ℕ), k > 0 → m ≥ n + k → lcmInterval m k ≠ lcmInterval n k
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/677.lean, line 44.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.