Erdős Problem 1052 to Erdős Problem 1071
TheoremErdős Problem 1052#
Reference: erdosproblems.com/1052
Quoted from FormalConjectures/ErdosProblems/1052.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/1052.
The file states 2 research or textbook statements: 1 open and 1 solved. It also has 5 test statements, counted here but not shown.
Erdos1052.erdos_1052
Open: stated without proof.
Are there only finitely many unitary perfect numbers?
theorem erdos_1052 :
{n | IsUnitaryPerfect n}.Finite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1052.lean, line 42.
Erdos1052.even_of_isUnitaryPerfect
Solved: stated here; a Lean proof is at https://github.com/mzhorvath1/formal-conjectures/blob/b70a2ddf5e55f743aac9d4f4a907786b39bc9807/FormalConjectures/ErdosProblems/1052.lean#L46.
All unitary perfect numbers are even.
Formal proof linked here provided by AlphaProof.
theorem even_of_isUnitaryPerfect (n : ℕ) (hn : IsUnitaryPerfect n) : Even n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1052.lean, line 53.
Sources
TheoremErdős Problem 1053#
References: - erdosproblems.com/1053 - [Gu04] Guy, Richard K., Unsolved problems in number theory. Springer-Verlag, New York (2004).
Quoted from FormalConjectures/ErdosProblems/1053.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/1053.
The file states 2 research or textbook statements: 2 open.
Erdos1053.erdos_1053
Open: stated without proof.
Call a number \(k\)-perfect if \(\sigma(n)=kn\), where \(\sigma(n)\) is the sum of the divisors of \(n\). Must \(k=o(\log\log n)\)?
A question of Erdős, as reported in problem B2 of Guy's collection [Gu04]. The little-\(o\) relation is taken as \(n \to \infty\) within the positive integers for which \(\sigma(n) = kn\) for some \(k\); on this set, \(\sigma(n)/n\) is precisely that multiplier \(k\).
theorem erdos_1053 :
(fun n : ℕ ↦ (σ 1 n : ℝ) / (n : ℝ)) =o[atTop ⊓ 𝓟 {n : ℕ | ∃ k, Nat.IsPerfectFor n 1 k}]
(fun n : ℕ ↦ Real.log (Real.log (n : ℝ)))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1053.lean, line 44.
Erdos1053.erdos_1053.variants.guy
Open: stated without proof.
Guy further writes 'It has even been suggested that there may be only finitely many \(k\)-perfect numbers with \(k\geq 3\).'
theorem erdos_1053.variants.guy :
∀ k ≥ 3, {n : ℕ | Nat.IsPerfectFor n 1 k}.Finite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1053.lean, line 54.
Sources
TheoremErdős Problem 1054#
References: - erdosproblems.com/1054 - PALOMAR-2026-10-05-000005
Quoted from FormalConjectures/ErdosProblems/1054.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/1054.
The file states 5 research or textbook statements: 3 solved and 2 textbook results.
Erdos1054.erdos_1054.parts.i
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/0917cd01090b52088aa82b09c8c84689047b8171/erdos-1054/Solution.lean#L97.
Let \(f(n)\) be the minimal integer \(m\) such that \(n\) is the sum of the \(k\) smallest divisors of \(m\) for some \(k\geq 1\). Is it true that \(f(n)=o(n)\)?
The strong claim that \(f(n)=o(n)\) was disproved by Tao in the comments to 468, in which he proves that the upper density of \(\{ n : f(n)\leq \delta n\}\) is \(\ll \delta^2\).
theorem erdos_1054.parts.i : ¬ (fun n ↦ (f n : ℝ)) =o[atTop] (fun n ↦ (n : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1054.lean, line 51.
Erdos1054.erdos_1054.parts.ii
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/0917cd01090b52088aa82b09c8c84689047b8171/erdos-1054/Solution.lean#L103.
Let \(f(n)\) be the minimal integer \(m\) such that \(n\) is the sum of the \(k\) smallest divisors of \(m\) for some \(k\geq 1\). Is it true that \(f(n)=o(n)\) for almost all \(n\)?
No: combining the Tao–Kovač small-ratio bound \(\#\{n \leq X : 0 < f(n) \leq \delta n\} \ll \delta^2 X\) with the fact that almost all odd integers are represented (or via the lower-density bound below), \(f(n)\) is not \(o(n)\) along any density-one set \(A\).
theorem erdos_1054.parts.ii : ¬ ∃ (A : Set ℕ), A.HasDensity 1 ∧
(fun (n : A) ↦ (f ↑n : ℝ)) =o[atTop] (fun n ↦ (n : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1054.lean, line 62.
Erdos1054.erdos_1054.parts.iii
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/0917cd01090b52088aa82b09c8c84689047b8171/erdos-1054/Solution.lean#L110.
Let \(f(n)\) be the minimal integer \(m\) such that \(n\) is the sum of the \(k\) smallest divisors of \(m\) for some \(k\geq 1\). Is it true that \(\limsup f(n)/n=\infty\)?
Yes: for every \(A \geq 1\), a positive lower density of odd integers satisfy \(f(n) > A n\), so \(\limsup f(n)/n = \infty\).
theorem erdos_1054.parts.iii : ∃ (A : Set ℕ), A.HasDensity 1 ∧
atTop.limsup (fun n ↦ (f n : EReal) / n) = ⊤
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1054.lean, line 73.
Erdos1054.f_undefined_at_2
Textbook result, proved here.
Let \(f(n)\) be the minimal integer \(m\) such that \(n\) is the sum of the \(k\) smallest divisors of \(m\) for some \(k\geq 1\). Show that \(f\) is undefined at \(n=2\), i.e. we get the junk value \(0\).
theorem f_undefined_at_2 : f 2 = 0
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1054.lean, line 80.
Erdos1054.f_undefined_at_3
Textbook result, proved here.
Let \(f(n)\) be the minimal integer \(m\) such that \(n\) is the sum of the \(k\) smallest divisors of \(m\) for some \(k\geq 1\). Show that \(f\) is undefined at \(n=5\), i.e. we get the junk value \(0\).
theorem f_undefined_at_3 : f 5 = 0
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1054.lean, line 99.
Sources
TheoremErdős Problem 1055#
Reference: erdosproblems.com/1055
Quoted from FormalConjectures/ErdosProblems/1055.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/1055.
The file states 4 research or textbook statements: 3 open and 1 textbook result.
Erdos1055.exists_p
Textbook result, stated without proof.
A prime \(p\) is in class \(1\) if the only prime divisors of \(p+1\) are \(2\) or \(3\). In general, a prime \(p\) is in class \(r\) if every prime factor of \(p+1\) is in some class \(\leq r-1\), with equality for at least one prime factor. Show that for each \(r\) there exists a prime \(p\) of class \(r\).
theorem exists_p (r : ℕ+) : ∃ p, p.Prime ∧ IsOfClass r p
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1055.lean, line 54.
Erdos1055.erdos_1055
Open: stated without proof.
A prime \(p\) is in class \(1\) if the only prime divisors of \(p+1\) are \(2\) or \(3\). In general, a prime \(p\) is in class \(r\) if every prime factor of \(p+1\) is in some class \(\leq r-1\), with equality for at least one prime factor. Are there infinitely many primes in each class?
theorem erdos_1055 (r) : {p | p.Prime ∧ IsOfClass r p}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1055.lean, line 71.
Erdos1055.erdos_1055.variants.erdos_limit
Open: stated without proof.
A prime \(p\) is in class \(1\) if the only prime divisors of \(p+1\) are \(2\) or \(3\). In general, a prime \(p\) is in class \(r\) if every prime factor of \(p+1\) is in some class \(\leq r-1\), with equality for at least one prime factor. If \(p_r\) is the least prime in class \(r\), then how does \(p_r^{1/r}\) behave? Erdos conjectured that this tends to infinity.
theorem erdos_1055.variants.erdos_limit :
Filter.atTop.Tendsto (fun r ↦ (p r : ℝ) ^ (1 / r : ℝ)) Filter.atTop
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1055.lean, line 80.
Erdos1055.erdos_1055.variants.selfridge_limit
Open: stated without proof.
A prime \(p\) is in class \(1\) if the only prime divisors of \(p+1\) are \(2\) or \(3\). In general, a prime \(p\) is in class \(r\) if every prime factor of \(p+1\) is in some class \(\leq r-1\), with equality for at least one prime factor. If \(p_r\) is the least prime in class \(r\), then how does \(p_r^{1/r}\) behave? Selfridge conjectured that this is bounded.
theorem erdos_1055.variants.selfridge_limit :
∃ M, ∀ r, (p r : ℝ) ^ (1 / r : ℝ) ≤ M
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1055.lean, line 90.
Sources
TheoremErdős Problem 1056#
Reference: erdosproblems.com/1056
Quoted from FormalConjectures/ErdosProblems/1056.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/1056.
The file states 4 research or textbook statements: 2 open and 2 textbook results.
Erdos1056.erdos_1056
Open: stated without proof.
Let \(k ≥ 2\). Does there exist a prime \(p\) and consecutive intervals \(I_0,\dots,I_k\) such that \(\prod\limits_{n{\in}I_i}n \equiv 1 \mod n\) for all \(1 \le i \le k\)?
theorem erdos_1056 :
∀ k ≥ 2, ∃ (p : ℕ) (_ : p.Prime) (boundaries : Fin (k + 1) → ℕ) (_ : StrictMono boundaries),
AllModProdEqualsOne p boundaries
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1056.lean, line 44.
Erdos1056.erdos_1056.variants.k2
Textbook result, proved here.
This is problem A15 in Guy's collection [Gu04], where he reports that in a letter in 1979 Erdős observed that \(3 * 4 \equiv 5 * 6 * 7 \equiv 1 \mod 11\).
theorem erdos_1056.variants.k2 :
AllModProdEqualsOne 11 ![3, 5, 8]
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1056.lean, line 54.
Erdos1056.erdos_1056.variants.k3
Textbook result, proved here.
Makowski [Ma83] found, for \(k=3\): \(2 * 3 * 4 * 5 \equiv 6 * 7 * 8 * 9 * 10 * 11 \equiv 12 * 13 * 14 * 15 \equiv 1 \mod 17\).
theorem erdos_1056.variants.k3 :
AllModProdEqualsOne 17 ![2, 6, 12, 16]
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1056.lean, line 64.
Erdos1056.erdos_1056.variants.noll_simmons
Open: stated without proof.
Noll and Simmons asked, more generally, whether there are solutions to \(q_1! \equiv \dots \equiv q_k! \mod p\) for arbitrarily large \(k\) (with \(q_1 < \dots < q_k\)).
theorem erdos_1056.variants.noll_simmons :
∀ᶠ k in Filter.atTop,
∃ (p : ℕ) (_ : p.Prime) (Q : Fin k → ℕ) (_ : StrictMono Q) (_ : ∀ i, Q i < p),
∀ i j : Fin k, (Q i)! ≡ (Q j)! [MOD p]
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1056.lean, line 74.
Sources
TheoremErdős Problem 1057#
References: - erdosproblems.com/1057 - [AGP94] Alford, W. R. and Granville, Andrew and Pomerance, Carl, There are infinitely many Carmichael numbers. Ann. of Math. (2) (1994), 703--722. - [Er56c] Erdős, P., On pseudoprimes and Carmichael numbers. Publ. Math. Debrecen (1956), 201--206. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437. - [Ha08] Harman, Glyn, Watt's mean value theorem and Carmichael numbers. Int. J. Number Theory (2008), 241--248. - [Li22] J. D. Lichtman, Primes in arithmetic progressions to large moduli and shifted primes without large prime factors. arXiv:2211.09641 (2022). - [Po89] Pomerance, Carl, Two methods in elementary analytic number theory. (1989), 135--161.
Quoted from FormalConjectures/ErdosProblems/1057.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/1057.
The file states 7 research or textbook statements: 2 open and 5 solved.
Erdos1057.erdos_1057
Open: stated without proof.
Is it true that \(C(x)=x^{1-o(1)}\)?
This is discussed in problem A13 of Guy's collection [Gu04].
theorem erdos_1057 :
Tendsto (fun x ↦ Real.log (carmichaelCounting x) / Real.log x) atTop (𝓝 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1057.lean, line 57.
Erdos1057.erdos_1057.variants.upper_bound
Solved: stated here without proof.
Erdős [Er56c] proved \(C(x) < x \exp\left(-c \frac{\log x\log\log\log x}{\log\log x}\right)\) for some constant \(c>0\).
theorem erdos_1057.variants.upper_bound :
∃ c > 0, ∀ᶠ x in atTop,
carmichaelCounting x < x * Real.exp (-c * (Real.log x * Real.log (Real.log (Real.log x))) /
Real.log (Real.log x))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1057.lean, line 66.
Erdos1057.erdos_1057.variants.pomerance
Open: stated without proof.
Pomerance [Po89] gave a heuristic suggesting that this is the true order of growth, and in fact \(C(x)= x \exp\left(-(1+o(1))\frac{\log x\log\log\log x}{\log\log x}\right)\).
theorem erdos_1057.variants.pomerance :
Tendsto (fun x ↦
-(Real.log (carmichaelCounting x / x) * Real.log (Real.log x)) /
(Real.log x * Real.log (Real.log (Real.log x)))) atTop (𝓝 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1057.lean, line 77.
Erdos1057.erdos_1057.variants.agp_infinite
Solved: stated here without proof.
Alford, Granville, and Pomerance [AGP94] proved that \(C(x)\to \infty\).
theorem erdos_1057.variants.agp_infinite :
Tendsto carmichaelCounting atTop atTop
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1057.lean, line 87.
Erdos1057.erdos_1057.variants.agp_lower_bound
Solved: stated here without proof.
Alford, Granville, and Pomerance [AGP94] proved that \(C(x)>x^{2/7}\) for large \(x\).
theorem erdos_1057.variants.agp_lower_bound :
∀ᶠ x in atTop, carmichaelCounting x > x ^ (2 / 7 : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1057.lean, line 95.
Erdos1057.erdos_1057.variants.harman_lower_bound
Solved: stated here without proof.
The lower bound \(C(x)> x^{0.33336704}\) was proved by Harman [Ha08].
theorem erdos_1057.variants.harman_lower_bound :
∀ᶠ x in atTop, carmichaelCounting x > x ^ (0.33336704 : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1057.lean, line 103.
Erdos1057.erdos_1057.variants.lichtman_lower_bound
Solved: stated here without proof.
This exponent was improved to \(0.3389\) by Lichtman [Li22].
theorem erdos_1057.variants.lichtman_lower_bound :
∀ᶠ x in atTop, carmichaelCounting x > x ^ (0.3389 : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1057.lean, line 111.
Sources
TheoremErdős Problem 1058#
References: - erdosproblems.com/1058 - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437. - [Lu01] Luca, Florian, On a conjecture of Erdős and Stewart. Math. Comp. (2001), 893-896.
Quoted from FormalConjectures/ErdosProblems/1058.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/1058.
The file states 2 research or textbook statements: 2 solved.
Erdos1058.erdos_1058
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1058.lean#L47.
Let \(2=p_1\lt p_2\lt \cdots\) be the sequence of prime numbers. Are there only finitely many \(n\) such that \(n\in [p_{k-1},p_k)\) and the only primes dividing \(n!+1\) are \(p_{k}\) and \(p_{k+1}\)?
A conjecture of Erdős and Stewart, as reported in problem A2 of Guy's collection [Gu04]. The only known cases are \(n=1,2,3,4,5\). Luca [Lu01] proved that indeed these are the only solutions.
theorem erdos_1058 : {n | IsSolution n}.Finite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1058.lean, line 55.
Erdos1058.erdos_1058.variants.luca
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1058.lean#L47.
Luca [Lu01] proved that \(n = 1, 2, 3, 4, 5\) are the only solutions.
theorem erdos_1058.variants.luca : {n | IsSolution n} = {1, 2, 3, 4, 5}
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1058.lean, line 62.
Sources
TheoremErdős Problem 1059#
Reference: erdosproblems.com/1059
Quoted from FormalConjectures/ErdosProblems/1059.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/1059.
The file states 1 research or textbook statement: 1 open. It also has 7 test statements, counted here but not shown.
Erdos1059.erdos_1059
Open: stated without proof.
Are there infinitely many primes \(p\) such that \(p - k!\) is composite for each \(k\) such that \(1 ≤ k! < p\)?
theorem erdos_1059 :
Set.Infinite {p | p.Prime ∧ AllFactorialSubtractionsComposite p}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1059.lean, line 41.
Sources
TheoremErdős Problem 1060#
Reference: erdosproblems.com/1060
Quoted from FormalConjectures/ErdosProblems/1060.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/1060.
The file states 2 research or textbook statements: 2 open.
Erdos1060.erdos_1060.parts.i
Open: stated without proof.
The conjecture is about the function \(f(n)\) which counts the number of solutions to \(k\sigma(k)=n\), where \(\sigma(k)\) is the sum of divisors of \(k\). The first bound is that \(f(n)\) grows slower than any power of \(n^(\frac{1}{\log\log n})\). The second bound is that \(f(n)\) is at most a power of \(\log n\).
theorem erdos_1060.parts.i :
∃ h : ℕ → ℝ,
h =o[atTop] (fun n ↦ 1 / log (log n)) ∧ ∀ᶠ n in atTop, #{k ≤ n | k * σ 1 k = n} ≤ (n : ℝ) ^ h n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1060.lean, line 40.
Erdos1060.erdos_1060.parts.ii
Open: stated without proof.
Part (ii) of Erdős Problem 1060: bound on the number of \(k \le n\) with \(k \sigma_1(k) = n\).
theorem erdos_1060.parts.ii :
∃ (C : ℝ), (fun n ↦ (#{k ≤ n | k * σ 1 k = n} : ℝ)) =O[atTop]
(fun n ↦ log n ^ C)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1060.lean, line 46.
Sources
TheoremErdős Problem 1061#
References: - erdosproblems.com/1061 - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), Problem B15.
Quoted from FormalConjectures/ErdosProblems/1061.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/1061.
The file states 1 research or textbook statement: 1 open.
Erdos1061.erdos_1061
Open: stated without proof.
How many (ordered) solutions are there to
σ(a) + σ(b) = σ(a + b)witha + b ≤ x? Is it true that this number is asymptotic toc * xfor some constantc > 0?
theorem erdos_1061 : ∃ c : ℝ, 0 < c ∧ S ~[atTop] (fun x : ℝ ↦ c * x)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1061.lean, line 49.
Sources
TheoremErdős Problem 1062#
Reference: erdosproblems.com/1062
Quoted from FormalConjectures/ErdosProblems/1062.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/1062.
The file states 3 research or textbook statements: 1 open and 2 solved.
Erdos1062.erdos_1062.parts.ii
Open: stated without proof.
Erdős asked whether the limiting density
f n / nexists and, if so, whether it is irrational.
theorem erdos_1062.parts.ii :
∃ l, Tendsto (fun n => (f n : ℝ) / n) atTop (𝓝 l) ∧ Irrational l
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1062.lean, line 49.
Erdos1062.erdos_1062.variants.lower_bound
Proved here.
The interval
[⌊n/3⌋, n]is fork-free, and thereforef nis at least⌈2n / 3⌉.
theorem erdos_1062.variants.lower_bound (n : ℕ) : ⌈(2 * n / 3 : ℝ)⌉₊ ≤ f n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1062.lean, line 55.
Erdos1062.erdos_1062.variants.lebensold_bounds
Solved: stated here without proof.
Lebensold proved that for large
n, the functionf nlies between0.6725 nand0.6736 n.
theorem erdos_1062.variants.lebensold_bounds :
∀ᶠ n in atTop, (0.6725 : ℝ) * n ≤ f n ∧ f n ≤ (0.6736 : ℝ) * n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1062.lean, line 82.
Sources
TheoremErdős Problem 1063#
References: * erdosproblems.com/1063 * [ErSe83] Erdos, P. and Selfridge, J. L., Problem 6447. Amer. Math. Monthly (1983), 710. * [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), Problem B31. * [Mo85] Monier, Jean-Marie, Problems and Solutions: Solutions of Advanced Problems: 6447. Amer. Math. Monthly 92 (1985), 435-436. * [Ku+26] Kung, P.-N., Song, L., Hwang, D., Yoon, J., Li, C.-L., Severini, S., Olšák, M., Lockhart, E., Le, Q. V., Gokturk, B., Luong, T., Pfister, T., & Peng, N. (2026). LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks. arXiv:2606.03303.
Quoted from FormalConjectures/ErdosProblems/1063.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/1063.
The file states 7 research or textbook statements: 1 open and 6 solved.
Erdos1063.erdos_1063.better_upper
Open: stated without proof.
Estimate \(n_k\) by finding a better upper bound than Cambie's \(n_k \leq k \cdot \operatorname{lcm}(1, \dotsc, k-1)\).
The comparator takes its least common multiple in
ℕand casts the result. Writing the ascription as((… ).lcm (fun n : ℕ => n) : ℝ)instead puts it on theFinset.lcmapplication, so the coercion lands onnand thelcmis taken inℝ, wherelcmof non-zero elements is1and the whole comparator collapses tok.
theorem erdos_1063.better_upper :
(fun k => (n k : ℝ)) =O[atTop] erdos_1063.better_upper.answer ∧
erdos_1063.better_upper.answer =o[atTop] fun k =>
(k : ℝ) * (((Finset.Icc 1 (k - 1)).lcm id : ℕ) : ℝ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1063.lean, line 61.
Erdos1063.erdos_1063.variants.subexponential_upper_bound
Solved: stated here; a Lean proof is at https://github.com/lfsong-google/formal-conjectures/blob/ff33e501bb78a90ae4703e22e052f8bb38e10146/FormalConjectures/ErdosProblems/1063.lean#L5524.
An improved upper bound \(n_k \ll \exp\left(\frac{k}{\log k}(\log \log k + \log \log \log k + \log 2)\right)\), which is \(o\bigl(k \cdot \operatorname{lcm}(1, \dotsc, k - 1)\bigr)\), was formally proved in Lean 4 by the LEAP prover agent [Ku+26] (see the linked
formal_proof). This is an improvement over another upper bound propsed here.
theorem erdos_1063.variants.subexponential_upper_bound :
let upper_bound : ℕ → ℝ := fun k =>
Real.exp ((k : ℝ) / Real.log k *
(Real.log (Real.log k) + Real.log (Real.log (Real.log k)) + Real.log 2))
(fun k => (n k : ℝ)) =O[atTop] upper_bound ∧
upper_bound =o[atTop] fun k =>
(k : ℝ) * (((Finset.Icc 1 (k - 1)).lcm id : ℕ) : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1063.lean, line 78.
Erdos1063.erdos_1063.variants.exists_exception
Solved: stated here; a Lean proof is at https://github.com/lfsong-google/formal-conjectures/blob/ff33e501bb78a90ae4703e22e052f8bb38e10146/FormalConjectures/ErdosProblems/1063.lean#L5533.
Erdős and Selfridge noted that, for \(n \ge 2k\) with \(k \ge 2\), at least one of the numbers \(n - i\) for \(0 \le i < k\) fails to divide \(\binom{n}{k}\) ([ErSe83]).
theorem erdos_1063.variants.exists_exception {n k : ℕ} (hk : 2 ≤ k) (h : 2 * k ≤ n) :
∃ i < k, ¬ (n - i) ∣ n.choose k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1063.lean, line 95.
Erdos1063.erdos_1063.variants.small_values
Proved here.
The initial values satisfy \(n_2 = 4\), \(n_3 = 6\), \(n_4 = 9\), and \(n_5 = 12\) ([Gu04], Problem B31).
theorem erdos_1063.variants.small_values :
n 2 = 4 ∧ n 3 = 6 ∧ n 4 = 9 ∧ n 5 = 12
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1063.lean, line 101.
Erdos1063.erdos_1063.variants.monier_upper_bound
Solved: stated here; a Lean proof is at https://github.com/lfsong-google/formal-conjectures/blob/ff33e501bb78a90ae4703e22e052f8bb38e10146/FormalConjectures/ErdosProblems/1063.lean#L5537.
Monier observed that \(n_k \le k!\) for \(k \ge 3\) ([Mo85]), since \(\binom{k!}{k}\) is divisible by \(k! - i\) for \(1 \le i < k\).
The hypothesis
3 ≤ kis necessary. At \(k = 2\) the bound is false: \(n_2 = 4\) and \(2! = 2\).
theorem erdos_1063.variants.monier_upper_bound {k : ℕ} (hk : 3 ≤ k) :
n k ≤ k !
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1063.lean, line 146.
Erdos1063.erdos_1063.variants.cambie_upper_bound
Solved: stated here; a Lean proof is at https://github.com/lfsong-google/formal-conjectures/blob/ff33e501bb78a90ae4703e22e052f8bb38e10146/FormalConjectures/ErdosProblems/1063.lean#L5541.
Cambie observed the improved bound \(n_k \le k \cdot \operatorname{lcm}(1, \dotsc, k - 1)\).
The hypothesis
3 ≤ kis necessary here too. At \(k = 2\) the right hand side is \(2 \cdot \operatorname{lcm}(1) = 2\), while \(n_2 = 4\).The source writes the bound as \(k[2, 3, \dotsc, k-1]\). That agrees with the range used here, because including \(1\) does not change a least common multiple.
theorem erdos_1063.variants.cambie_upper_bound {k : ℕ} (hk : 3 ≤ k) :
n k ≤ k * (Finset.Icc 1 (k - 1)).lcm id
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1063.lean, line 162.
Erdos1063.erdos_1063.variants.exp_upper_bound
Solved: stated here; a Lean proof is at https://github.com/lfsong-google/formal-conjectures/blob/ff33e501bb78a90ae4703e22e052f8bb38e10146/FormalConjectures/ErdosProblems/1063.lean#L5545.
The least common multiple bound implies \(n_k \le \exp((1 + o(1))k)\).
theorem erdos_1063.variants.exp_upper_bound :
∃ f : ℕ → ℝ, Tendsto f atTop (𝓝 0) ∧
∀ k, (n k : ℝ) ≤ exp ((1 + f k) * k)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1063.lean, line 171.
Sources
TheoremErdős Problem 1064#
Reference: erdosproblems.com/1064
Quoted from FormalConjectures/ErdosProblems/1064.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/1064.
The file states 3 research or textbook statements: 3 solved.
Erdos1064.erdos_1064
Solved: stated here without proof.
Let \(ϕ(n)\) be the Euler's totient function, then the \(n\) satisfies \(ϕ(n)>ϕ(n - ϕ(n))\) have asymptotic density 1. Reference: [LuPo02] Luca, Florian and Pomerance, Carl, On some problems of {M}\polhk akowski-{S}chinzel and {E}rd\H os concerning the arithmetical functions {\(\phi\)} and {\(\sigma\)}. Colloq. Math.
theorem erdos_1064 : {n | φ n > φ (n - φ n)}.HasDensity 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1064.lean, line 40.
Erdos1064.erdos_1064.variants.k2
Proved here.
Let \(ϕ(n)\) be the Euler's totient function, there exist infinitely many \(n\) such that \(ϕ(n)< ϕ(n - ϕ(n))\) Reference: [GLW01] Grytczuk, A. and Luca, F. and W\'ojtowicz, M., A conjecture of {E}rdős concerning inequalities for the {E}uler totient function.
theorem erdos_1064.variants.k2 : {n | φ n < φ (n - φ n)}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1064.lean, line 50.
Erdos1064.erdos_1064.variants.general_function
Solved: stated here without proof.
For any function \(f(n)=o(n)\), we have \(\phi(n)>\phi(n-\phi(n))+f(n)\) for almost all \(n\). Reference: [LuPo02] Luca, Florian and Pomerance, Carl, On some problems of {M}\polhk akowski-{S}chinzel and {E}rd\H os concerning the arithmetical functions {\(\phi\)} and {\(\sigma\)}. Colloq. Math. (2002), 111--130.
theorem erdos_1064.variants.general_function (f : ℕ → ℕ)
(hf : (fun n ↦ (f n : ℝ)) =o[atTop] (fun n ↦ (n : ℝ))) :
{n : ℕ | φ (n - φ n) + f n < φ n}.HasDensity 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1064.lean, line 87.
Sources
TheoremErdős Problem 1065#
Reference: erdosproblems.com/1065
Quoted from FormalConjectures/ErdosProblems/1065.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/1065.
The file states 2 research or textbook statements: 2 open.
Erdos1065.erdos_1065.parts.i
Open: stated without proof.
Are there infinitely many primes \(p\) such that \(p = 2^k * q + 1\) for some prime \(q\) and \(k ≥ 0\)?
This is mentioned as B46 in Unsolved Problems in Number Theory by Richard K. Guy
theorem erdos_1065.parts.i :
Set.Infinite {p | ∃ q k, p.Prime ∧ q.Prime ∧ p = 2^k * q + 1}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1065.lean, line 39.
Erdos1065.erdos_1065.parts.ii
Open: stated without proof.
Are there infinitely many primes \(p\) such that \(p = 2^k 3^l q + 1\) for some prime \(q\) and \(k ≥ 0\), \(l ≥ 0\)?
theorem erdos_1065.parts.ii :
Set.Infinite {p | ∃ q k l, p.Prime ∧ q.Prime ∧ p = 2^k * 3^l * q + 1}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1065.lean, line 48.
Sources
TheoremErdős Problem 1066#
References: - erdosproblems.com/1066 - [Cs98] Csizmadia, G., On the independence number of minimum distance graphs. Discrete Comput. Geom. 20 (1998), 179-187. - [Er87b] Erdős, P., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985) (1987), 167-177. - [PaTo96] Pach, J. and Tóth, G., On the independence number of coin graphs. Geombinatorics 6 (1996), 30-33. - [Po85] Pollack, R., Increasing the minimum distance of a set of points. J. Combin. Theory Ser. A 40 (1985), 450. - [Sw02] Swanepoel, K. J., Independence numbers of planar contact graphs. Discrete Comput. Geom. 28 (2002), 649-670.
Quoted from FormalConjectures/ErdosProblems/1066.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/1066.
The file states 5 research or textbook statements: 2 open and 3 solved. It also has 1 API statement, counted here but not shown.
Erdos1066.erdos_1066
Open: stated without proof.
Let \(G\) be a graph given by \(n\) points in \(\mathbb{R}^2\), where any two distinct points are at least distance \(1\) apart, and we draw an edge between two points if they are distance \(1\) apart.
Let \(g(n)\) be maximal such that any such graph always has an independent set on at least \(g(n)\) vertices. Estimate \(g(n)\), or perhaps \(\lim \frac{g(n)}{n}\).
We ask for \(\lim g(n)/n\). The limit exists by Fekete's lemma, since placing two configurations far apart shows \(g(a+b) \leq g(a)+g(b)\).
theorem erdos_1066 :
Tendsto (fun n : ℕ ↦ (g n : ℝ) / n) atTop (𝓝 erdos_1066.answer)
Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1066.lean, line 84.
Erdos1066.erdos_1066.variants.pollack
Solved: stated here without proof.
Such graphs are always planar. Pollack [Po85] noted that the Four colour theorem implies \(g(n)\geq n/4\), since the graph is planar.
theorem erdos_1066.variants.pollack (n : ℕ) : (n : ℝ) / 4 ≤ (g n : ℝ)
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1066.lean, line 93.
Erdos1066.erdos_1066.variants.swanepoel
Solved: stated here without proof.
This lower bound has been improved to \(\frac{9}{35}n\) by Csizmadia [Cs98] and then \(\frac{8}{31}n\) by Swanepoel [Sw02].
theorem erdos_1066.variants.swanepoel (n : ℕ) : (8 / 31 : ℝ) * n ≤ (g n : ℝ)
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1066.lean, line 101.
Erdos1066.erdos_1066.variants.pach_toth
Solved: stated here without proof.
Erdős initially thought that \(g(n)=n/3\), but Chung and Graham, and independently Pach, gave a construction that shows \(g(n)\leq \frac{6}{19}n\). Pach and Tóth [PaTo96] improved this to \(g(n)\leq \frac{5}{16}n\).
Since \(g(1) = 1\), the bound cannot hold for all \(n\), so it is stated for infinitely many \(n\), with \(5/16\) replaced by \(5/16+\varepsilon\) for every \(\varepsilon > 0\).
theorem erdos_1066.variants.pach_toth :
∀ ε > (0 : ℝ), ∃ᶠ n : ℕ in atTop, (g n : ℝ) ≤ (5 / 16 + ε) * n
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1066.lean, line 113.
Erdos1066.erdos_1066.variants.higher_dim
Open: stated without proof.
Pollack [Po85] also reports a letter from Erdős which poses the more general problem of, given \(n\) points in \(\mathbb{R}^d\) with minimum distance \(1\), let \(g_d(n)\) be maximal such that there always exist at least \(g_d(n)\) many points which have minimum distance \(>1\). Is it true that \(g_d(n) \gg n/d\) in general?
We read this with a constant independent of \(d\) and \(n\).
theorem erdos_1066.variants.higher_dim :
∃ c > (0 : ℝ), ∀ d n : ℕ, 1 ≤ d → c * n / d ≤ (gDim d n : ℝ)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1066.lean, line 126.
Sources
TheoremErdős Problem 1067#
References: - erdosproblems.com/1067 - [BoPi24] N. Bowler and M. Pitz, A note on uncountably chromatic graphs. arXiv:2402.05984 (2024). - [ErHa66] Erdős, P. and Hajnal, A., On chromatic number of graphs and set-systems. Acta Math. Acad. Sci. Hungar. (1966), 61-99. - [Ko13] Komjáth, Péter, A note on chromatic number and connectivity of infinite graphs. Israel J. Math. (2013), 499--506. - [So15] Soukup, Dániel T., Trees, ladders and graphs. J. Combin. Theory Ser. B (2015), 96--116. - [Th17] Thomassen, Carsten, Infinitely connected subgraphs in graphs of uncountable chromatic number. Combinatorica (2017), 785--793.
Quoted from FormalConjectures/ErdosProblems/1067.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/1067.
The file states 2 research or textbook statements: 2 solved.
Erdos1067.erdos_1067
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1067.lean.
Does every graph with chromatic number \(\aleph_1\) contain an infinitely connected subgraph with chromatic number \(\aleph_1\)?
Komjáth [Ko13] proved that it is consistent that the answer is no. This was improved by Soukup [So15], who constructed a counterexample using no extra set-theoretical assumptions. A simpler elementary example was given by Bowler and Pitz [BoPi24].
This was formalized in Lean by Alexeev using Aristotle and Aleph Prover.
theorem erdos_1067 :
¬ ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = ℵ_ 1 →
∃ (H : G.Subgraph), H.coe.chromaticCardinal = ℵ_ 1 ∧ InfinitelyConnected H.coe
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1067.lean, line 61.
Erdos1067.erdos_1067.variants.infinite_edge_connectivity
Solved: stated here without proof.
Does every graph with chromatic number \(\aleph_1\) contain an infinitely edge-connected subgraph with chromatic number \(\aleph_1\)?
Thomassen [Th17] proved that the answer is yes: every graph of uncountable chromatic number has a subgraph with infinite edge-connectivity and uncountable chromatic number.
theorem erdos_1067.variants.infinite_edge_connectivity :
∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = ℵ_ 1 →
∃ (H : G.Subgraph), H.coe.chromaticCardinal = ℵ_ 1 ∧ InfinitelyEdgeConnected H.coe
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1067.lean, line 74.
Sources
TheoremErdős Problem 1068#
Reference: erdosproblems.com/1068
Quoted from FormalConjectures/ErdosProblems/1068.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/1068.
The file states 1 research or textbook statement: 1 open.
Erdos1068.erdos_1068
Open: stated without proof.
Does every graph with chromatic number \(\aleph_1\) contain a countable subgraph which is infinitely connected?
theorem erdos_1068 :
∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = ℵ_ 1 →
∃ s : Set V, s.Countable ∧ InfinitelyConnected (G.induce s)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1068.lean, line 37.
Sources
TheoremErdős Problem 1069#
References: - erdosproblems.com/1069 - [Er87b] Erdős, P., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985) (1987), 167-177. - [Sa87] Sah, C.-H., The rich line problem of P. Erdős. (1987), 123-125. - [SzTr83] Szemerédi, E. and Trotter, Jr., W. T., Extremal problems in discrete geometry. Combinatorica (1983), 381-392.
Quoted from FormalConjectures/ErdosProblems/1069.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/1069.
The file states 2 research or textbook statements: 1 solved and 1 textbook result. It also has 1 API statement, counted here but not shown.
Erdos1069.erdos_1069
Solved: stated here without proof.
Given any \(n\) points in \(\mathbb{R}^2\), the number of \(k\)-rich lines (lines which contain \(\geq k\) of the points) is, provided \(k\leq n^{1/2}\),
\[\ll \frac{n^2}{k^3}.\]Erdős [Er87b] describes this as a conjecture of himself, Croft, and Purdy. It was proved by Szemerédi and Trotter [SzTr83]. We take \(k \geq 2\), since for \(k \leq 1\) there are infinitely many \(k\)-rich lines.
theorem erdos_1069 :
∃ C : ℝ, 0 < C ∧ ∀ (n k : ℕ) (s : Finset ℝ²), s.card = n → 2 ≤ k →
(k : ℝ) ≤ Real.sqrt n →
((richLines s k).ncard : ℝ) ≤ C * (n : ℝ) ^ 2 / (k : ℝ) ^ 3
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1069.lean, line 62.
Erdos1069.erdos_1069.variants.lattice
Textbook result, stated without proof.
When \(k=n^{1/2}\) the lattice points show that there can be \(\geq(2+o(1))n^{1/2}\) many \(n^{1/2}\)-rich lines: for \(n=m^2\) the \(m\times m\) grid has \(2m\) lines with \(m\) points each. Erdős thought that perhaps this is best possible, but Sah [Sa87] gave a construction achieving \(\geq (3+o(1))n^{1/2}\) many \(n^{1/2}\)-rich lines.
theorem erdos_1069.variants.lattice (m : ℕ) (hm : 2 ≤ m) :
∃ s : Finset ℝ², s.card = m ^ 2 ∧ 2 * m ≤ (richLines s m).ncard
Category textbook; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1069.lean, line 75.
Sources
TheoremErdős Problem 1070#
References: - erdosproblems.com/1070 - [DuVa26] Dúcz, Á. and Varga, D., A unit-distance graph in the plane with independence ratio below 1/4. arXiv:2606.28157 (2026). - [Er87b] Erdős, P., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985) (1987), 167-177. PDF - [MRVZ23] Matolcsi, M., Ruzsa, I. Z., Varga, D. and Zsámboki, P., The fractional chromatic number of the plane is at least \(4\). arXiv:2311.10069 (2023).
If we also insist that no two points are distance \(<1\) apart, we get erdosproblems.com/1066.
Quoted from FormalConjectures/ErdosProblems/1070.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/1070.
The file states 5 research or textbook statements: 1 open, 3 solved and 1 textbook result. It also has 1 API statement, counted here but not shown.
Erdos1070.erdos_1070.parts.i
Open: stated without proof.
Let \(f(n)\) be maximal such that, given any \(n\) points in \(\mathbb{R}^2\), there exist \(f(n)\) points such that no two are distance \(1\) apart. Estimate \(f(n)\). In particular, is it true that \(f(n)\geq n/4\)?
This is the first part, a problem of Erdős [Er87b, p. 171]. Since \(f(n)=\Theta(n)\) is already known, we ask for \(\lim f(n)/n\). The limit exists by Fekete's lemma, since placing two configurations far apart shows \(f(a+b) \leq f(a)+f(b)\).
theorem erdos_1070.parts.i :
Tendsto (fun n : ℕ ↦ (f n : ℝ) / n) atTop (𝓝 erdos_1070.parts.i.answer)
Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1070.lean, line 75.
Erdos1070.erdos_1070.parts.ii
Solved: stated here without proof.
Let \(f(n)\) be maximal such that, given any \(n\) points in \(\mathbb{R}^2\), there exist \(f(n)\) points such that no two are distance \(1\) apart. Estimate \(f(n)\). In particular, is it true that \(f(n)\geq n/4\)?
This is the second part, read as the inequality for every \(n\). The answer is no: Dúcz and Varga [DuVa26, Theorem 1] construct a finite unit distance graph \(G\) in the plane with \(\alpha(G) < |V(G)|/4\). For its vertex set \(X\),
f_le Xgives \(f(|X|) \leq \alpha(U_X) \leq \alpha(G) < |X|/4\), where \(U_X\) is the unit distance graph on \(X\).
theorem erdos_1070.parts.ii : ¬ ∀ n : ℕ, (n : ℝ) / 4 ≤ (f n : ℝ)
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1070.lean, line 90.
Erdos1070.erdos_1070.variants.moser_spindle
Textbook result, stated without proof.
The Moser spindle shows \(f(n)\leq \frac{2}{7}n\approx 0.285n\).
The Moser spindle has \(7\) points and independence number \(2\), so \(m\) far-apart copies give the bound for \(n=7m\).
theorem erdos_1070.variants.moser_spindle (m : ℕ) : f (7 * m) ≤ 2 * m
Category textbook; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1070.lean, line 100.
Erdos1070.erdos_1070.variants.matolcsi_ruzsa_varga_zsamboki_graphs
Solved: stated here without proof.
Matolcsi, Ruzsa, Varga, and Zsámboki [MRVZ23, Section 3, after Theorem 2] showed that for every \(\varepsilon>0\) there is a finite unit distance graph \(G\subseteq\mathbb{R}^2\) whose largest independent set has size at most \((1/4+\varepsilon)|G|\).
theorem erdos_1070.variants.matolcsi_ruzsa_varga_zsamboki_graphs :
∀ ε > (0 : ℝ), ∃ X : Finset ℝ², X.Nonempty ∧
((UnitDistancePlaneGraph (X : Set ℝ²)).indepNum : ℝ) ≤ (1 / 4 + ε) * X.card
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1070.lean, line 109.
Erdos1070.erdos_1070.variants.matolcsi_ruzsa_varga_zsamboki
Solved: stated here without proof.
Matolcsi, Ruzsa, Varga, and Zsámboki [MRVZ23] have improved the upper bound to
\[f(n) \leq \left(\frac{1}{4}+o(1)\right)n.\]This follows from the previous statement by taking disjoint copies of the graph far apart.
theorem erdos_1070.variants.matolcsi_ruzsa_varga_zsamboki :
∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (f n : ℝ) ≤ (1 / 4 + ε) * n
Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1070.lean, line 121.
Sources
TheoremErdős Problem 1071#
References: * erdosproblems.com/1071 * [Da85] Danzer, L., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985), 167-177.
Quoted from FormalConjectures/ErdosProblems/1071.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/1071.
The file states 2 research or textbook statements: 2 solved.
Erdos1071.erdos_1071.parts.i
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1071.lean.
Can a finite set of disjoint unit segments in a unit square be maximal? Solved affirmatively by [Da85], who gave an explicit construction.
This was formalized in Lean by Alexeev using Aristotle and ChatGPT.
theorem erdos_1071.parts.i :
∃ S : Finset (ℝ² × ℝ²),
Maximal (fun T : Finset (ℝ² × ℝ²) =>
(∀ seg ∈ T, dist seg.1 seg.2 = 1 ∧
seg.1 0 ∈ Icc 0 1 ∧ seg.1 1 ∈ Icc 0 1 ∧
seg.2 0 ∈ Icc 0 1 ∧ seg.2 1 ∈ Icc 0 1) ∧
(T : Set (ℝ² × ℝ²)).Pairwise SegmentsDisjoint) S
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1071.lean, line 47.
Erdos1071.erdos_1071.parts.ii
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1071b.lean.
Is there a region \(R\) with a maximal set of disjoint unit line segments that is countably infinite? Here a unit line segment is a rotated and translated copy of the open interval \((0,1)\), and it is required to be contained in \(R\). Solved affirmatively by [Fo99], who gave an explicit construction.
This was formalized in Lean by Alexeev using Aristotle and ChatGPT.
theorem erdos_1071.parts.ii :
∃ (R : Set ℝ²) (S : Set (ℝ² × ℝ²)),
IsOpen R ∧ IsConnected R ∧ S.Countable ∧ S.Infinite ∧
Maximal (fun T : Set (ℝ² × ℝ²) =>
(∀ seg ∈ T, dist seg.1 seg.2 = 1 ∧ openSegment ℝ seg.1 seg.2 ⊆ R) ∧
T.Pairwise SegmentsDisjoint) S
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1071.lean, line 65.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.