Erdős Problem 926 to Erdős Problem 947
TheoremErdős Problem 926#
References: - erdosproblems.com/926 - [Er69b] Erdős, P., Problems and results in chromatic graph theory. Proof Techniques in Graph Theory (Proc. Second Ann Arbor Graph Theory Conf., Ann Arbor, Mich., 1968) (1969), 27-35. - [Er71] Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109. - [Er74c] Erdős, Paul, Extremal problems on graphs and hypergraphs. (1974), 75-84. - [Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350. - [Fu91] Füredi, Zoltán, On a Turán type problem of Erdős. Combinatorica (1991), 75--79. - [AKS03] Alon, Noga and Krivelevich, Michael and Sudakov, Benny, Turán numbers of bipartite graphs and related Ramsey-type questions. Combin. Probab. Comput. (2003), 477-494.
Quoted from FormalConjectures/ErdosProblems/926.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/926.
The file states 2 research or textbook statements: 2 solved.
Erdos926.erdos_926
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos926.lean#L644.
Let \(k\geq 4\). Is it true that
\[\mathrm{ex}(n;H_k) \ll_k n^{3/2},\]where \(H_k\) is the graph on vertices \(x,y_1,\ldots,y_k,z_1,\ldots,z_{\binom{k}{2}}\), where \(x\) is adjacent to all \(y_i\) and each pair of \(y_i,y_j\) is adjacent to a unique \(z_i\).
It is trivial that \(\mathrm{ex}(n;H_k)\gg n^{3/2}\) since \(H_k\) contians a \(C_4\) for \(k\geq 3\). Erdős [Er71] claimed a proof for \(k=3\).
The answer is yes, proved by Füredi [Fu91], who proved that \(\mathrm{ex}(n;H_k) \ll (kn)^{3/2}\). This was improved to \(\mathrm{ex}(n;H_k) \ll kn^{3/2}\) by Alon, Krivelevich, and Sudakov [AKS03].
Since each \(H_k\) is 2-degenerate this is a special case of 146. The extremal number of the graph \(H_k\) with the vertex \(x\) omitted is the subject of 1021.
theorem erdos_926 : ∀ k : ℕ, 4 ≤ k →
(fun n : ℕ => (extremalNumber n (H k) : ℝ)) =O[atTop] fun n : ℕ => (n : ℝ) ^ (3 / 2 : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/926.lean, line 81.
Erdos926.erdos_926.variants.aks
Solved: stated here without proof.
Alon, Krivelevich, and Sudakov [AKS03] proved \(\mathrm{ex}(n;H_k) \ll kn^{3/2}\) with an absolute implied constant.
theorem erdos_926.variants.aks : ∃ C : ℝ, ∀ k : ℕ, 4 ≤ k → ∀ n : ℕ,
(extremalNumber n (H k) : ℝ) ≤ C * k * (n : ℝ) ^ (3 / 2 : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/926.lean, line 88.
Sources
TheoremErdős Problem 927#
References: - erdosproblems.com/927 - [MoMo65] Moon, J. W. and Moser, L., On cliques in graphs. Israel J. Math. (1965), 23-28. - [Er66b] Erdős, P., On cliques in graphs. Israel J. Math. (1966), 233--234. - [Er69b] Erdős, P., Problems and results in chromatic graph theory. Proof Techniques in Graph Theory (Proc. Second Ann Arbor Graph Theory Conf., Ann Arbor, Mich., 1968) (1969), 27-35. - [Er71] Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109. - [Sp71] Spencer, J. H., On cliques in graphs. Israel J. Math. (1971), 419-421.
Quoted from FormalConjectures/ErdosProblems/927.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/927.
The file states 1 research or textbook statement: 1 solved.
Erdos927.erdos_927
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos927.lean#L23.
Let \(g(n)\) be the maximum number of different sizes of cliques that can occur in a graph on \(n\) vertices. Estimate \(g(n)\) - in particular, is it true that
\[g(n) = n - \log_2 n - \log_*(n) + O(1),\]where \(\log_*(n)\) is the number of iterated logarithms such that \(\log \cdots \log n < 1\)?
A quantity first considered by Moon and Moser [MoMo65], who proved \(n - \log_2 n - 2 \log \log n < g(n) \le n - \lfloor \log_2 n \rfloor\). Erdős [Er66b] improved the lower bound to \(n - \log_2 n - \log_*(n) - O(1) < g(n)\) and conjectured this was the correct order of magnitude. This was disproved by Spencer [Sp71], who proved that in fact \(g(n) > n - \log_2 n - O(1)\).
Here \(\log_2 n\) and \(\log_*(n)\) are formalised as
Nat.log 2 nandNat.iteratedLog 2 n(iteratingNat.log 2until the value is at most1); both differ from the quantities in the problem by \(O(1)\), so the statement is unaffected. See alsoerdos_775.variants.spenceranderdos_775.variants.moon_moser.
theorem erdos_927 :
¬ ∃ C : ℕ, ∀ᶠ n : ℕ in atTop,
g n + Nat.log 2 n + Nat.iteratedLog 2 n ≤ n + C ∧
n ≤ g n + Nat.log 2 n + Nat.iteratedLog 2 n + C
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/927.lean, line 68.
Sources
TheoremErdős Problem 929#
References: - erdosproblems.com/929 - [Er76d] Erdős, P., Problems and results on number theoretic properties of consecutive integers and related questions. Proceedings of the Fifth Manitoba Conference on Numerical Mathematics (Univ. Manitoba, Winnipeg, Man., 1975) (1976), 25-44. PDF
Quoted from FormalConjectures/ErdosProblems/929.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/929.
The file states 4 research or textbook statements: 2 open, 1 solved and 1 textbook result. It also has 1 API statement, counted here but not shown.
Erdos929.erdos_929.parts.i
Open: stated without proof.
Let \(k\geq 2\) be large and let \(S(k)\) be the minimal \(x\) such that there is a positive density set of \(n\) where
\[n+1,n+2,\ldots,n+k\]are all divisible by primes \(\leq x\).
Estimate \(S(k)\) - in particular, is it true that \(S(k)\geq k^{1-o(1)}\)?
A problem of Erdős [Er76d, p. 26]. This is the first part. We read "estimate" as \(S(k) = \Theta(\text{answer})\) as \(k \to \infty\).
theorem erdos_929.parts.i : (fun k ↦ (S k : ℝ)) =Θ[atTop] erdos_929.parts.i.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/929.lean, line 74.
Erdos929.erdos_929.parts.ii
Open: stated without proof.
Let \(k\geq 2\) be large and let \(S(k)\) be the minimal \(x\) such that there is a positive density set of \(n\) where
\[n+1,n+2,\ldots,n+k\]are all divisible by primes \(\leq x\).
Estimate \(S(k)\) - in particular, is it true that \(S(k)\geq k^{1-o(1)}\)?
This is the second part. We read \(o(1)\) as an arbitrary \(\varepsilon > 0\) for all large \(k\).
theorem erdos_929.parts.ii :
∀ ε : ℝ, 0 < ε → ∀ᶠ k : ℕ in atTop, (k : ℝ) ^ (1 - ε) ≤ (S k : ℝ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/929.lean, line 88.
Erdos929.erdos_929.variants.rosser
Solved: stated here without proof.
It follows from Rosser's sieve that \(S(k)> k^{1/2-o(1)}\).
Erdős [Er76d, p. 26] states this for the index \(\ell\) with \(p_\ell = S(k)\). Since \(S(k) = p_\ell \geq \ell\), the bound transfers to \(S(k)\). The \(o(1)\) is stated with an arbitrary \(\varepsilon > 0\).
theorem erdos_929.variants.rosser :
∀ ε : ℝ, 0 < ε → ∀ᶠ k : ℕ in atTop, (k : ℝ) ^ ((1 : ℝ) / 2 - ε) ≤ (S k : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/929.lean, line 100.
Erdos929.erdos_929.variants.trivial_upper
Textbook result, stated without proof.
It is trivial that \(S(k)\leq k+1\) since, for example, one can take \(n\equiv 1\pmod{(k+1)!}\).
theorem erdos_929.variants.trivial_upper (k : ℕ) : S k ≤ k + 1
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/929.lean, line 108.
Sources
TheoremErdős Problem 930#
Reference: erdosproblems.com/930
Quoted from FormalConjectures/ErdosProblems/930.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/930.
The file states 3 research or textbook statements: 1 open and 2 solved.
Erdos930.erdos_930
Open: stated without proof.
Is it true that, for every \(r\), there is a \(k\) such that if \(I_1,\ldots,I_r\) are disjoint intervals of consecutive integers, all of length at least \(k\), then
\[ \prod_{1\leq i\leq r}\prod_{m\in I_i}m \]is not a perfect power?
theorem erdos_930 :
∀ r > 0, ∃ k, ∀ I₁ I₂ : Fin r → ℕ,
(∀ i : Fin r, 0 < I₁ i ∧ I₁ i + k ≤ I₂ i + 1) →
(∀ i j : Fin r, i < j → I₂ i < I₁ j) →
¬ IsPower (∏ i : Fin r, ∏ m ∈ Icc (I₁ i) (I₂ i), m)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/930.lean, line 49.
Erdos930.erdos_930.variants.consecutive_strong
Solved: stated here without proof.
Let \(k\), \(l\), \(n\) be integers such that \(k \ge 3\), \(l \ge 2\) and \(n + k \ge p^{(k)}\), where \(p^{(k)}\) is the least prime satisfying \(p^{(k)} \ge k\). Then there is a prime \(p \ge k\) for which \(l\) does not divide the multiplicity of the prime factor \(p\) in \((n + 1) \ldots (n + k)\).
Theorem 2 from [ErSe75].
[ErSe75] Erdős, P. and Selfridge, J. L., The product of consecutive integers is never a power. Illinois J. Math. (1975), 292-301.
theorem erdos_930.variants.consecutive_strong :
∀ k l n, 3 ≤ k → 2 ≤ l → nextPrime k ≤ n + k →
∃ p, k ≤ p ∧ p.Prime ∧
¬ (l ∣ Nat.factorization (∏ m ∈ Icc (n + 1) (n + k), m) p)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/930.lean, line 73.
Erdos930.erdos_930.variants.consecutive_integers
Solved: stated here without proof.
Erdos and Selfridge [ErSe75] proved that the product of consecutive integers is never a power (establishing the case \(r=1\)).
Theorem 1 from [ErSe75].
It is implied from
erdos_930.variants.consecutive_strong.[ErSe75] Erdős, P. and Selfridge, J. L., The product of consecutive integers is never a power. Illinois J. Math. (1975), 292-301.
theorem erdos_930.variants.consecutive_integers :
∀ n k, 0 ≤ n → 2 ≤ k →
¬ IsPower (∏ m ∈ Icc (n + 1) (n + k), m)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/930.lean, line 90.
Sources
TheoremErdős Problem 931#
Reference: erdosproblems.com/931
Quoted from FormalConjectures/ErdosProblems/931.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/931.
The file states 4 research or textbook statements: 3 open and 1 solved.
Erdos931.erdos_931
Open: stated without proof.
Let \(k_1 \geq k_2 \geq 3\). Are there only finitely many \(n_2\geq n_1 + k_1\) such that
\[ \prod_{1\leq i\leq k_1}(n_1 + i)\ \text{and}\ \prod_{1\leq j\leq k_2} (n_2 + j) \]have the same prime factors?
theorem erdos_931 : ∀ᵉ (k₁ : ℕ) (k₂ ≥ 3), k₂ ≤ k₁ →
{ (n₁, n₂) | n₁ + k₁ ≤ n₂ ∧
(∏ i ∈ Finset.Icc 1 k₁, (n₁ + i)).primeFactors =
(∏ j ∈ Finset.Icc 1 k₂, (n₂ + j)).primeFactors }.Finite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/931.lean, line 39.
Erdos931.erdos_931.variants.additional_condition
Open: stated without proof.
Erdős thought perhaps if the two products have the same factors then \(n_2 > 2(n_1 + k_1)\). It is an open question whether this is true when allowing a finite number of counterexamples.
theorem erdos_931.variants.additional_condition : ∀ᵉ (k₁ : ℕ) (k₂ ≥ 3), k₂ ≤ k₁ →
{(n₁, n₂) | n₁ + k₁ ≤ n₂ ∧ n₂ ≤ 2 * (n₁ + k₁) ∧
(∏ i ∈ Finset.Icc 1 k₁, (n₁ + i)).primeFactors =
(∏ j ∈ Finset.Icc 1 k₂, (n₂ + j)).primeFactors}.Finite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/931.lean, line 51.
Erdos931.erdos_931.variants.additional_condition_nonempty
Proved here.
In fact there exist counterexamples, like this one found by AlphaProof.
theorem erdos_931.variants.additional_condition_nonempty : ∃ (k₁ k₂ : ℕ), ∃ (_h₁ : k₂ ≤ k₁), ∃ (_h₂ : 3 ≤ k₂),
{(n₁, n₂) | n₁ + k₁ ≤ n₂ ∧ n₂ ≤ 2 * (n₁ + k₁) ∧
(∏ i ∈ Finset.Icc 1 k₁, (n₁ + i)).primeFactors =
(∏ j ∈ Finset.Icc 1 k₂, (n₂ + j)).primeFactors}.Nonempty
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/931.lean, line 61.
Erdos931.erdos_931.variants.exists_prime
Open: stated without proof.
Erdős was unable to prove that if the two products have the same factors then there must exist a prime between \(n_1\) and \(n_2\).
theorem erdos_931.variants.exists_prime (k₁ k₂ n₁ n₂ : ℕ) (h₁ : k₂ ≤ k₁) (h₂ : 3 ≤ k₂)
(h₃ : n₁ + k₁ ≤ n₂) (h₄ : (∏ i ∈ Finset.Icc 1 k₁, (n₁ + i)).primeFactors =
(∏ j ∈ Finset.Icc 1 k₂, (n₂ + j)).primeFactors) :
∃ (p : ℕ), p.Prime ∧ n₁ ≤ p ∧ p ≤ n₂
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/931.lean, line 75.
Sources
TheoremErdős Problem 932#
Reference: erdosproblems.com/932
Quoted from FormalConjectures/ErdosProblems/932.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/932.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos932.erdos_932
Open: stated without proof.
Let \(p_k\) denote the \(k\)th prime. For infinitely many \(r\) there are at least two integers \(p_r < n < p_{r+1}\) all of whose prime factors are \(< p_{r + 1} - p_r\).
theorem erdos_932 :
{ r : ℕ | 2 ≤ (Finset.Ioo (r.nth Nat.Prime) (r.succ.nth Nat.Prime) |>.filter
(fun m => m.maxPrimeFac < r.succ.nth Nat.Prime - r.nth Nat.Prime)).card }.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/932.lean, line 35.
Erdos932.erdos_932.variants.one_le
Solved: stated here without proof.
Erdős could show that the density of \(r\) such that at least one such \(n\) exists is \(0\).
theorem erdos_932.variants.one_le :
{ r : ℕ | 1 ≤ (Finset.Ioo (r.nth Nat.Prime) (r.succ.nth Nat.Prime) |>.filter
(fun m => m.maxPrimeFac < r.succ.nth Nat.Prime - r.nth Nat.Prime)).card }.HasDensity 0
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/932.lean, line 44.
Sources
TheoremErdős Problem 933#
References: - erdosproblems.com/933 - [Er76d] Erdős, P, Problems and results on number theoretic properties of consecutive integers and related questions. Proceedings of the Fifth Manitoba Conference on Numerical Mathematics (Univ. Manitoba, Winnipeg, Man., 1975) (1976), 25-44.
Quoted from FormalConjectures/ErdosProblems/933.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/933.
The file states 3 research or textbook statements: 1 open and 2 solved.
Erdos933.erdos_933
Open: stated without proof.
If \(n(n+1)=2^k3^lm\), where \((m,6)=1\), then is it true that \(\limsup_{n\to \infty} \frac{2^k3^l}{n\log n}=\infty\)?
theorem erdos_933 :
atTop.limsup (fun n : ℕ ↦
((((2 ^ k n * 3 ^ l n : ℕ) : ℝ) / ((n : ℝ) * Real.log (n : ℝ))) : EReal)) = ⊤
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/933.lean, line 47.
Erdos933.erdos_933.variants.mahler
Solved: stated here without proof.
Mahler proved (a more general result that implies in particular) that \(2^k3^l\lt n^{1+o(1)}\).
theorem erdos_933.variants.mahler :
∃ c : ℕ → ℝ, (c =o[atTop] (1 : ℕ → ℝ)) ∧
∀ᶠ n in atTop, ((2 ^ k n * 3 ^ l n : ℕ) : ℝ) < (n : ℝ) ^ (1 + c n)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/933.lean, line 56.
Erdos933.erdos_933.variants.lower_bound
Proved here.
Erdős [Er76d] wrote 'it is easy to see' that for infinitely many \(n\), \(2^k 3^l > n\log n\).
Steinerberger has noted a simple proof of this fact follows from taking \(n=2^{3^r}\) for any integer \(r\geq 1\), when \(k=3^r\) and \(l=r+1\).
theorem erdos_933.variants.lower_bound :
Set.Infinite { n : ℕ | ((2 ^ k n * 3 ^ l n : ℕ) : ℝ) > (n : ℝ) * Real.log (n : ℝ) }
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/933.lean, line 68.
Sources
TheoremErdős Problem 934#
References: - erdosproblems.com/934 - [Er88] Erdős, P., Problems and results in combinatorial analysis and graph theory. Discrete Math. 72 (1988), 81-92. - [BBPP83] Bermond, J.-C., Bond, J., Paoli, M. and Peyrat, C., Graphs and interconnection networks: diameter and vulnerability. Surveys in Combinatorics (Southampton, 1983), London Math. Soc. Lecture Note Ser. 82, Cambridge Univ. Press (1983), 1-30. - [CGTT90] Chung, F. R. K., Gyárfás, A., Tuza, Z. and Trotter, W. T., The maximum number of edges in \(2K_2\)-free graphs of bounded degree. Discrete Math. 81 (1990), 129-135. - [CCJK22] Cambie, S., Cames van Batenburg, W., de Joannis de Verclos, R. and Kang, R. J., Maximising line subgraphs of diameter at most \(t\). SIAM J. Discrete Math. 36 (2022), 939-950. arXiv:2103.11898 - [KMP26] Kumar, H., Mohar, B. and Pragada, S., An improved bound for the strong clique index of graphs. arXiv:2607.02698 (2026). - [CvBK26] Cames van Batenburg, W. and Korsky, S., Asymptotically attaining the Moore bound. arXiv:2608.03965 (2026).
Quoted from FormalConjectures/ErdosProblems/934.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/934.
The file states 10 research or textbook statements: 1 open and 9 solved. It also has 1 API statement, counted here but not shown.
Erdos934.erdos_934
Open: stated without proof.
Let \(h_t(d)\) be minimal such that every graph \(G\) with \(h_t(d)\) edges and maximal degree \(\leq d\) contains two edges whose shortest path between them has length \(\geq t\).
Estimate \(h_t(d)\).
A problem of Erdős and Nešetřil [Er88]. Erdős wrote 'This problem seems to be interesting only if there is a nice expression for \(h_t(d)\).' We read "estimate" as asking for an exact expression, as in that remark:
h t d = erdos_934.answer t dfor all1 ≤ tand alld.
theorem erdos_934 : ∀ t d : ℕ, 1 ≤ t → h t d = erdos_934.answer t d
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/934.lean, line 91.
Erdos934.erdos_934.variants.h_one
Solved: stated here without proof.
It is easy to see that \(h_t(d)\leq 2d^t\) always and \(h_1(d)=d+1\).
The site (and [CCJK22, p. 1]) states \(h_1(d)=d+1\) without restriction; it fails for \(d=2\) (the triangle has three pairwise intersecting edges, so \(h_1(2)=4\)), hence we assume \(d\neq 2\).
theorem erdos_934.variants.h_one : ∀ d : ℕ, d ≠ 2 → h 1 d = d + 1
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/934.lean, line 101.
Erdos934.erdos_934.variants.h_two
Solved: stated here without proof.
Erdős and Nešetřil and Bermond, Bond, Paoli, and Peyrat [BBPP83] independently conjectured that \(h_2(d) \leq \tfrac{5}{4}d^2+1\), with equality for even \(d\). This was proved by Chung, Gyárfás, Tuza, and Trotter [CGTT90].
theorem erdos_934.variants.h_two :
(∀ d : ℕ, 4 * h 2 d ≤ 5 * d ^ 2 + 4) ∧
∀ d : ℕ, Even d → 4 * h 2 d = 5 * d ^ 2 + 4
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/934.lean, line 110.
Erdos934.erdos_934.variants.h_three_three
Solved: stated here without proof.
Cambie, Cames van Batenburg, de Joannis de Verclos, and Kang [CCJK22, Theorem 2] proved that \(h_3(3)=23\).
theorem erdos_934.variants.h_three_three : h 3 3 = 23
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/934.lean, line 119.
Erdos934.erdos_934.variants.upper
Solved: stated here without proof.
The same authors prove that for all \(t\geq 1\) we have
\[h_t(d) \leq \tfrac{3}{2}d^t+1.\]See [CCJK22, Theorem 6]. Here the inequality is stated as
2 * h t d ≤ 3 * d ^ t + 2.
theorem erdos_934.variants.upper :
∀ t d : ℕ, 1 ≤ t → 2 * h t d ≤ 3 * d ^ t + 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/934.lean, line 128.
Erdos934.erdos_934.variants.lower_large_t
Solved: stated here without proof.
The same authors prove that, if \(t\) is large, then there are infinitely many \(d\) such that \(h_t(d) \geq 0.629^td^t\). See [CCJK22, Proposition 5].
theorem erdos_934.variants.lower_large_t :
∃ t₀ : ℕ, ∀ t : ℕ, t₀ ≤ t →
∃ᶠ d : ℕ in atTop, ((629 : ℝ) / 1000) ^ t * (d : ℝ) ^ t ≤ (h t d : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/934.lean, line 137.
Erdos934.erdos_934.variants.kmp_h_three_four
Solved: stated here without proof.
Cambie, Cames van Batenburg, de Joannis de Verclos, and Kang [CCJK22] conjectured that \(h_3(d) \leq d^3-d^2+d+2\) (with equality if \(d-1\) is a prime power; the site writes "if and only if", while [CCJK22, Conjecture 1] says "if"). Kumar, Mohar and Pragada [KMP26, Lemma 3.1] refute the inequality: the odd graph \(KG(7,3)\) has \(35\) vertices, is \(4\)-regular, has \(70\) edges and any two of its edges are at distance less than \(3\), so \(h_3(4)\geq 71 > 54\).
theorem erdos_934.variants.kmp_h_three_four : 71 ≤ h 3 4
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/934.lean, line 150.
Erdos934.erdos_934.variants.ccjk_conjecture_false
Solved: stated here without proof.
The inequality \(h_3(d) \leq d^3-d^2+d+2\) conjectured in [CCJK22] is false [KMP26, Conjecture 1.9 and Lemma 3.1]. Here the inequality is stated as
h 3 d + d ^ 2 ≤ d ^ 3 + d + 2.
theorem erdos_934.variants.ccjk_conjecture_false :
¬ ∀ d : ℕ, h 3 d + d ^ 2 ≤ d ^ 3 + d + 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/934.lean, line 158.
Erdos934.erdos_934.variants.kmp_liminf
Solved: stated here without proof.
Kumar, Mohar and Pragada [KMP26, Theorem 1.11] proved
\[\liminf_{d\to\infty}\frac{h_3(d)}{d^3}\geq \frac{253}{225}.\]In particular the conjecture of [CCJK22] that \(h_t(d)\leq (1+o(1))d^t\) is false for \(t=3\).
theorem erdos_934.variants.kmp_liminf :
∀ ε > (0 : ℝ), ∀ᶠ d : ℕ in atTop, (253 / 225 - ε) * (d : ℝ) ^ 3 ≤ (h 3 d : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/934.lean, line 168.
Erdos934.erdos_934.variants.lower_liminf
Solved: stated here without proof.
For every fixed \(t\geq 2\), \(\liminf_{d\to\infty} h_t(d)/d^t \geq 1\) [CvBK26, Corollary 1.2]. This confirms, in a strong form, the conjecture of [CCJK22] that \(h_t(d)\geq (1-o(1))d^t\) for infinitely many \(d\).
theorem erdos_934.variants.lower_liminf :
∀ t : ℕ, 2 ≤ t → ∀ ε > (0 : ℝ), ∀ᶠ d : ℕ in atTop,
(1 - ε) * (d : ℝ) ^ t ≤ (h t d : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/934.lean, line 178.
Sources
TheoremErdős Problem 935#
References: - erdosproblems.com/935 - [Er76d] Erdős, P., Problems and results on number theoretic properties of consecutive integers and related questions. Proceedings of the Fifth Manitoba Conference on Numerical Mathematics (Univ. Manitoba, Winnipeg, Man., 1975) (1976), 25-44. PDF - [Fe26] Feng, T. et al., Semi-Autonomous Mathematics Discovery with Gemini: A Case Study on the Erdős Problems. arXiv:2601.22401 (2026).
The powerful part \(Q_2(m)\) of \(m\) is
Erdos367.B 2 m, the product of \(p^a\) over the primes \(p\) with \(p^a \parallel m\) and \(a \geq 2\). The second question is essentially the same as erdosproblems.com/367.
Quoted from FormalConjectures/ErdosProblems/935.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/935.
The file states 5 research or textbook statements: 2 open and 3 solved.
Erdos935.erdos_935.parts.i
Open: stated without proof.
For any integer \(n=\prod p^{k_p}\) let \(Q_2(n)\) be the powerful part of \(n\), so that
\[Q_2(n) = \prod_{\substack{p\\ k_p\geq 2}}p^{k_p}.\]Is it true that, for every \(\epsilon>0\) and \(\ell\geq 1\), if \(n\) is sufficiently large then
\[Q_2(n(n+1)\cdots(n+\ell))\lt n^{2+\epsilon}?\]A problem of Erdős [Er76d, p. 32], who writes that if this is true then it seems very difficult to prove. This is the first part.
theorem erdos_935.parts.i :
∀ ε : ℝ, 0 < ε → ∀ ℓ : ℕ, 1 ≤ ℓ → ∀ᶠ n : ℕ in atTop,
((Erdos367.B 2 (∏ m ∈ Finset.Icc n (n + ℓ), m) : ℕ) : ℝ) < (n : ℝ) ^ (2 + ε)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/935.lean, line 54.
Erdos935.erdos_935.parts.ii
Solved: stated here without proof.
For any integer \(n=\prod p^{k_p}\) let \(Q_2(n)\) be the powerful part of \(n\), so that
\[Q_2(n) = \prod_{\substack{p\\ k_p\geq 2}}p^{k_p}.\]If \(\ell\geq 2\) then is
\[\limsup_{n\to \infty}\frac{Q_2(n(n+1)\cdots(n+\ell))}{n^2}\]infinite?
This is the second part. We write "infinite" as: for every \(C\), \(C n^2 < Q_2(\cdots)\) for infinitely many \(n\). The answer is yes, by the Pell equation construction of
erdos_935.variants.ell_two(the case \(\ell = 2\)); for larger \(\ell\) the product for \(\ell = 2\) divides the product for \(\ell\), and \(Q_2\) does not decrease under divisibility.
theorem erdos_935.parts.ii :
∀ ℓ : ℕ, 2 ≤ ℓ → ∀ C : ℝ, ∃ᶠ n : ℕ in atTop,
C * (n : ℝ) ^ 2 < ((Erdos367.B 2 (∏ m ∈ Finset.Icc n (n + ℓ), m) : ℕ) : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/935.lean, line 72.
Erdos935.erdos_935.parts.iii
Open: stated without proof.
For any integer \(n=\prod p^{k_p}\) let \(Q_2(n)\) be the powerful part of \(n\), so that
\[Q_2(n) = \prod_{\substack{p\\ k_p\geq 2}}p^{k_p}.\]If \(\ell\geq 2\) then is
\[\lim_{n\to \infty}\frac{Q_2(n(n+1)\cdots(n+\ell))}{n^{\ell+1}}=0?\]This is the third part. The restriction \(\ell \geq 2\) is needed: for \(\ell = 1\) the Pell solutions of
erdos_935.variants.mahlergive \(Q_2(n(n+1)) = n(n+1)\) infinitely often.
theorem erdos_935.parts.iii :
∀ ℓ : ℕ, 2 ≤ ℓ → Tendsto
(fun n : ℕ ↦ ((Erdos367.B 2 (∏ m ∈ Finset.Icc n (n + ℓ), m) : ℕ) : ℝ) / (n : ℝ) ^ (ℓ + 1))
atTop (nhds 0)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/935.lean, line 87.
Erdos935.erdos_935.variants.mahler
Solved: stated here without proof.
A result of Mahler implies, for every \(\ell\geq 1\),
\[\limsup_{n\to \infty}\frac{Q_2(n(n+1)\cdots(n+\ell))}{n^2}\geq 1.\]Erdős [Er76d, pp. 31-32] derives this from the infinitely many solutions of \(x^2-8y^2=1\), which give consecutive powerful numbers. We write \(\limsup \geq 1\) as: for every \(\varepsilon > 0\), \((1-\varepsilon) n^2 < Q_2(\cdots)\) for infinitely many \(n\).
theorem erdos_935.variants.mahler :
∀ ℓ : ℕ, 1 ≤ ℓ → ∀ ε : ℝ, 0 < ε → ∃ᶠ n : ℕ in atTop,
(1 - ε) * (n : ℝ) ^ 2 < ((Erdos367.B 2 (∏ m ∈ Finset.Icc n (n + ℓ), m) : ℕ) : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/935.lean, line 102.
Erdos935.erdos_935.variants.ell_two
Solved: stated here without proof.
The construction of van Doorn for [367] (also given by Aletheia [Fe26, §4.2]) proves the second part in the affirmative: a construction via solutions to the Pell equation \(x^2-8y^2=1\) implies
\[\limsup_{n\to \infty}\frac{Q_2(n(n+1)(n+2))}{n^2}=\infty.\]This is the case \(\ell = 2\), stated as in
erdos_935.parts.ii.
theorem erdos_935.variants.ell_two :
∀ C : ℝ, ∃ᶠ n : ℕ in atTop,
C * (n : ℝ) ^ 2 < ((Erdos367.B 2 (∏ m ∈ Finset.Icc n (n + 2), m) : ℕ) : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/935.lean, line 115.
Sources
TheoremErdős Problem 936#
Reference: erdosproblems.com/936
Quoted from FormalConjectures/ErdosProblems/936.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/936.
The file states 4 research or textbook statements: 4 open.
Erdos936.erdos_936.variants.two_pow_add_one
Open: stated without proof.
Is \(2^n + 1\) powerful for finitely many \(n\)?
theorem erdos_936.variants.two_pow_add_one :
EventuallyNotPowerful (2 ^ · + 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/936.lean, line 39.
Erdos936.erdos_936.variants.two_pow_sub_one
Open: stated without proof.
Is \(2^n - 1\) powerful for finitely many \(n\)?
theorem erdos_936.variants.two_pow_sub_one :
EventuallyNotPowerful (2 ^ · - 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/936.lean, line 45.
Erdos936.erdos_936.variants.factorial_add_one
Open: stated without proof.
Is \(n! + 1\) powerful for finitely many \(n\)?
theorem erdos_936.variants.factorial_add_one :
EventuallyNotPowerful (·! + 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/936.lean, line 51.
Erdos936.erdos_936.variants.factorial_sub_one
Open: stated without proof.
Is \(n! - 1\) powerful for finitely many \(n\)?
theorem erdos_936.variants.factorial_sub_one :
EventuallyNotPowerful (·! - 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/936.lean, line 57.
Sources
TheoremErdős Problem 937#
Reference: erdosproblems.com/937
References: * [BBC24] Bajpai, P., Bennett, M. A. and Chan, T. H., Arithmetic progressions in squarefull / powerful numbers, Int. J. Number Theory 20 (2024), 19-45.
Quoted from FormalConjectures/ErdosProblems/937.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/937.
The file states 1 research or textbook statement: 1 solved. It also has 1 test statement, counted here but not shown.
Erdos937.erdos_937
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/dfe2d78128b493c572cf525b1b8edf4897fb7664/src/latest/ErdosProblems/Erdos937.lean#L1031.
Are there infinitely many four-term arithmetic progressions of coprime powerful numbers? (A number \(n\) is powerful if \(p \mid n \to p^2 \mid n\);
Nat.Powerful.)Erdős [Er76d] asked this; the answer is yes: Bajpai, Bennett and Chan [BBC24] proved that there are infinitely many four-term arithmetic progressions of pairwise coprime powerful numbers. (Without coprimality this is easy, and by a theorem of Fermat there are no four squares in arithmetic progression.)
theorem erdos_937 :
{p : ℕ × ℕ | IsCoprimePowerfulAP4 p.1 p.2}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/937.lean, line 56.
Sources
TheoremErdős Problem 938#
Reference: erdosproblems.com/938
Quoted from FormalConjectures/ErdosProblems/938.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/938.
The file states 1 research or textbook statement: 1 open.
Erdos938.erdos_938
Open: stated without proof.
Let \(A=\{n_1 < n_2 < \cdots\}\) be the sequence of powerful numbers (if \(p\mid n\) then \(p^2\mid n\)). Are there only finitely many three-term progressions of consecutive terms \(n_k,n_{k+1},n_{k+2}\)?
theorem erdos_938 : {P : Finset ℕ | (P : Set ℕ).IsAPOfLength 3 ∧ ∃ k,
P = {nth Powerful k, nth Powerful (k + 1), nth Powerful (k + 2)}}.Finite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/938.lean, line 37.
Sources
TheoremErdős Problem 939#
References: - erdosproblems.com/939 - [Ni95] Nitaj, A., On a conjecture of Erdős on 3-powerful numbers. Bull. London Math. Soc. (1995), 317-318. - [Co98] Cohn, J. H. E., A conjecture of Erdős on 3-powerful numbers. Math. Comp. (1998), 439-440. - [Wa24] Walsh, P., A question of Erdős on 3-powerful numbers and an elliptic curve analogue of the Ankeny-Artin-Chowla conjecture. arXiv:2404.03970 (2024). - [LaPa67] Lander, L. J. and Parkin, T. R., A counterexample to Euler's sum of powers conjecture. Math. Comp. (1967), 101-103.
Quoted from FormalConjectures/ErdosProblems/939.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/939.
The file states 8 research or textbook statements: 1 open and 7 solved.
Erdos939.erdos_939
Open: stated without proof.
If \(r≥4\) then can the sum of \(r-2\) coprime \(r\)-powerful numbers ever be itself \(r\)-powerful?
theorem erdos_939 : ∀ r ≥ 4, (Erdos939Sums r).Nonempty
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/939.lean, line 61.
Erdos939.erdos_939.variants.finite
Solved: stated here without proof.
If \(r≥4\), are there at most finitely many sums of \(r-2\) coprime \(r\)-powerful numbers that are themselves \(r\)-powerful?
The answer is no: for every \(r \ge 6\) there are infinitely many such sums, see
erdos_939.variants.infinite_of_six_le. (For \(r = 4\) and \(r = 5\) the question is open; for \(r = 4\) no example is known at all, seeerdos_939.) A construction in the site's comments, from GPT-5.5 Pro prompted by Price, gives infinitely many for every \(r \ge 6\). This statement quantifies over every \(r \ge 4\), so it stays open at \(r = 4\) and \(r = 5\). The category is unchanged because the construction is recorded in the comments and not in the literature.
theorem erdos_939.variants.finite : ¬ ∀ r ≥ 4, (Erdos939Sums r).Finite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/939.lean, line 77.
Erdos939.erdos_939.variants.infinite_of_six_le
Solved: stated here without proof.
For every \(r \ge 6\) there are infinitely many sums of \(r - 2\) coprime \(r\)-powerful numbers that are themselves \(r\)-powerful.
A construction, found by GPT-5.5 Pro prompted by Liam Price and recorded in the comments on erdosproblems.com/939, expands \((X+Y)^r = (X-Y)^r + \sum_{j \text{ odd}} 2\binom{r}{j} X^{r-j} Y^j\), splits the \(j = 3\) term into \(\lfloor r/2 \rfloor - 2\) distinct pieces to obtain exactly \(r - 2\) summands, and takes \(X = q^r\), \(Y = B^r\) with \(B\) divisible by all primes in the coefficients and \(q > B\) a prime not dividing \(B\); varying \(q\) gives infinitely many solutions.
theorem erdos_939.variants.infinite_of_six_le : ∀ r ≥ 6, (Erdos939Sums r).Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/939.lean, line 92.
Erdos939.erdos_939.variants.triples
Solved: stated here without proof.
Are there infinitely many triples of coprime \(3\)-powerful numbers \(a, b, c\) such that \(a + b = c\)?
The answer is yes. Nitaj [Ni95] proved it, with \(2^3\cdot 3^5\cdot 73^3 + 271^3 = 919^3\) as an example. In Nitaj's construction at least two of \(a, b, c\) are perfect cubes. Cohn [Co98] constructed infinitely many triples of which none is a perfect cube, and Walsh [Wa24] gave a further construction.
theorem erdos_939.variants.triples :
{(a,b,c) | ({a, b, c} : Finset ℕ).Coprime ∧
0 < a ∧ 0 < b ∧
(3).Full a ∧ (3).Full b ∧ (3).Full c ∧
a + b = c}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/939.lean, line 104.
Erdos939.erdos_939.variants.examples
Proved here.
Cambie has found several examples of the sum of \(r - 2\) coprime \(r\)-powerful numbers being itself \(r\)-powerful. For example when \(r=5\) we have
\[3^7\cdot 61^5 = 2^8\cdot3^{10}\cdot 5^7 + 2^{12}\cdot 23^6 + 11^5\cdot 13^5\].
theorem erdos_939.variants.examples : (∃ r ≥ 4, (Erdos939Sums r).Nonempty)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/939.lean, line 117.
Erdos939.erdos_939.variants.seven
Solved: stated here without proof.
Cambie has also found solutions when \(r=7\).
theorem erdos_939.variants.seven : (Erdos939Sums 7).Nonempty
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/939.lean, line 132.
Erdos939.erdos_939.variants.eight
Solved: stated here without proof.
Cambie has also found solutions when \(r=8\).
The source adds that the \(r=8\) solution works "even with the sum of \(5\) \(8\)-powerful numbers". That is a stronger result than this statement, which asks for the \(r - 2 = 6\) summands of
Erdos939Sums.
theorem erdos_939.variants.eight : (Erdos939Sums 8).Nonempty
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/939.lean, line 143.
Erdos939.erdos_939.variants.euler
Proved here.
Euler had conjectured that the sum of \(k - 1\) many \(k\)-th powers is never a \(k\)-th power, but this is false for \(k=5\), as Lander and Parkin [LaPa67] found
\[27^5+84^5+110^5+133^5=144^5\].
The summands must be positive. Without that condition a set containing
0would count, so the negation would be satisfied by a sum of fewer than \(k-1\) powers and would claim less than the refutation of Euler's conjecture that this theorem records.
theorem erdos_939.variants.euler : ¬ (∀ k ≥ 4, ∀ S : Finset ℕ, S.card = k - 1 →
(∀ s ∈ S, 0 < s) → ¬ (∃ q, ∑ s ∈ S, s ^ k = q ^k))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/939.lean, line 156.
Sources
TheoremErdős Problem 940#
References: - erdosproblems.com/940 - [BaBr94] Baker, R. C. and Brüdern, J., On sums of two squarefull numbers. Math. Proc. Cambridge Philos. Soc. (1994), 1-5. - [He88] Heath-Brown, D. R., Ternary quadratic forms and sums of three square-full numbers. (1988), 137-163.
Quoted from FormalConjectures/ErdosProblems/940.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/940.
The file states 5 research or textbook statements: 3 open and 2 solved.
Erdos940.erdos_940
Open: stated without proof.
Let \(r \ge 3\). Is it true that the set of integers which are the sum of at most \(r\) \(r\)-powerful numbers has density \(0\)?
theorem erdos_940 :
∀ r ≥ 3,
{n : ℕ | ∃ (S : Multiset ℕ), S.card ≤ r ∧ (∀ s ∈ S, r.Full s) ∧ n = S.sum}.HasDensity 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/940.lean, line 42.
Erdos940.erdos_940.variants.two
Solved: stated here without proof.
The set of integers which are the sum of at most two \(2\)-powerful numbers has density \(0\).
Erdős called this 'easy'. Baker and Brüdern [BaBr94] gave the first proof in the literature.
theorem erdos_940.variants.two :
{n : ℕ | ∃ (S : Multiset ℕ),
S.card ≤ 2 ∧ (∀ s ∈ S, (2).Full s) ∧ n = S.sum}.HasDensity 0
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/940.lean, line 53.
Erdos940.erdos_940.variants.three_cubes
Open: stated without proof.
Is it true that the set of integers which are the sum of at most three cubes has density \(0\)?
The cubes are those of non-negative integers, which is what
Multiset ℕgives. This choice decides the question: overℤa sum of three cubes is conjectured to represent every integer that is not \(\pm 4 \bmod 9\), which is density \(7/9\).
theorem erdos_940.variants.three_cubes :
{n : ℕ | ∃ (S : Multiset ℕ), S.card ≤ 3 ∧ n = (Multiset.map (· ^ 3) S).sum}.HasDensity 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/940.lean, line 66.
Erdos940.erdos_940.variants.large_integers
Open: stated without proof.
Let \(r \ge 3\). Are there infinitely many integers which are not the sum of at most \(r\)-many \(r\)-powerful numbers?
theorem erdos_940.variants.large_integers :
∀ r ≥ 3, ¬ (∀ᶠ x in atTop, ∃ (S : Multiset ℕ), S.card ≤ r ∧ (∀ s ∈ S, r.Full s) ∧ x = S.sum)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/940.lean, line 76.
Erdos940.erdos_940.variants.three_powerful
Solved: stated here without proof.
Heath-Brown [He88] has proved that all large numbers are the sum of at most three \(2\)-powerful numbers.
This is the case \(r = 2\) of
Erdos1107.erdos_1107, which asks the same question with \(r + 1\) summands, and it is stated there asErdos1107.erdos_1107.variants.two.
theorem erdos_940.variants.three_powerful :
∀ᶠ x in atTop, ∃ (S : Multiset ℕ), S.card ≤ 3 ∧ (∀ s ∈ S, (2).Full s) ∧ x = S.sum
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/940.lean, line 88.
Sources
TheoremErdős Problem 942#
Reference: erdosproblems.com/942
Quoted from FormalConjectures/ErdosProblems/942.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/942.
The file states 3 research or textbook statements: 1 open and 2 textbook results.
Erdos942.erdos_942
Open: stated without proof.
Is there some constant \(c > 0\) such that \(h(n) < (\log n)^{c + o(1)}\) and, for infinitely many \(n\), \(h(n) > (\log n)^{c - o(1)}\).
theorem erdos_942 : ∃ c > 0, ∃ (o : ℕ → ℝ), o =o[atTop] (1 : ℕ → ℝ) ∧
(∀ᶠ n in atTop, erdos_942.h n < (Real.log n) ^ (c + o n)) ∧
{n | erdos_942.h n > (Real.log n) ^ (c - o n)}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/942.lean, line 42.
Erdos942.erdos_942.variants.limsup
Textbook result, stated without proof.
It is not hard to prove that \(\limsup h(n) = \infty\).
theorem erdos_942.variants.limsup :
atTop.limsup (((fun (n : ℕ) ↦ (n : ℕ∞)) ∘ erdos_942.h)) = ⊤
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/942.lean, line 51.
Erdos942.erdos_942.variants.density
Textbook result, stated without proof.
It is not hard to prove that the density \(\delta_l\) of integers for which \(h(n) = l\) exists and satisfies
\[\sum_l \delta_l = 1\].
theorem erdos_942.variants.density :
∃ δ : ℕ → ℝ, ∀ l, {n | erdos_942.h n = l}.HasDensity (δ l) ∧
∑' l, δ l = 1
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/942.lean, line 60.
Sources
TheoremErdős Problem 943#
Reference: erdosproblems.com/943
Quoted from FormalConjectures/ErdosProblems/943.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/943.
The file states 1 research or textbook statement: 1 open.
Erdos943.erdos_943
Open: stated without proof.
Let \(A\) be the set of powerful numbers. Is is true that \(1_A\ast 1_A(n)=n^{o(1)}\) for every \(n\)?
theorem erdos_943 :
∃ (o : ℕ → ℝ), o =o[atTop] (1 : ℕ → ℝ) ∧ ∀ᶠ n in atTop, (sumRep Powerful n) ≤ (n : ℝ)^(o n)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/943.lean, line 36.
Sources
TheoremErdős Problem 944#
Reference: erdosproblems.com/944
Quoted from FormalConjectures/ErdosProblems/944.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/944.
The file states 7 research or textbook statements: 1 open and 6 solved.
Erdos944.erdos_944
Open: stated without proof.
Let \(k \ge 4\) and \(r\ge 1\). Must there exist a graph \(G\) with chromatic number \(k\) such that every vertex is critical, yet every critical set of edges has size \(>r\)?
theorem erdos_944 :
∀ k ≥ 4, ∀ r ≥ 1, ∃ (V : Type u) (G : SimpleGraph V), G.IsErdos944 k r
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/944.lean, line 47.
Erdos944.erdos_944.variants.dirac_conjecture
Solved: stated here without proof.
Let \(k \ge 4\). Must there exist a graph \(G\) with chromatic number \(k\) such that every vertex is critical, yet every critical set of edges has size \(>1\)?
This was conjectured by Dirac in 1970.
theorem erdos_944.variants.dirac_conjecture :
∀ k ≥ 4, ∃ (V : Type u) (G : SimpleGraph V), G.IsErdos944 k 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/944.lean, line 58.
Erdos944.erdos_944.variants.dirac_conjecture.k_eq_5
Solved: stated here without proof.
Dirac's conjecture was proved, for \(k=5\): There exists a graph \(G\) with chromatic number \(5\), such that every vertex is critical, yet every critical set of edges has size \(>1\), or in other words: has no critical edge.
[Br92] Brown, Jason I., A vertex critical graph without critical edges. Discrete Math. (1992), 99--101
theorem erdos_944.variants.dirac_conjecture.k_eq_5 :
∃ (V : Type u) (G : SimpleGraph V), G.IsErdos944 5 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/944.lean, line 71.
Erdos944.erdos_944.variants.dirac_conjecture.k_sub_one_not_prime
Solved: stated here without proof.
Lattanzio [La02] proved there exist \(k\)-critical graphs without critical edges for all \(k\) such that \(k - 1\) is not prime.
[La02] Lattanzio, John J., A note on a conjecture of {D}irac. Discrete Math. (2002), 323--330
theorem erdos_944.variants.dirac_conjecture.k_sub_one_not_prime (k : ℕ) (hk : 4 ≤ k)
(h : ¬ (k - 1).Prime) : ∃ (V : Type u) (G : SimpleGraph V), G.IsErdos944 k 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/944.lean, line 82.
Erdos944.erdos_944.variants.dirac_conjecture.k_ge_five
Solved: stated here without proof.
Jensen [Je02] gave an construction for \(k\)-critical graphs without any critical edges for all \(k ≥ 5\).
[Je02] Jensen, Tommy R., Dense critical and vertex-critical graphs. Discrete Math. (2002), 63--84.
theorem erdos_944.variants.dirac_conjecture.k_ge_five (k : ℕ) (hk : 5 ≤ k) :
∃ (V : Type u) (G : SimpleGraph V), G.IsErdos944 k 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/944.lean, line 92.
Erdos944.erdos_944.variants.dirac_conjecture.k_eq_four
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-944-dirac-k4-lean/blob/9606d77/lean4web/Erdos944K4R1Lean4Web.lean#L676-L690.
The case \(k=4\) and \(r=1\) was the remaining open case: Are there \(4\)-critical graphs without any critical edges?
Answer: Yes. The Lean formalization linked below proves the existence of such a graph. Together with Jensen's result for \(k \ge 5\), this settles Dirac's conjecture for every \(k \ge 4\).
theorem erdos_944.variants.dirac_conjecture.k_eq_four :
∃ (V : Type u) (G : SimpleGraph V), G.IsErdos944 4 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/944.lean, line 108.
Erdos944.erdos_944.variants.large_k_for_any_r
Solved: stated here without proof.
Martinsson and Steiner [MaSt25] proved for every \(r \ge 1\) if \(k\) is sufficiently large, depending on \(r\), there exist a graph \(G\) with chromatic number \(k\) such that every vertex is critical, yet every critical set of edges has size \(>r\).
[MaSt25] Martinsson, Anders and Steiner, Raphael, Vertex-critical graphs far from edge-criticality. Combin. Probab. Comput. (2025), 151--157
theorem erdos_944.variants.large_k_for_any_r (r : ℕ) (hr : 1 ≤ r) : ∀ᶠ k in Filter.atTop,
∃ (V : Type u) (G : SimpleGraph V), G.IsErdos944 k r
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/944.lean, line 120.
Sources
TheoremErdős Problem 945#
References: - erdosproblems.com/945 - [ErMi52] Erdős, P. and Mirsky, L., The distribution of values of the divisor function {\(d(n)\)}. Proc. London Math. Soc. (3) (1952), 257--271.
Quoted from FormalConjectures/ErdosProblems/945.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/945.
The file states 5 research or textbook statements: 2 open, 2 solved and 1 textbook result.
Erdos945.erdos_945
Open: stated without proof.
Is it true that \(F(x) \leq (\log x)^{O(1)}\)?
theorem erdos_945 : Erdos945Prop
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/945.lean, line 51.
Erdos945.erdos_945.variants.constant
Open: stated without proof.
Is there a constant \(C > 0\) such that, for all large \(x\), every interval \([x, x+(\log x)C]\) contains two integers with the same number of divisors?
theorem erdos_945.variants.constant : Erdos945Constant
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/945.lean, line 66.
Erdos945.erdos_945.variants.equivalence
Textbook result, stated without proof.
The two ways of phrasing the conjecture are equivalent.
theorem erdos_945.variants.equivalence : Erdos945Prop ↔ Erdos945Constant
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/945.lean, line 74.
Erdos945.erdos_945.variants.lower_bound
Solved: stated here without proof.
Erdős and Mirsky [ErMi52] proved that \(\frac{(\log x)^{1/2}}{\log\log x}\ll F(x)\).
theorem erdos_945.variants.lower_bound :
(fun (x : ℕ) => (log x).sqrt /(log x).log) =O[atTop] fun (n : ℕ) => (F n : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/945.lean, line 81.
Erdos945.erdos_945.variants.upper_bound
Solved: stated here without proof.
Erdős and Mirsky [ErMi52] proved that \(\log F(x) \ll \frac{(\log x)^{1/2}}\).
theorem erdos_945.variants.upper_bound :
(fun (n : ℕ) => (F n : ℝ).log) =O[atTop] fun (x : ℕ) => (log x).sqrt /(log x).log
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/945.lean, line 89.
Sources
TheoremErdős Problem 946#
References: - erdosproblems.com/946 - [ErMi52] Erdős, P. and Mirsky, L., The distribution of values of the divisor function {\(d(n)\)}. Proc. London Math. Soc. (3) (1952), 257--271. - [Sp81] Spiro, C. A., The frequency with which an integral-valued, prime-independent, multiplicative or additive function of n divides a polynomial function of n. - [He84] Heath-Brown, D. R., The divisor function at consecutive integers. Mathematika 31 (1984), no. 2, 141--149. - [Hi85] Hildebrand, A., The divisor function at consecutive integers. Pacific J. Math. (1987), 307--319 - [EPS87] Erdős, P., Pomerance, C., and Sarkőzy, A., On locally repeated values of arithmetic functions. III. Proc. Amer. Math. Soc. (1987), 1--7.
Quoted from FormalConjectures/ErdosProblems/946.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/946.
The file states 5 research or textbook statements: 5 solved.
Erdos946.erdos_946
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos946.lean#L75.
There are infinitely many \(n\) such that \(τ(n) = τ(n+1)\). Proved in [He84]. Here τ is the divisor counting function, which is
σ 0in mathlib.
theorem erdos_946 : {n : ℕ | σ 0 n = σ 0 (n + 1)}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/946.lean, line 52.
Erdos946.erdos_946.variants.spiro_5040
Solved: stated here without proof.
There are infinitely many \(n\) such that \(τ(n) = τ(n + 5040)\). Proved in [Sp81].
theorem erdos_946.variants.spiro_5040 : {n : ℕ | σ 0 n = σ 0 (n + 5040)}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/946.lean, line 59.
Erdos946.erdos_946.variants.heathbrown_lower_bound
Solved: stated here without proof.
The number of \(n \le x\) with \(τ(n) = τ(n+1)\) is at least \(x / (\log x)^7\) for all sufficiently large \(x\). Proved in [He84].
theorem erdos_946.variants.heathbrown_lower_bound :
(fun x => x / (x.log)^7) =O[atTop] erdos946Count
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/946.lean, line 71.
Erdos946.erdos_946.variants.hildebrand_lower_bound
Solved: stated here without proof.
Improved lower bound in [Hi85]: \(Ω(x / (\log \log x)^3)\).
theorem erdos_946.variants.hildebrand_lower_bound :
(fun x => x / (x.log.log)^3) =O[atTop] erdos946Count
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/946.lean, line 79.
Erdos946.erdos_946.variants.upper_bound
Solved: stated here without proof.
Upper bound in [EPS87]: \(O(x / \sqrt{\log \log x})\).
theorem erdos_946.variants.upper_bound : erdos946Count =O[atTop] (fun x => x / √x.log.log )
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/946.lean, line 87.
Sources
TheoremErdős Problem 947#
References: - erdosproblems.com/947 - [Er77c] Erdős, Paul, Problems and results on combinatorial number theory. III. Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976) (1977), 43-72. - [Er50] Erdős, P., On integers of the form \(2^k+p\) and some related problems. Summa Brasil. Math. (1950), 113-123.
Quoted from FormalConjectures/ErdosProblems/947.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/947.
The file states 1 research or textbook statement: 1 solved.
Erdos947.erdos_947
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos947.lean#L277.
There is no exact covering system - that is, a finite collection of congruence classes \(a_i\pmod{n_i}\) with distinct \(n_i\) such that every integer satisfies exactly one of these congruence classes.
This is true, and was proved independently by Mirsky and Newman and by Davenport and Rado; the Mirsky–Newman proof first appeared in [Er50]. See also [Er77c].
A
StrictCoveringSystem ℤis a finite family of congruence classes with distinct moduli \(n_i \geq 2\) covering \(\mathbb{Z}\); the trivial exact covering system consisting of the single class \(0 \pmod 1\) is therefore excluded.
theorem erdos_947 : ¬ ∃ c : StrictCoveringSystem ℤ, Pairwise (Disjoint on c.coset)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/947.lean, line 52.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.