Erdős Problem 824 to Erdős Problem 844
TheoremErdős Problem 824#
References: - erdosproblems.com/824 - [Er59c] Erdős, P., Remarks on number theory. II. Some problems on the \(\sigma\) function. Acta Arith. (1959), 171--177. - [Er74b] Erdős, P., Remarks on some problems in number theory. Math. Balkanica (1974), 197-202. - [PoPo16] Pollack, Paul and Pomerance, Carl, Some problems of Erdős on the sum-of-divisors function. Trans. Amer. Math. Soc. Ser. B (2016), 1-26. - [LiZh26] Li, Shisheng and Zhuang, Zhong, Coprime pairs with equal sum of divisors, assuming smooth shifted primes. Preprint (October 2026). github.com/daizisheng/erdos-824 - [OpenAI26] OpenAI, Weighted dilation graphs, smooth shifted primes and totient fibers. OpenAI Math Release preprint (September 2026). github.com/openai/math
Quoted from FormalConjectures/ErdosProblems/824.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/824.
The file states 3 research or textbook statements: 1 open and 2 solved.
Erdos824.erdos_824
Solved: stated here; a Lean proof is at https://github.com/cadamcat/equal-divisor-sums-lean4/blob/6280393739de142f3c54160ce7083110ed55f194/Erdos824/Theorem.lean#L17.
Let \(h(x)\) count the number of integers \(1\leq a\lt b\lt x\) such that \((a,b)=1\) and \(\sigma(a)=\sigma(b)\), where \(\sigma\) is the sum of divisors function. Is it true that \(h(x)>x^{2-o(1)}\)?
That is, is it true that for every \(\epsilon > 0\) we have \(h(x) > x^{2-\epsilon}\) for all large \(x\)? According to erdosproblems.com, Erdős [Er74b] proved that \(\limsup h(x)/x = \infty\) and claimed a similar proof for this problem.
theorem erdos_824 :
∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℕ in atTop, (x : ℝ) ^ (2 - ε) < (h x : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/824.lean, line 73.
Erdos824.erdos_824.variants.pollack_pomerance
Solved: stated here without proof.
Pollack and Pomerance [PoPo16, Section 6] proved that \(h(x)/x \to \infty\), answering a question of Erdős [Er59c].
theorem erdos_824.variants.pollack_pomerance :
Tendsto (fun x : ℕ ↦ (h x : ℝ) / (x : ℝ)) atTop atTop
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/824.lean, line 82.
Erdos824.erdos_824.variants.squarefree
Open: stated without proof.
A similar question can be asked if the condition \((a,b)=1\) is replaced by the condition that \(a\) and \(b\) are squarefree. Let \(h'(x)\) count the number of squarefree integers \(1\leq a\lt b\lt x\) with \(\sigma(a)=\sigma(b)\). Is it true that \(h'(x)>x^{2-o(1)}\)?
theorem erdos_824.variants.squarefree :
∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℕ in atTop, (x : ℝ) ^ (2 - ε) < (hSquarefree x : ℝ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/824.lean, line 92.
Sources
TheoremErdős Problem 825#
Reference: erdosproblems.com/825
Quoted from FormalConjectures/ErdosProblems/825.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/825.
The file states 2 research or textbook statements: 2 solved.
Erdos825.erdos_825
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/dfe2d78128b493c572cf525b1b8edf4897fb7664/src/latest/ErdosProblems/Erdos825.lean#L5893.
Is there an absolute constant \(C > 0\) such that every integer \(n\) with \(\sigma(n) > Cn\) is the distinct sum of proper divisors of \(n\)?
This has been solved in the affirmative by Larsen - in fact, for any \(\epsilon>0\) there exists \(L\) such that if \(n\) has only prime divisors \(>L\) and \(\sigma(n)>(2+\epsilon)n\) then \(n\) is the distinct sum of proper divisors of \(n\).
theorem erdos_825 :
∃ (C : ℝ) (_ : C > 0),
∀ (n) (_ : σ 1 n > C * n),
∃ s ⊆ n.properDivisors, n = s.sum id
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/825.lean, line 43.
Erdos825.erdos_825.variants.necessary_cond
Proved here.
Show that if the constant \(C > 0\) is such that every integer \(n\) with \(\sigma(n) > Cn\) is the distinct sum of proper divisors of \(n\), then we must have \(C > 2\).
theorem erdos_825.variants.necessary_cond (C : ℝ) (_hC : 0 < C)
(h : ∀ (n : ℕ) (_ : σ 1 n > C * n),
∃ s ⊆ n.properDivisors, n = s.sum id) :
2 < C
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/825.lean, line 55.
Sources
TheoremErdős Problem 826#
Reference: erdosproblems.com/826
Quoted from FormalConjectures/ErdosProblems/826.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/826.
The file states 1 research or textbook statement: 1 open.
Erdos826.erdos_826
Open: stated without proof.
Are there infinitely many \(n\) such that, for all \(k\geq 1\)
\[ \tau(n + k) \ll k? \]
theorem erdos_826 :
∃ C > (0 : ℝ), { n | ∀ k ≥ 1, σ 0 (n + k) ≤ C * k }.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/826.lean, line 39.
Sources
TheoremErdős Problem 827#
References: - erdosproblems.com/827 - [Er75h] Erdős, P., Some problems on elementary geometry. Austral. Math. Soc. Gaz. 2 (1975), 2-3. - [Er78c] Erdős, P., Some more problems on elementary geometry. Austral. Math. Soc. Gaz. 5 (1978), 52-54. - [MaRo15] Martínez, L. and Roldán-Pensado, E., Points defining triangles with distinct circumradii. Acta Math. Hungar. 145 (2015), 136-141. arXiv:1402.6276
Quoted from FormalConjectures/ErdosProblems/827.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/827.
The file states 4 research or textbook statements: 1 open and 3 solved. It also has 1 API statement, counted here but not shown.
Erdos827.erdos_827
Open: stated without proof.
Let \(n_k\) be minimal such that if \(n_k\) points in \(\mathbb{R}^2\) are in general position then there exists a subset of \(k\) points such that all \(\binom{k}{3}\) triples determine circles of different radii.
Determine \(n_k\).
General position means that no three points are collinear and no four are concyclic, as in [Er75h] (quoted in [MaRo15]).
theorem erdos_827 : n = erdos_827.answer
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/827.lean, line 81.
Erdos827.erdos_827.variants.martinez_roldan_pensado
Solved: stated here without proof.
In [Er78c] Erdős gave an argument for \(n_k \leq k+2\binom{k-1}{2}\binom{k-1}{3}\), but this argument is incorrect, as explained by Martínez and Roldán-Pensado [MaRo15], who give a corrected argument that proves \(n_k\ll k^9\).
[MaRo15, Theorem 1.1] assumes only that no four points lie on a line or a circle. That class contains the sets in general position, so the bound holds for \(n_k\) as defined here.
theorem erdos_827.variants.martinez_roldan_pensado :
(fun k : ℕ ↦ (n k : ℝ)) =O[atTop] fun k : ℕ ↦ (k : ℝ) ^ 9
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/827.lean, line 93.
Erdos827.erdos_827.variants.n_four_le
Solved: stated here without proof.
Martínez and Roldán-Pensado [MaRo15, Theorem 1.2] show that \(n_4 \leq 9\).
theorem erdos_827.variants.n_four_le : n 4 ≤ 9
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/827.lean, line 101.
Erdos827.erdos_827.variants.n_five_le
Solved: stated here without proof.
Martínez and Roldán-Pensado [MaRo15, Theorem 1.2] show that \(n_5 \leq 37\).
theorem erdos_827.variants.n_five_le : n 5 ≤ 37
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/827.lean, line 108.
Sources
TheoremErdős Problem 828#
Reference: erdosproblems.com/828
Quoted from FormalConjectures/ErdosProblems/828.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/828.
The file states 3 research or textbook statements: 2 open and 1 textbook result.
Erdos828.erdos_828
Open: stated without proof.
Is it true that, for any \(a \in \mathbb{Z}\), there are infinitely many \(n\) such that
\[\phi(n) | n + a\]?
theorem erdos_828 : ∀ a : ℤ, Set.Infinite {n : ℕ | ↑(φ n) ∣ n + a}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/828.lean, line 37.
Erdos828.erdos_828.variants.lehmer_conjecture
Open: stated without proof.
When \(n > 1\), Lehmer conjectured that \(\phi(n) | n - 1\) if and only if \(n\) is prime.
theorem erdos_828.variants.lehmer_conjecture : ∀ n > 1, φ n ∣ n - 1 ↔ Prime n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/828.lean, line 44.
Erdos828.erdos_828.variants.phi_dvd_self_iff_pow2_pow3
Textbook result, stated without proof. A Lean proof is at https://github.com/XC0R/formal-conjectures/blob/d252395a9c80fc8eca30d9e5feb6e3b0bc7fc612/FormalConjectures/ErdosProblems/828.lean#L49.
It is an easy exercise to show that \(\phi(n) | n\) if and only if \(n = 0, 1\) or \(n = 2^a 3^b\) for some \(a > 0\).
theorem erdos_828.variants.phi_dvd_self_iff_pow2_pow3 {n : ℕ} :
φ n ∣ n ↔ n ≤ 1 ∨ ∃ᵉ (a > 0) (b), n = 2 ^ a * 3 ^ b
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/828.lean, line 53.
Sources
TheoremErdős Problem 829#
References: - erdosproblems.com/829 - [Er83] Erdős, P. and Dudley, U., Some remarks and problems in number theory related to the work of Euler. Math. Mag. (1983), 292-298.
Quoted from FormalConjectures/ErdosProblems/829.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/829.
The file states 4 research or textbook statements: 1 open and 3 solved. It also has 4 test statements and 1 API statement, counted here but not shown.
Erdos829.erdos_829
Open: stated without proof.
Erdős Problem 829 (open). Let \(A \subseteq \mathbb{N}\) be the set of perfect cubes. Is it true that \((1_A \ast 1_A)(n) \ll (\log n)^{O(1)}\)? That is, does there exist a natural number \(C\) such that the number of representations of \(n\) as a sum of two cubes is \(O((\log n)^C)\) as \(n \to \infty\)?
theorem erdos_829 :
∃ C : ℕ, (fun n : ℕ => (sumRep cubes n : ℝ)) =O[atTop]
(fun n : ℕ => (Real.log n) ^ C)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/829.lean, line 57.
Erdos829.variants.mordell
Solved: stated here without proof.
Mordell proved \(\limsup_{n \to \infty} (1_A \ast 1_A)(n) = \infty\), where \(A\) is the set of perfect cubes. Equivalently, the number of representations of \(n\) as a sum of two cubes is unbounded.
theorem mordell : limsup (fun n : ℕ => (sumRep cubes n : ℕ∞)) atTop = (⊤ : ℕ∞)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/829.lean, line 95.
Erdos829.variants.mahler
Solved: stated here without proof.
Mahler proved \((1_A \ast 1_A)(n) \gg (\log n)^{1/4}\) for infinitely many \(n\), where \(A\) is the set of perfect cubes.
[Ma35b] Mahler, K., On the lattice points on curves of genus 1. Proc. London Math. Soc. (2) (1935), 431-466.
theorem mahler : ∃ C > (0 : ℝ),
∃ᶠ (n : ℕ) in atTop, C * (Real.log n) ^ ((1 : ℝ) / 4) ≤ (sumRep cubes n : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/829.lean, line 106.
Erdos829.variants.stewart
Solved: stated here without proof.
Stewart improved Mahler's lower bound to \((1_A \ast 1_A)(n) \gg (\log n)^{11/13}\) for infinitely many \(n\), where \(A\) is the set of perfect cubes.
[St08] Stewart, C. L., Cubic Thue equations with many solutions. Int. Math. Res. Not. IMRN (2008), Art. ID rnn040, 11.
theorem stewart : ∃ C > (0 : ℝ),
∃ᶠ (n : ℕ) in atTop, C * (Real.log n) ^ ((11 : ℝ) / 13) ≤ (sumRep cubes n : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/829.lean, line 118.
Sources
TheoremErdős Problem 830#
References: - erdosproblems.com/830 - [Er55b] Erdős, P., On amicable numbers. Publ. Math. Debrecen (1955), 108-111. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437. - [Po15] Pomerance, Carl, On amicable numbers. (2015), 321-327. - [Po81] Pomerance, Carl, On the distribution of amicable numbers. II. J. Reine Angew. Math. (1981), 183-188.
Quoted from FormalConjectures/ErdosProblems/830.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/830.
The file states 5 research or textbook statements: 2 open and 3 solved.
Erdos830.erdos_830.parts.i
Open: stated without proof.
Erdos Problem 830, Part 1 We say that \(a,b\in \mathbb{N}\) are an amicable pair if \(\sigma(a)=\sigma(b)=a+b\). Are there infinitely many amicable pairs?
theorem erdos_830.parts.i : {(a, b) | IsAmicable a b}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/830.lean, line 51.
Erdos830.erdos_830.parts.ii
Open: stated without proof.
Erdos Problem 830, Part 2 We say that \(a,b\in \mathbb{N}\) are an amicable pair if \(\sigma(a)=\sigma(b)=a+b\). If \(A(x)\) counts the number of amicable \(1\leq a\leq b\leq x\) then is it true that
\[A(x) > x^{1-o(1)}?\]
theorem erdos_830.parts.ii : ∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧ ∀ᶠ x in atTop,
x ^ (1 - o x) < A x
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/830.lean, line 60.
Erdos830.erdos_830.variants.erdos
Solved: stated here without proof.
We say that \(a,b\in \mathbb{N}\) are an amicable pair if \(\sigma(a)=\sigma(b)=a+b\). If \(A(x)\) counts the number of amicable \(1\leq a\leq b\leq x\) then one can show that \(A(x) = o(x)\).
theorem erdos_830.variants.erdos : A =o[atTop] id
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/830.lean, line 69.
Erdos830.erdos_830.variants.pomerance
Solved: stated here without proof.
We say that \(a,b\in \mathbb{N}\) are an amicable pair if \(\sigma(a)=\sigma(b)=a+b\). If \(A(x)\) counts the number of amicable \(1\leq a\leq b\leq x\) then one can show that \(A(x) \leq x \exp(-(\log x)^{1/3})\).
theorem erdos_830.variants.pomerance : ∀ᶠ x in atTop, A x ≤ x * rexp (- Real.nthRoot 3 x.log)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/830.lean, line 78.
Erdos830.erdos_830.variants.pomerance_stronger
Solved: stated here without proof.
We say that \(a,b\in \mathbb{N}\) are an amicable pair if \(\sigma(a)=\sigma(b)=a+b\). If \(A(x)\) counts the number of amicable \(1\leq a\leq b\leq x\) then one can show that \(A(x) \leq x \exp(-(\tfrac{1}{2}+o(1))(\log x\log\log\log x)^{1/2})\). (erdosproblems.com has \(\log\log x\); [Po15, Theorem 1.1] has \(\log\log\log x\).)
theorem erdos_830.variants.pomerance_stronger :
∃ o : ℝ → ℝ, o =o[atTop] (1 : ℝ → ℝ) ∧
∀ᶠ x in atTop, A x ≤ x * rexp (- (1/ 2 + o x) * √(x.log * x.log.log.log))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/830.lean, line 88.
Sources
TheoremErdős Problem 831#
References: - erdosproblems.com/831 - [Er75h] Erdős, P., Some problems on elementary geometry. Austral. Math. Soc. Gaz. (1975), 2-3. PDF - [Er92e] Erdős, Pál, Some Unsolved problems in Geometry, Number Theory and Combinatorics. Eureka (1992), 44-48.
Quoted from FormalConjectures/ErdosProblems/831.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/831.
The file states 2 research or textbook statements: 1 open and 1 solved. It also has 1 API statement, counted here but not shown.
Erdos831.erdos_831
Open: stated without proof.
Let \(h(n)\) be maximal such that in any \(n\) points in \(\mathbb{R}^2\) (with no three on a line and no four on a circle) there are at least \(h(n)\) many circles of different radii passing through three points. Estimate \(h(n)\).
Erdős asks this in [Er75h, pp. 2-3] (see also [Er92e]); see also Problems 104 and 506. We read "estimate" as the order of magnitude
=Θ. [Er75h] also asks how \(h(n)\) changes if one only assumes that the points are not all on a circle; this is not formalised.
theorem erdos_831 :
(fun n : ℕ ↦ (h n : ℝ)) =Θ[atTop] erdos_831.answer
Category research open; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/831.lean, line 80.
Erdos831.erdos_831.variants.szekeres
Solved: stated here without proof.
Erdős [Er75h, p. 2] attributes to E. Szekeres the observation that for three points \(x_1,x_2,x_3\) of the plane, not on a line, there is a unique point \(x_4\) such that \(x_1,x_2,x_3,x_4\) are not on a circle and the four circles determined by the four triples of these points have the same radius; one can take \(x_4\) to be the orthocentre of the triangle \(x_1x_2x_3\).
Read literally this fails for a right-angled triangle, whose orthocentre is a vertex, so we assume that the triangle has no right angle. We also require the four points to be in general position, so that the four circles exist.
theorem erdos_831.variants.szekeres (x₁ x₂ x₃ : ℝ²)
(hcol : ¬ Collinear ℝ ({x₁, x₂, x₃} : Set ℝ²)) (hright : ¬ IsRightAngled x₁ x₂ x₃) :
∃! x₄ : ℝ², x₄ ∉ ({x₁, x₂, x₃} : Set ℝ²) ∧
InGeneralPosition ({x₁, x₂, x₃, x₄} : Set ℝ²) ∧
(circleRadii ({x₁, x₂, x₃, x₄} : Set ℝ²)).ncard = 1
Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/831.lean, line 96.
Sources
TheoremErdős Problem 832#
References: - erdosproblems.com/832 - [AkSh16] Akolzin, Ilia and Shabanov, Dmitry, Colorings of hypergraphs with large number of colors. Discrete Math. (2016), 3020--3031. - [Al85] Alon, Noga, Hypergraphs with high chromatic number. Graphs Combin. (1985), 387--389. - [ChPe20] Cherkashin, Danila and Petrov, Fedor, Regular behavior of the maximal hypergraph chromatic number. SIAM J. Discrete Math. (2020), 1326--1333.
Quoted from FormalConjectures/ErdosProblems/832.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/832.
The file states 1 research or textbook statement: 1 solved.
Erdos832.erdos_832
Solved: stated here without proof.
Let \(r\geq 3\) and \(k\) be sufficiently large in terms of \(r\). Is it true that every \(r\)-uniform hypergraph with chromatic number \(k\) has at least
\[\binom{(r-1)(k-1)+1}{r}\]edges, with equality only for the complete graph on \((r-1)(k-1)+1\) vertices?
This was disproved by Alon [Al85]. The validity of this conjecture for \(r=3\) remains open.
theorem erdos_832 :
¬ ∀ r : ℕ, 3 ≤ r → ∀ᶠ k : ℕ in atTop,
∀ (n : ℕ) (H : Finset (Finset (Fin n))),
H.IsUniform r → H.HasHypergraphChromaticNumber k →
((r - 1) * (k - 1) + 1).choose r ≤ H.card ∧
(H.card = ((r - 1) * (k - 1) + 1).choose r →
∃ S : Finset (Fin n), S.card = (r - 1) * (k - 1) + 1 ∧ H = S.powersetCard r)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/832.lean, line 47.
Sources
TheoremErdős Problem 833#
References: - erdosproblems.com/833 - [ErLo75] Erdős, P. and Lovász, L., Problems and results on {\(3\)}-chromatic hypergraphs and some related questions. (1975), 609--627.
Quoted from FormalConjectures/ErdosProblems/833.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/833.
The file states 1 research or textbook statement: 1 solved.
Erdos833.erdos_833
Solved: stated here without proof.
Does there exist an absolute constant \(c>0\) such that, for all \(r\geq 2\), in any \(r\)-uniform hypergraph with chromatic number \(3\) there is a vertex contained in at least \((1+c)^r\) many edges?
This was solved by Erdős and Lovász [ErLo75], who proved in particular that there is a vertex contained in at least \(\frac{2^{r-1}}{4r}\) many edges.
theorem erdos_833 :
∃ c : ℝ, 0 < c ∧ ∀ r : ℕ, 2 ≤ r →
∀ (n : ℕ) (H : Finset (Finset (Fin n))),
H.IsUniform r → H.HasHypergraphChromaticNumber 3 →
∃ v : Fin n, (1 + c) ^ r ≤ (H.hypergraphDegree v : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/833.lean, line 43.
Sources
TheoremErdős Problem 834#
References: - erdosproblems.com/834 - [Li25] R. Li, On an Erdős-Lovász problem: \(3\)-critical \(3\)-graphs of minimum degree \(7\). arXiv:2512.24850 (2025).
Quoted from FormalConjectures/ErdosProblems/834.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/834.
The file states 2 research or textbook statements: 2 solved.
Erdos834.erdos_834.parts.i
Solved: stated here without proof.
Does there exist a \(3\)-critical \(3\)-uniform hypergraph in which every vertex has degree \(\geq 7\), where criticality means that the transversal number is \(3\) and deleting any edge reduces it to \(2\)?
In the first formulation, the transversal notion of criticality, Li [Li25] proves that a \(3\)-critical \(3\)-uniform hypergraph must have a vertex of degree \(\leq 6\).
theorem erdos_834.parts.i :
¬ ∃ (n : ℕ) (H : Finset (Finset (Fin n))),
H.IsUniform 3 ∧ (H : Set (Finset (Fin n))).HasFiniteTransversal 3 ∧
¬ (H : Set (Finset (Fin n))).HasFiniteTransversal 2 ∧
(∀ e ∈ H, (H.erase e : Set (Finset (Fin n))).HasFiniteTransversal 2) ∧
∀ v : Fin n, 7 ≤ H.hypergraphDegree v
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/834.lean, line 44.
Erdos834.erdos_834.parts.ii
Solved: stated here without proof.
Does there exist a \(3\)-critical \(3\)-uniform hypergraph with minimum degree at least \(7\), where criticality means that deleting any edge or vertex reduces chromatic number \(3\) to \(2\)?
In the second formulation, the chromatic notion of criticality, Li [Li25] provides an explicit \(3\)-critical \(3\)-uniform hypergraph on \(9\) vertices with minimum degree \(7\).
theorem erdos_834.parts.ii :
∃ (n : ℕ) (H : Finset (Finset (Fin n))),
H.IsUniform 3 ∧ H.HasHypergraphChromaticNumber 3 ∧
(∀ e ∈ H, (H.erase e).HypergraphColorable 2) ∧
(∀ v : Fin n, (H.filter (fun e ↦ v ∉ e)).HypergraphColorable 2) ∧
∀ v : Fin n, 7 ≤ H.hypergraphDegree v
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/834.lean, line 60.
Sources
TheoremErdős Problem 835#
References: - erdosproblems.com/835 - MT25
Quoted from FormalConjectures/ErdosProblems/835.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/835.
The file states 11 research or textbook statements: 3 open and 8 solved. It also has 2 test statements, counted here but not shown.
Erdos835.erdos_835
Open: stated without proof.
Does there exist a \(k>2\) such that the \(k\)-sized subsets of {1,...,2k} can be coloured with \(k+1\) colours such that for every \(A\subset \{1,\ldots,2k\}\) with \(\lvert A\rvert=k+1\) all \(k+1\) colours appear among the \(k\)-sized subsets of \(A\)?
theorem erdos_835 : ∃ k > 2, Property k
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/835.lean, line 52.
Erdos835.erdos_835.variants.johnson
Open: stated without proof.
Alternative statement of Erdős Problem 835 using the chromatic number of the Johnson graph. This is equivalent to asking whether there exists \(k > 2\) such that the chromatic number of the Johnson graph \(J(2k, k)\) is \(k+1\).
theorem erdos_835.variants.johnson : ∃ l,
-- making sure k > 2
letI k := l + 3
J(2 * k, k).chromaticNumber = k + 1
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/835.lean, line 67.
Erdos835.johnsonGraph_2k_k_chromaticNumber_known_cases
Solved: stated here without proof.
It is known that for \(3 \leq k \leq 8\), the chromatic number of \(J(2k, k)\) is greater than \(k+1\), see Johnson graphs.
theorem johnsonGraph_2k_k_chromaticNumber_known_cases (k : ℕ) (hk : 3 ≤ k) (hk' : k ≤ 8) :
J(2 * k, k).chromaticNumber > k + 1
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/835.lean, line 78.
Erdos835.johnsonGraph_18_9_chromaticNumber
Solved: stated here without proof.
The smallest case not on this page is \(k=9\): But that one can be solved as well: The chromatic number of \(J(18, 9)\) is at least \(11\).
theorem johnsonGraph_18_9_chromaticNumber : J(18, 9).chromaticNumber > 9 + 1
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/835.lean, line 88.
Erdos835.indepNum_johnson_le_johnsonBound
Solved: stated here without proof.
Johnson's bound for the independence number of the Johnson graph.
lemma indepNum_johnson_le_johnsonBound : α(J(n, k)) ≤ johnsonBound n 4 k
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/835.lean, line 102.
Erdos835.div_johnsonBound_le_chromaticNum_johnson
Proved here.
Johnson's bound for the chromatic number of the Johnson graph.
lemma div_johnsonBound_le_chromaticNum_johnson :
⌈(n.choose k / johnsonBound n 4 k : ℚ≥0)⌉₊ ≤ χ(J(n, k))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/835.lean, line 106.
Erdos835.chromaticNumber_johnson_2k_k_lower_bound
Solved: stated here without proof.
It is known that for \(3 \leq k \leq 8\), the chromatic number of \(J(2k, k)\) is greater than \(k+1\), see Johnson graphs.
theorem chromaticNumber_johnson_2k_k_lower_bound (hk : 3 ≤ k) (hk' : k ≤ 8) :
k + 1 < J(2 * k, k).chromaticNumber
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/835.lean, line 117.
Erdos835.chromaticNumber_johnson_2k_k_lower_bound_odd
Proved here.
It is also known that for \(3 \leq k \leq 203\) odd, the chromatic number of \(J(2k, k)\) is greater than \(k+1\), see Johnson graphs.
theorem chromaticNumber_johnson_2k_k_lower_bound_odd (hk : 3 ≤ k) (hk' : k ≤ 300) (hk_odd : Odd k) :
k + 1 < J(2 * k, k).chromaticNumber
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/835.lean, line 124.
Erdos835.johnson_chromaticNumber_odd
Solved: stated here without proof.
It can be seen that the chromatic number of \(J(2k,k)\) is \(>k+1\) for all odd \(k>2\).
theorem johnson_chromaticNumber_odd (k : ℕ) (hk : 2 < k) (h : Odd k) :
k + 1 < J(2 * k, k).chromaticNumber
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/835.lean, line 133.
Erdos835.johnson_chromaticNumber_composite
Solved: stated here without proof.
Ma and Tang have proved that the chromatic number of \(J(2k,k)\) is \(>k+1\) for all \(k>2\) not of the form \(p-1\) for prime \(p\).
theorem johnson_chromaticNumber_composite (k : ℕ) (hk : 2 < k) (h : (k + 1).Composite) :
k + 1 < J(2 * k, k).chromaticNumber
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/835.lean, line 142.
Erdos835.johnson_chromaticNumber
Open: stated without proof.
Is the chromatic number of
J(2 * k, k)always at leastk + 2?
theorem johnson_chromaticNumber :
∀ k ≥ 3, k + 2 ≤ J(2 * k, k).chromaticNumber
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/835.lean, line 162.
Sources
TheoremErdős Problem 836#
References: - erdosproblems.com/836 - [ErLo75] Erdős, P. and Lovász, L., Problems and results on {\(3\)}-chromatic hypergraphs and some related questions. (1975), 609--627. - [Pr26] Price, L., A Linear Intersection Bound. (2026).
Quoted from FormalConjectures/ErdosProblems/836.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/836.
The file states 2 research or textbook statements: 2 solved.
Erdos836.erdos_836.parts.i
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/ad12db51383ed41ec8b6b54e0ffabfa828773d38/erdos-836/Solution.lean#L33.
Let \(r\geq 2\) and let \(G\) be an intersecting \(r\)-uniform hypergraph with chromatic number \(3\). Must \(G\) contain \(O(r^2)\) many vertices? Vertices are counted in the union of the edges, so isolated vertices are excluded.
Alon has provided a counterexample to the first question: this hypergraph is intersecting, its chromatic number is \(3\), and it has \(\asymp 4^r/\sqrt{r}\) many vertices.
theorem erdos_836.parts.i :
¬ ∃ C : ℝ, 0 < C ∧ ∀ r : ℕ, 2 ≤ r →
∀ (n : ℕ) (H : Finset (Finset (Fin n))),
H.IsUniform r → H.HasHypergraphChromaticNumber 3 → (H : Set (Finset (Fin n))).Intersecting →
((H.biUnion id).card : ℝ) ≤ C * (r : ℝ) ^ 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/836.lean, line 47.
Erdos836.erdos_836.parts.ii
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/ad12db51383ed41ec8b6b54e0ffabfa828773d38/erdos-836/Solution.lean#L41.
In an intersecting \(r\)-uniform hypergraph with chromatic number \(3\), must there be two distinct edges which meet in \(\gg r\) many vertices?
theorem erdos_836.parts.ii :
∃ c : ℝ, 0 < c ∧ ∀ r : ℕ, 2 ≤ r →
∀ (n : ℕ) (H : Finset (Finset (Fin n))),
H.IsUniform r → H.HasHypergraphChromaticNumber 3 → (H : Set (Finset (Fin n))).Intersecting →
∃ e ∈ H, ∃ f ∈ H, e ≠ f ∧ c * r ≤ ((e ∩ f).card : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/836.lean, line 61.
Sources
TheoremErdős Problem 837#
References: - erdosproblems.com/837
Quoted from FormalConjectures/ErdosProblems/837.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/837.
The file states 1 research or textbook statement: 1 open.
Erdos837.erdos_837
Open: stated without proof.
Let \(k\geq 2\) and \(A_k\subseteq [0,1]\) be the set of \(\alpha\) such that there exists some \(\beta(\alpha)>\alpha\) with the property that, if \(G_1,G_2,\ldots\) is a sequence of \(k\)-uniform hypergraphs with
\[\liminf \frac{e(G_n)}{\binom{\lvert G_n\rvert}{k}} >\alpha\]then there exist subgraphs \(H_n\subseteq G_n\) such that \(\lvert H_n\rvert \to \infty\) and
\[\liminf \frac{e(H_n)}{\binom{\lvert H_n\rvert}{k}} >\beta,\]and further that this property does not necessarily hold if \(>\alpha\) is replaced by \(\geq \alpha\). What is \(A_3\)?
theorem erdos_837 :
{α : ℝ | α ∈ Set.Icc 0 1 ∧ ∃ β : ℝ, α < β ∧
Hypergraph.HasDensityJump 3 α β true ∧ ¬ Hypergraph.HasDensityJump 3 α β false}
= erdos_837.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/837.lean, line 46.
Sources
TheoremErdős Problem 838#
References: - erdosproblems.com/838 - [Er78c] Erdős, P., Some more problems on elementary geometry. Austral. Math. Soc. Gaz. 5 (1978), 52-54. PDF
Quoted from FormalConjectures/ErdosProblems/838.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/838.
The file states 3 research or textbook statements: 2 open and 1 solved. It also has 1 API statement, counted here but not shown.
Erdos838.erdos_838.parts.i
Open: stated without proof.
Let \(f(n)\) be maximal such that any \(n\) points in \(\mathbb{R}^2\), with no three on a line, determine at least \(f(n)\) different convex subsets. Estimate \(f(n)\) - in particular, does there exist a constant \(c\) such that
\[\lim \frac{\log f(n)}{(\log n)^2}=c?\]A question of Erdős and Hammer [Er78c, pp. 52-53]. This is the first part. We read "estimate" as asking for an asymptotic formula for \(\log f(n)\).
theorem erdos_838.parts.i :
(fun n : ℕ ↦ Real.log (f n)) ~[atTop] erdos_838.parts.i.answer
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/838.lean, line 68.
Erdos838.erdos_838.parts.ii
Open: stated without proof.
Let \(f(n)\) be maximal such that any \(n\) points in \(\mathbb{R}^2\), with no three on a line, determine at least \(f(n)\) different convex subsets. Estimate \(f(n)\) - in particular, does there exist a constant \(c\) such that
\[\lim \frac{\log f(n)}{(\log n)^2}=c?\]A question of Erdős and Hammer [Er78c, p. 53]. This is the second part.
theorem erdos_838.parts.ii :
∃ c : ℝ, Tendsto (fun n : ℕ ↦ Real.log (f n) / Real.log n ^ 2) atTop (nhds c)
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/838.lean, line 81.
Erdos838.erdos_838.variants.erdos_bounds
Solved: stated here without proof.
Erdős proved in [Er78c] that there exist constants \(c_1,c_2>0\) such that
\[n^{c_1\log n}\lt f(n)< n^{c_2\log n}.\]Here \(\log\) is the natural logarithm (another base only changes the constants), and \(n\geq 2\).
theorem erdos_838.variants.erdos_bounds :
∃ c₁ c₂ : ℝ, 0 < c₁ ∧ 0 < c₂ ∧ ∀ n : ℕ, 2 ≤ n →
(n : ℝ) ^ (c₁ * Real.log n) < f n ∧ (f n : ℝ) < (n : ℝ) ^ (c₂ * Real.log n)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/838.lean, line 91.
Sources
TheoremErdős Problem 839#
References: - erdosproblems.com/839 - [Er78f] Erdős, P., Problems in number theory and combinatorics, Proc. Sixth Manitoba Conf. on Numerical Math. (1978), 35-58. - [Er92c] Erdős, P., Some of my favourite unsolved problems, J. Combin. Theory Ser. A (1992).
See also Erdős Problem 359 and Erdős Problem 867.
Quoted from FormalConjectures/ErdosProblems/839.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/839.
The file states 2 research or textbook statements: 2 open.
Erdos839.erdos_839.parts.i
Open: stated without proof.
Erdős Problem 839 (Part 1) [Er78f][Er92c]:
Let \(1 \leq a_1 < a_2 < \cdots\) be a strictly increasing sequence of positive integers such that no \(a_i\) is the sum of consecutive \(a_j\) for \(j < i\). Is it true that \(\limsup a_n / n = \infty\)?
theorem erdos_839.parts.i :
∀ (a : ℕ → ℕ), (∀ n, 1 ≤ a n) → StrictMono a → SumOfConsecutiveFree a →
atTop.limsup (fun n : ℕ => (a n : ℝ≥0∞) / n) = ⊤
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/839.lean, line 55.
Erdos839.erdos_839.parts.ii
Open: stated without proof.
Erdős Problem 839 (Part 2, stronger) [Er78f][Er92c]:
Let \(1 \leq a_1 < a_2 < \cdots\) be a strictly increasing sequence of positive integers such that no \(a_i\) is the sum of consecutive \(a_j\) for \(j < i\). Is it true that \(\lim_{x \to \infty} \frac{1}{\log x} \sum_{a_n < x} \frac{1}{a_n} = 0\)?
This is equivalent to asking whether the range \(\{a_1,a_2,\ldots\}\) has logarithmic density zero (see
Set.HasLogDensity).
theorem erdos_839.parts.ii :
∀ (a : ℕ → ℕ), (∀ n, 1 ≤ a n) → StrictMono a → SumOfConsecutiveFree a →
Set.HasLogDensity (Set.range a) 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/839.lean, line 71.
Sources
TheoremErdős Problem 840#
References: - erdosproblems.com/840 - [Er81h] Erdős, P., Some problems and results on additive and multiplicative number theory. Analytic number theory (Philadelphia, Pa., 1980), Lecture Notes in Math. 899 (1981), 171-182. PDF - [ErFr91] Erdős, P. and Freud, R., On sums of a Sidon-sequence. J. Number Theory 38 (1991), 196-205. - [Pi06] Pikhurko, O., Dense edge-magic graphs and thin additive bases. Discrete Math. 306 (2006), 2097-2107.
Quoted from FormalConjectures/ErdosProblems/840.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/840.
The file states 4 research or textbook statements: 1 open and 3 solved. It also has 1 test statement, counted here but not shown.
Erdos840.erdos_840
Open: stated without proof.
Let \(f(N)\) be the size of the largest quasi-Sidon subset \(A\subset\{1,\ldots,N\}\), where we say that \(A\) is quasi-Sidon if
\[\lvert A+A\rvert=(1+o(1))\binom{\lvert A\rvert}{2}.\]How does \(f(N)\) grow?
Following [Er81h, p. 175], we ask for the largest \(c\) such that there are quasi-Sidon sets \(A \subseteq \{1, \ldots, N\}\) with \(\lvert A\rvert = (1+o(1))cN^{1/2}\).
theorem erdos_840 : IsLUB {c : ℝ | IsQuasiSidonConstant c} erdos_840.answer
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/840.lean, line 69.
Erdos840.erdos_840.variants.erdos_freud_lower
Solved: stated here without proof.
Erdős and Freud [ErFr91] proved
\[\left(\frac{2}{\sqrt{3}}+o(1)\right)N^{1/2} \leq f(N) \leq \left(2+o(1)\right)N^{1/2}.\](Although both bounds were already given by Erdős in [Er81h].)
This is the lower bound. The lower bound is taking a genuine Sidon set \(B\subset [1,N/3]\) of size \(\sim N^{1/2}/\sqrt{3}\) and taking the union with \(\{N-b : b\in B\}\).
theorem erdos_840.variants.erdos_freud_lower : IsQuasiSidonConstant (2 / Real.sqrt 3)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/840.lean, line 81.
Erdos840.erdos_840.variants.erdos_freud_upper
Proved here.
Erdős and Freud [ErFr91] proved
\[\left(\frac{2}{\sqrt{3}}+o(1)\right)N^{1/2} \leq f(N) \leq \left(2+o(1)\right)N^{1/2}.\](Although both bounds were already given by Erdős in [Er81h].)
This is the upper bound.
theorem erdos_840.variants.erdos_freud_upper (c : ℝ) (hc : IsQuasiSidonConstant c) : c ≤ 2
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/840.lean, line 92.
Erdos840.erdos_840.variants.pikhurko
Solved: stated here without proof.
The upper bound was improved by Pikhurko [Pi06] to
\[f(N) \leq \left(\left(\frac{1}{4}+\frac{1}{(\pi+2)^2}\right)^{-1/2}+o(1)\right)N^{1/2}\](the constant here is \(=1.863\cdots\)).
theorem erdos_840.variants.pikhurko (c : ℝ) (hc : IsQuasiSidonConstant c) :
c ≤ (1 / 4 + 1 / (Real.pi + 2) ^ 2) ^ (-(1 : ℝ) / 2)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/840.lean, line 141.
Sources
TheoremErdős Problem 841#
References: - erdosproblems.com/841 - [ErSe92] Erdős, Paul and Selfridge, J. L., Problems and Solutions: Solutions: 6655. Amer. Math. Monthly (1992), 791--794. - [BPZ24] Bui, Hung M. and Pratt, Kyle and Zaharescu, Alexandru, A problem of Erdős-Graham-Granville-Selfridge on integral points on hyperelliptic curves. Math. Proc. Cambridge Philos. Soc. (2024), 309--323. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.
Quoted from FormalConjectures/ErdosProblems/841.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/841.
The file states 5 research or textbook statements: 5 solved.
Erdos841.erdos_841
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos841/Core.lean#L16920.
Let \(t_n\) be minimal such that \(\{n+1,\ldots,n+t_n\}\) contains a subset whose product with \(n\) is a square number (and let \(t_n=0\) if \(n\) is itself square). Estimate \(t_n\).
A problem of Erdős, Graham, and Selfridge. For example, \(t_6=6\) since \(6\cdot 8\cdot 12=24^2\). It is trivial that \(t_n\geq P(n)\), where \(P(n)\) is the largest prime divisor of \(n\).
Bui, Pratt, and Zaharescu [BPZ24] proved that the distribution of \(t_n\) continues to follow \(P(n)\), in that for any fixed \(c\in (0,1]\)
\[\lim_{x\to \infty}\frac{\lvert \{ n\leq x : t_n\leq n^c\}\rvert}{x} = \lim_{x\to \infty}\frac{\lvert \{ n\leq x : P(n)\leq n^c\}\rvert}{x}.\]The statement below is that the difference of the two counting functions is \(o(x)\).
This was formalized in Lean by Codex.
theorem erdos_841 (c : ℝ) (hc : c ∈ Set.Ioc 0 1) :
Tendsto (fun x : ℕ ↦
((((Finset.Icc 1 x).filter fun n : ℕ ↦ (t n : ℝ) ≤ (n : ℝ) ^ c).card : ℝ) -
((Finset.Icc 1 x).filter fun n : ℕ ↦ (n.maxPrimeFac : ℝ) ≤ (n : ℝ) ^ c).card) / x)
atTop (𝓝 0)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/841.lean, line 62.
Erdos841.erdos_841.variants.selfridge_large_prime
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos841/LowerBound.lean#L3183.
Selfridge proved that \(t_n=P(n)\) if \(P(n)>\sqrt{2n}+1\).
This was formalized in Lean by Codex.
theorem erdos_841.variants.selfridge_large_prime (n : ℕ) (hn : 1 < n)
(h : √(2 * n) + 1 < (n.maxPrimeFac : ℝ)) : t n = n.maxPrimeFac
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/841.lean, line 76.
Erdos841.erdos_841.variants.selfridge_sqrt
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos841/Core.lean#L1373.
Selfridge proved that \(t_n \ll n^{1/2}\) if \(P(n)\leq\sqrt{2n}+1\).
This was formalized in Lean by Codex.
theorem erdos_841.variants.selfridge_sqrt :
∃ C : ℝ, ∀ n : ℕ, (n.maxPrimeFac : ℝ) ≤ √(2 * n) + 1 → (t n : ℝ) ≤ C * √n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/841.lean, line 87.
Erdos841.erdos_841.variants.many_small_values
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos841/Core.lean#L16105.
Bui, Pratt, and Zaharescu [BPZ24] proved that for at least \(x^{1-o(1)}\) many \(n\leq x\) we have
\[t_n \leq \exp(O(\sqrt{\log n\log\log n})).\]This was formalized in Lean by Codex.
theorem erdos_841.variants.many_small_values : ∃ K : ℝ,
Tendsto (fun x : ℕ ↦
log (((Finset.Icc 1 x).filter fun n ↦
(t n : ℝ) ≤ exp (K * √(log n * log (log n)))).card : ℝ) / log x) atTop (𝓝 1)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/841.lean, line 100.
Erdos841.erdos_841.variants.lower_bound
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos841/LowerBound.lean#L3166.
Bui, Pratt, and Zaharescu [BPZ24] proved that for all non-square \(n\)
\[t_n \gg (\log\log n)^{6/5}(\log\log\log n)^{-1/5}.\]This was formalized in Lean by Codex.
theorem erdos_841.variants.lower_bound : ∃ C : ℝ, 0 < C ∧
∀ᶠ n : ℕ in atTop, ¬ IsSquare n →
C * (log (log n) ^ ((6 : ℝ) / 5) * log (log (log n)) ^ (-(1 : ℝ) / 5)) ≤ t n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/841.lean, line 114.
Sources
TheoremErdős Problem 842#
References: - erdosproblems.com/842 - [Er92b] Erdős, Paul, Some of my favourite problems in various branches of combinatorics. Matematiche (Catania) (1992), 231-240. - [FlSt92] Fleischner, Herbert and Stiebitz, Michael, A solution to a colouring problem of P. Erdős. Discrete Math. (1992), 39--48.
Quoted from FormalConjectures/ErdosProblems/842.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/842.
The file states 1 research or textbook statement: 1 solved.
Erdos842.erdos_842
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos842.lean#L46.
Let \(G\) be a graph on \(3n\) vertices formed by taking \(n\) vertex disjoint triangles and adding a Hamiltonian cycle (with all new edges) between these vertices. Does \(G\) have chromatic number at most \(3\)?
The answer is yes, proved by Fleischner and Stiebitz [FlSt92].
theorem erdos_842 :
∀ (V : Type) (G : SimpleGraph V) (n : ℕ), IsTrianglesPlusHamiltonianCycle G n →
G.chromaticNumber ≤ 3
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/842.lean, line 54.
Sources
TheoremErdős Problem 844#
References: - erdosproblems.com/844 - [AMS25] Alexeev, B., Mixon, D. and Sawin, W., The independence and clique cover numbers of the squarefree graph. arXiv:2507.01928 (2025). - [Ch74] Chvátal, V., Intersecting families of edges in hypergraphs having the hereditary property. (1974), 61-66.
Quoted from FormalConjectures/ErdosProblems/844.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/844.
The file states 1 research or textbook statement: 1 solved.
Erdos844.erdos_844
Solved: stated here; a Lean proof is at https://gist.githubusercontent.com/JohnEdwardJennings/e32f2c412b0225091e7519d60741bd2d/raw/7d811ea413e2f7c0c0442749958aaac421eb6807/Erdos844.lean.
Let \(A\subseteq \{1,\ldots,N\}\) be such that, for all \(a,b\in A\), the product \(ab\) is not squarefree.
Is the maximum size of such an \(A\) achieved by taking \(A\) to be the set of even numbers and odd non-squarefree numbers?
A problem of Erdős and Sárközy.
Weisenberg has provided the following positive proof. It is clear that such a maximal \(A\) must contain all non-squarefree numbers. It therefore suffices to find the largest size of a subset of all squarefree numbers in \(\{1,\ldots,N\}\) such that any two have at least one prime factor in common. By the result of Chvátal [Ch74] discussed in [701] this is maximised by the set of all even squarefree numbers.
An alternative proof was independently found by Alexeev, Mixon, and Sawin [AMS25].
This was formalized in Lean by Jennings using Aristotle.
theorem erdos_844 : ∀ N : ℕ,
IsGreatest {k : ℕ | ∃ A ⊆ Finset.Icc 1 N,
(∀ a ∈ A, ∀ b ∈ A, ¬ Squarefree (a * b)) ∧ A.card = k}
(evenOrOddNonSquarefree N).card
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/844.lean, line 62.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.