Erdős Problem 423 to Erdős Problem 444
TheoremErdős Problem 423#
References: - erdosproblems.com/423 - [Er77c] Erdős, P., Problems and results on combinatorial number theory. III, Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976), 1977, pp. 43–72. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory, Monographies de L'Enseignement Mathématique (1980). - [Cu25] Cushman, A., A Note on the Sum-Product Problem and the Convex Sumset Problem. arXiv:2512.13849 (2025). - [Ta26] Tang, Q., The Hofstadter consecutive-sum sequence omits infinitely many positive integers. arXiv:2603.09939 (2026). - [Bolan] Bolan, M., Hofstader–Ulam Sequence, https://github.com/mjtb49/HofstaderUlam/blob/main/HofstaderUlamSequence.pdf - OEIS A005243
Quoted from FormalConjectures/ErdosProblems/423.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/423.
The file states 6 research or textbook statements: 1 open and 5 solved. It also has 3 test statements and 5 API statements, counted here but not shown.
Erdos423.erdos_423
Open: stated without proof.
Erdős Problem 423 [Er77c, p.71; ErGr80, p.83]:
Let \(a(1) = 1\), \(a(2) = 2\), and for \(k \ge 3\) let \(a(k)\) be the least integer greater than \(a(k-1)\) that is a sum of at least two consecutive terms of the sequence. What is the asymptotic behaviour of this sequence? It seems likely that \(a_n = n + o(n)\).
theorem erdos_423 :
∀ a : ℕ → ℕ, IsHofstadterSeq a →
(fun n : ℕ => (a n : ℝ) - n) =o[atTop] (fun n : ℕ => (n : ℝ))
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/423.lean, line 110.
Erdos423.erdos_423.variants.nondecreasing
Solved: stated here without proof.
Bolan and Tang [Ta26] independently proved that \(a_n-n\) is nondecreasing.
theorem erdos_423.variants.nondecreasing :
∀ a : ℕ → ℕ, IsHofstadterSeq a →
∀ n m : ℕ, 1 ≤ n → n ≤ m → a n - n ≤ a m - m
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/423.lean, line 119.
Erdos423.erdos_423.variants.unbounded
Solved: stated here without proof.
Bolan and Tang [Ta26] independently proved that \(a_n-n\to\infty\).
theorem erdos_423.variants.unbounded :
∀ a : ℕ → ℕ, IsHofstadterSeq a →
∀ M : ℕ, ∀ᶠ n in atTop, M + n ≤ a n
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/423.lean, line 128.
Erdos423.erdos_423.variants.infinite_complement
Solved: stated here without proof.
Bolan and Tang [Ta26] independently proved that infinitely many positive integers do not occur in the Hofstadter sequence.
theorem erdos_423.variants.infinite_complement :
∀ a : ℕ → ℕ, IsHofstadterSeq a → Set.Infinite (Set.range a)ᶜ
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/423.lean, line 138.
Erdos423.erdos_423.variants.upper_bound
Solved: stated here without proof.
Tang [Ta26] proved \(a_n \ll n^{1/(c-1)+o(1)}\) whenever every finite convex set \(A\) satisfies \(|A-A|\geq |A|^{c-o(1)}\). Using the bound of Cushman [Cu25] gives \(a_n\ll n^{688/413+o(1)}\).
theorem erdos_423.variants.upper_bound :
∀ a : ℕ → ℕ, IsHofstadterSeq a →
∀ ε > (0 : ℝ), (fun n => (a n : ℝ)) =O[atTop]
(fun n => (n : ℝ) ^ ((688 : ℝ) / 413 + ε))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/423.lean, line 275.
Erdos423.erdos_423.variants.lower_bound
Solved: stated here without proof.
Tang [Ta26] proved the lower bound \(a_n=n+\Omega(\log\log n)\).
theorem erdos_423.variants.lower_bound :
∀ a : ℕ → ℕ, IsHofstadterSeq a →
(fun n : ℕ => Real.log (Real.log n)) =O[atTop]
(fun n : ℕ => (a n : ℝ) - n)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/423.lean, line 285.
Sources
TheoremErdős Problem 424: Sequence generated by \(a_i a_j - 1\)#
References: - erdosproblems.com/424 - A5244 - Ben Green's Open Problem 63 - [Ko26] Korsky, S., A problem of Erdős on the sequence \(a_ia_j - 1\), arXiv:2608.07910
Quoted from FormalConjectures/ErdosProblems/424.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/424.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos424.erdos_424
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos424.lean#L6409.
Let \(a_1 = 2\) and \(a_2 = 3\) and continue the sequence by appending to \(a_1, \ldots, a_n\) all possible values of \(a_i a_j - 1\) with \(i \neq j\). Is it true that the set of integers which eventually appear has positive density?
As explained on erdosproblems.com/424, "positive density" here means positive lower density: is there \(c > 0\) such that for all large \(x\) at least \(cx\) of the integers in \([1, x]\) appear? See
erdos_424.variants.exact_densityfor the literal reading.The answer is yes: Korsky [Ko26] (with ChatGPT 5.6 Pro) proved that the set has positive lower density. The linked formal proof (Alexeev and Codex) shows that there is
c > 0withc * x ≤ #{n ∈ [1, x] | n ∈ generatedSet}for all largex, which givesc / 2 ≤ generatedSet.lowerDensity.
theorem erdos_424 : 0 < generatedSet.lowerDensity
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/424.lean, line 73.
Erdos424.erdos_424.variants.exact_density
Open: stated without proof.
A literal interpretation of "positive density": the natural density of
generatedSetexists (i.e. the lower and upper density agree) and is positive.
theorem erdos_424.variants.exact_density : generatedSet.HasPosDensity
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/424.lean, line 81.
Sources
TheoremErdős Problem 425#
Reference: Erdős Problem 425
Quoted from FormalConjectures/ErdosProblems/425.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/425.
The file states 2 research or textbook statements: 2 open. It also has 1 test statement, counted here but not shown.
Erdos425.erdos_425.parts.i
Open: stated without proof.
Let \(F(n)\) be the maximum size of a subset of \(\{1,\ldots,n\}\) with distinct pairwise products. Is there a constant \(c > 0\) such that
\[F(n) = \pi(n) + (c + o(1)) n^{3/4}(\log n)^{-3/2}?\]
theorem erdos_425.parts.i : ∃ c : ℝ, 0 < c ∧
Tendsto
(fun n : ℕ =>
((pairProductExtremal n : ℝ) - (Nat.primeCounting n : ℝ)) /
((n : ℝ) ^ ((3 : ℝ) / 4) * (Real.log n) ^ (-(3 : ℝ) / 2)))
atTop (𝓝 c)
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/425.lean, line 92.
Erdos425.erdos_425.parts.ii
Open: stated without proof.
If all products of \(r\) distinct elements of \(A \subseteq \{1,\ldots,n\}\) are distinct, must
\[|A| \leq \pi(n) + O\bigl(n^{(r+1)/(2r)}\bigr)?\]
theorem erdos_425.parts.ii : ∀ r : ℕ, 1 ≤ r → ∃ C : ℝ, 0 < C ∧
∀ᶠ n in atTop, ∀ A : Finset ℕ, A ⊆ Finset.Icc 1 n → RProductsDistinct r A →
(A.card : ℝ) ≤ (Nat.primeCounting n : ℝ) +
C * (n : ℝ) ^ (((r : ℝ) + 1) / (2 * r))
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/425.lean, line 104.
Sources
TheoremErdős Problem 426#
References: - erdosproblems.com/426 - [Er76b] Erdős, P., Problems and results in graph theory and combinatorial analysis. Proceedings of the Fifth British Combinatorial Conference (1976), 169-192. - [EnEr72] Entringer, R. C. and Erdős, Paul, On the number of unique subgraphs of a graph. J. Combinatorial Theory Ser. B (1972), 112-115. - [HaSc73] Harary, Frank and Schwenk, Allen J., On the number of unique subgraphs. J. Combinatorial Theory Ser. B (1973), 156-160. - [Br75] Brouwer, A. E., Note: "On the number of unique subgraphs of a graph" (J. Combinatorial Theory Ser. B 13 (1972), 112-115) by R. C. Entringer and P. Erdős. J. Combinatorial Theory Ser. B (1975), 184-185. - [BrCh24] Bradač, D. and Christoph, M., Unique subgraphs are rare. arXiv:2410.16233 (2024).
Quoted from FormalConjectures/ErdosProblems/426.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/426.
The file states 1 research or textbook statement: 1 solved. It also has 1 test statement, counted here but not shown.
Erdos426.erdos_426
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/68da20b96673899166e94638f5a7fffeb7231d35/src/latest/ErdosProblems/Erdos426.lean.
We say \(H\) is a unique subgraph of \(G\) if there is exactly one way to find \(H\) as a subgraph (not necessarily induced) of \(G\). Is there a graph on \(n\) vertices with
\[\gg \frac{2^{\binom{n}{2}}}{n!}\]many distinct unique subgraphs?
Bradač and Christoph [BrCh24] have proved the answer is no: if \(f(n)\) is the maximum number of unique subgraphs in a graph on \(n\) vertices then
\[f(n) = o\left(\frac{2^{\binom{n}{2}}}{n!}\right).\]The \(\gg\) below is read as: some constant \(c>0\) works for arbitrarily large \(n\). The negation of the proposition on the right is then exactly \(f(n) = o(2^{\binom{n}{2}}/n!)\), the form in which Bradač and Christoph [BrCh24] resolved the problem.
The linked file states the resolution in that negated form, as
Tendsto fSeq atTop (nhds 0). It counts the isomorphism classes occurring as unique subgraphs, whereasuniqueSubgraphCountcounts their representatives \(G\leq H\); uniqueness forces exactly one representative per class, so the two counts agree.
theorem erdos_426 :
¬ ∃ c : ℝ, 0 < c ∧ ∃ᶠ (n : ℕ) in atTop, ∃ H : SimpleGraph (Fin n),
c * ((2 : ℝ) ^ n.choose 2 / n.factorial) ≤ (uniqueSubgraphCount H : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/426.lean, line 72.
Sources
TheoremErdős Problem 427#
Reference: erdosproblems.com/427
Quoted from FormalConjectures/ErdosProblems/427.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/427.
The file states 3 research or textbook statements: 3 solved.
Erdos427.erdos_427.variants.shiu
Solved: stated here without proof.
Shiu's theorem: for any \(k \geq 1\) and \((a, q) = 1\) there exist infinitely many \(k\)-tuples of consecutive primes \(p_m, \dots, p_{m + k - 1}\) all of which are congruent to \(a\) modulo \(q\).
This is stated ahead of
erdos_427because the formal proof linked there assumes it, and theassumingclause must name a declaration that already exists.[Sh00] Shiu, D. K. L., Strings of congruent primes. J. London Math. Soc. (2) (2000), 359-373.
theorem erdos_427.variants.shiu : ShiuTheorem
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/427.lean, line 64.
Erdos427.erdos_427
Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/main/problems/427/Erdos427.lean.
Erdős Problem 427: is it true that, for every \(n\) and \(d\), there exists \(k\) such that
\[ d \mid p_{n + 1} + \cdots + p_{n + k}, \]where \(p_r\) denotes the \(r\)th prime?
theorem erdos_427 : erdos427
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/427.lean, line 79.
Erdos427.erdos_427.variants.of_shiu
Solved: stated here without proof.
Cedric Pilatte has observed that a positive solution to Erdős Problem 427 follows from Shiu's theorem.
theorem erdos_427.variants.of_shiu (H : ShiuTheorem) : erdos427
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/427.lean, line 87.
Sources
TheoremErdős Problem 428#
Reference: erdosproblems.com/428
Quoted from FormalConjectures/ErdosProblems/428.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/428.
The file states 1 research or textbook statement: 1 open.
Erdos428.erdos_428
Open: stated without proof.
Is there a set \(A\subseteq \mathbb{N}\) such that, for infinitely many \(n\), all of \(n-a\) are prime for all \(a\in A\) with \(0 < a < n\) and
\[\liminf\frac{\lvert A\cap [1,x]\rvert}{\pi(x)}>0?\]
theorem erdos_428 :
∃ A : Set ℕ,
(∃ᶠ n in atTop, ∀ a ∈ A, 0 < a → a < n → (n - a).Prime) ∧
liminf (fun n ↦ primeDensityRatio A n) atTop > 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/428.lean, line 43.
Sources
TheoremErdős Problem 429#
References: - erdosproblems.com/429 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [We24] D. Weisenberg, Sparse Admissible Sets and a Problem of Erdős and Graham. Integers (2024).
Quoted from FormalConjectures/ErdosProblems/429.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/429.
The file states 1 research or textbook statement: 1 solved.
Erdos429.erdos_429
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos429.lean.
Is it true that, if \(A\subseteq \mathbb{N}\) is sparse enough and does not cover all residue classes modulo \(p\) for any prime \(p\), then there exists some \(n\in \mathbb{Z}\) such that \(n+a\) is prime for all \(a\in A\)?
Weisenberg [We24] has shown the answer is no: \(A\) can be arbitrarily sparse and missing at least one residue class modulo every prime \(p\), and yet \(A+n\) is not contained in the primes for any \(n\in \mathbb{Z}\). (Weisenberg gives several constructions of such an \(A\).)
theorem erdos_429 :
¬ ∃ f : ℕ → ℕ, Tendsto f atTop atTop ∧
∀ A : Set ℕ, A.Infinite → (∀ N, (A ∩ Set.Icc 1 N).ncard ≤ f N) →
(∀ p : ℕ, p.Prime → ∃ b : ZMod p, ∀ a ∈ A, (a : ZMod p) ≠ b) →
∃ n : ℤ, ∀ a ∈ A, (n + a).toNat.Prime
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/429.lean, line 50.
Sources
TheoremErdős Problem 430#
References: - erdosproblems.com/430 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
The question is equivalent to the first part of Erdős Problem 385 (an observation of Sarosh Adenwalla recorded on both problem pages).
Quoted from FormalConjectures/ErdosProblems/430.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/430.
The file states 1 research or textbook statement: 1 open. It also has 1 test statement and 1 API statement, counted here but not shown.
Erdos430.erdos_430
Open: stated without proof.
Fix some integer \(n\) and define a decreasing sequence in \([1,n)\) by \(a_1=n-1\) and, for \(k\geq 2\), letting \(a_k\) be the greatest integer in \([1,a_{k-1})\) such that all of the prime factors of \(a_k\) are \(>n-a_k\).
Is it true that, for sufficiently large \(n\), not all of this sequence can be prime?
theorem erdos_430 : ∀ᶠ n in atTop, ¬ ∀ m ∈ terms n, m.Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/430.lean, line 74.
Sources
TheoremErdős Problem 431#
References: - erdosproblems.com/431 - [OAI26a] OpenAI, The additive indecomposability of the primes. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/the-additive-indecomposability-of-the-primes-September-24-2026/paper.pdf
Quoted from FormalConjectures/ErdosProblems/431.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/431.
The file states 2 research or textbook statements: 2 solved.
Erdos431.erdos_431
Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/Ostmann/Complete.lean#L16.
Are there two infinite sets \(A\) and \(B\) such that \(A+B\) agrees with the primes up to finitely many exceptions?
This was disproved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.
theorem erdos_431 :
¬ ∃ A B : Set ℕ, A.Infinite ∧ B.Infinite ∧
(A + B : Set ℕ) =ᶠ[Filter.cofinite] {n | n.Prime}
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/431.lean, line 46.
Erdos431.erdos_431.variants.ostmann
Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/Ostmann/Result.lean#L14.
Ostmann's inverse Goldbach conjecture: if \(A\) and \(B\) each have at least two elements, then \(A+B\) differs from the primes in infinitely many elements.
This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.
theorem erdos_431.variants.ostmann :
∀ A B : Set ℕ, A.Nontrivial → B.Nontrivial → ((A + B) ∆ {n | n.Prime}).Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/431.lean, line 59.
Sources
TheoremErdős Problem 433#
References: - Erdős Problem 433 - P. Erdős and R. L. Graham, On a linear Diophantine problem of Frobenius, Acta Arithmetica 21 (1972), 399–408. - J. Dixmier, Proof of a conjecture by Erdős and Graham on Frobenius' coin problem, Proceedings of the AMS 109 (1990), 567–577.
Quoted from FormalConjectures/ErdosProblems/433.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/433.
The file states 1 research or textbook statement: 1 solved.
Erdos433.erdos_433
Solved: stated here without proof.
For every fixed \(k \geq 2\), Erdős and Graham conjectured that
\[g(k,n) \sim \frac{n^2}{k-1}.\]The conjecture was proved by Dixmier [Di90].
theorem erdos_433 : ∀ k, 2 ≤ k →
Tendsto (fun n : ℕ => (g k n : ℝ) / ((n : ℝ) ^ 2 / ((k : ℝ) - 1))) atTop (𝓝 1)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/433.lean, line 53.
Sources
TheoremErdős Problem 434#
References: - erdosproblems.com/434 - [Ki02] Kiss, G., On the extremal Frobenius problem in a new aspect. Ann. Univ. Sci. Budapest. Eötvös Sect. Math. (2002), 139–142.
Quoted from FormalConjectures/ErdosProblems/434.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/434.
The file states 2 research or textbook statements: 2 solved.
Erdos434.erdos_434.parts.i
Solved: stated here; a Lean proof is at https://www.erdosproblems.com/forum/thread/434#post-4437.
Let \(k \le n\). What choice of \(A\subseteq\{1, \dots, n\}\) (with \(\text{gcd}(A) = 1\)) of size \(|A| = k\) maximises the number of integers not representable as the sum of finitely many elements from \(A\) (with repetitions allowed)? Is it \(\{n, n - 1, \dots, n - k + 1\}\)?
The maximal choice is indeed \(\{n, \dots, n - k + 1\}\), as proved by Kiss [Ki02].
The Lean theorem assumes \(2 \le k\). When \(k = 1 < n\), the proposed singleton \(\{n\}\) does not have gcd \(1\); the gcd condition instead forces the unique admissible choice \(A = \{1\}\).
theorem erdos_434.parts.i (n k : ℕ) (hn : 1 ≤ n) (hk : 2 ≤ k) (h : k ≤ n) :
IsGreatest
{ Nat.NcardUnrepresentable S | (S : Finset ℕ) (_ : S ⊆ Finset.Icc 1 n)
(_ : #S = k) (_ : S.gcd id = 1) }
(Nat.NcardUnrepresentable <| erdos_434.parts.i.answer n k)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/434.lean, line 65.
Erdos434.erdos_434.parts.ii
Solved: stated here; a Lean proof is at https://www.erdosproblems.com/forum/thread/434#post-4437.
For \(2 \le k \le n\), the interval \(A = \{n, n - 1, \dots, n - k + 1\}\) maximises the number of integers not representable as the sum of finitely many elements from \(A\) (with repetitions allowed), as proved by Kiss [Ki02].
theorem erdos_434.parts.ii : ∀ᵉ (n ≥ 1) (k ≥ 2), k ≤ n →
IsGreatest
{ Nat.NcardUnrepresentable S | (S : Finset ℕ) (_ : S ⊆ Finset.Icc 1 n)
(_ : #S = k) (_ : S.gcd id = 1)}
(Nat.NcardUnrepresentable <| Set.Icc (n - k + 1 : ℕ) n)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/434.lean, line 79.
Sources
TheoremErdős Problem 435#
References: - erdosproblems.com/435 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [HwSo24] W. Hwang and K. Song, The Frobenius problem for Numerical Semigroups generated by binomial coefficients. arXiv:2412.17882 (2024).
Quoted from FormalConjectures/ErdosProblems/435.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/435.
The file states 1 research or textbook statement: 1 solved.
Erdos435.erdos_435
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos435.lean.
Let \(n\in\mathbb{N}\) with \(n\neq p^k\) for any prime \(p\) and \(k\geq 0\). What is the largest integer not of the form
\[\sum_{1\leq i\lt n}c_i\binom{n}{i}\]where the \(c_i\geq 0\) are integers?
If \(n=\prod p_k^{a_k}\) then the largest integer not of this form is
\[\sum_k \left( \sum_{1\leq d\leq a_k}\binom{n}{p_k^d}\right)(p_k-1)-n.\]This was first proved by Hwang and Song [HwSo24]. Independently this was found in the comment section by Peake and Cambie.
theorem erdos_435 (n : ℕ) (hn : n ≠ 0)
(hpk : ∀ p k : ℕ, p.Prime → n ≠ p ^ k) :
IsGreatest
{m : ℤ | ¬ ∃ c : ℕ → ℕ, m = ∑ i ∈ Finset.Ico 1 n, (c i : ℤ) * (n.choose i : ℤ)}
((∑ p ∈ n.primeFactors,
(∑ d ∈ Finset.Icc 1 (n.factorization p), (n.choose (p ^ d) : ℤ)) * ((p : ℤ) - 1)) - n)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/435.lean, line 48.
Sources
TheoremErdős Problem 436#
References: - erdosproblems.com/436 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [LeLe62] Lehmer, D. H. and Lehmer, Emma, On runs of residues. Proc. Amer. Math. Soc. (1962), 102-106. - [LLMS62] Lehmer, D. H. and Lehmer, E. and Mills, W. H. and Selfridge, J. L., Machine proof of a theorem on cubic residues. Math. Comp. (1962), 407-415. - [BiMi63] Bierstedt, R. G. and Mills, W. H., On the bound for a pair of consecutive quartic residues of a prime. Proc. Amer. Math. Soc. (1963), 628-632. - [LLM63] Lehmer, D. H. and Lehmer, Emma and Mills, W. H., Pairs of consecutive power residues. Canadian J. Math. (1963), 172-177. - [BLL64] Brillhart, John and Lehmer, D. H. and Lehmer, Emma, Bounds for pairs of consecutive seventh and higher power residues. Math. Comp. (1964), 397-407. - [Gr64g] Graham, R. L., On quadruples of consecutive \(k\)th power residues. Proc. Amer. Math. Soc. (1964), 196-197. - [Du65] Dunton, M., Bounds for pairs of cubic residues. Proc. Amer. Math. Soc. (1965), 330-332. - [Hi91] Hildebrand, Adolf, On consecutive \(k\)th power residues. II. Michigan Math. J. (1991), 241-253.
Quoted from FormalConjectures/ErdosProblems/436.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/436.
The file states 11 research or textbook statements: 1 open and 10 solved. It also has 1 test statement, counted here but not shown.
Erdos436.erdos_436.parts.i
Solved: stated here without proof.
If \(p\) is a prime and \(k, m \geq 2\), let \(r(k, m, p)\) be the minimal \(r\) such that \(r, r + 1, \ldots, r + m - 1\) are all \(k\)th power residues modulo \(p\), and let \(\Lambda(k, m) = \limsup_{p \to \infty} r(k, m, p)\). Is \(\Lambda(k, 2)\) finite for all \(k\)?
A question of Lehmer and Lehmer [LeLe62]. Hildebrand [Hi91] proved that \(\Lambda(k, 2)\) is finite for all \(k \geq 2\).
theorem erdos_436.parts.i : ∀ k ≥ 2, Λ k 2 < ⊤
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/436.lean, line 77.
Erdos436.erdos_436.parts.ii
Open: stated without proof.
Is \(\Lambda(k, 3)\) finite for all odd \(k\)?
Lehmer, Lehmer, Mills and Selfridge [LLMS62] proved \(\Lambda(3, 3) = 23532\). The question is open for odd \(k \geq 5\).
theorem erdos_436.parts.ii : ∀ k ≥ 3, Odd k → Λ k 3 < ⊤
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/436.lean, line 87.
Erdos436.erdos_436.variants.two_two
Solved: stated here without proof.
Lehmer and Lehmer [LeLe62] proved \(\Lambda(2, 2) = 9\).
theorem erdos_436.variants.two_two : Λ 2 2 = 9
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/436.lean, line 92.
Erdos436.erdos_436.variants.three_two
Solved: stated here without proof.
Dunton [Du65] proved \(\Lambda(3, 2) = 77\).
theorem erdos_436.variants.three_two : Λ 3 2 = 77
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/436.lean, line 97.
Erdos436.erdos_436.variants.four_two
Solved: stated here without proof.
Bierstedt and Mills [BiMi63] proved \(\Lambda(4, 2) = 1224\).
theorem erdos_436.variants.four_two : Λ 4 2 = 1224
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/436.lean, line 102.
Erdos436.erdos_436.variants.five_two
Solved: stated here without proof.
Lehmer, Lehmer and Mills [LLM63] proved \(\Lambda(5, 2) = 7888\).
theorem erdos_436.variants.five_two : Λ 5 2 = 7888
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/436.lean, line 107.
Erdos436.erdos_436.variants.six_two
Solved: stated here without proof.
Lehmer, Lehmer and Mills [LLM63] proved \(\Lambda(6, 2) = 202124\).
theorem erdos_436.variants.six_two : Λ 6 2 = 202124
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/436.lean, line 112.
Erdos436.erdos_436.variants.seven_two
Solved: stated here without proof.
Brillhart, Lehmer and Lehmer [BLL64] proved \(\Lambda(7, 2) = 1649375\).
theorem erdos_436.variants.seven_two : Λ 7 2 = 1649375
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/436.lean, line 117.
Erdos436.erdos_436.variants.three_three
Solved: stated here without proof.
Lehmer, Lehmer, Mills and Selfridge [LLMS62] proved \(\Lambda(3, 3) = 23532\).
theorem erdos_436.variants.three_three : Λ 3 3 = 23532
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/436.lean, line 122.
Erdos436.erdos_436.variants.even_three
Solved: stated here without proof.
Lehmer and Lehmer [LeLe62] proved \(\Lambda(k, 3) = \infty\) for all even \(k\).
theorem erdos_436.variants.even_three : ∀ k ≥ 2, Even k → Λ k 3 = ⊤
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/436.lean, line 127.
Erdos436.erdos_436.variants.ge_four
Solved: stated here without proof.
Graham [Gr64g] proved \(\Lambda(k, l) = \infty\) for all \(k \geq 2\) and \(l \geq 4\).
theorem erdos_436.variants.ge_four : ∀ k ≥ 2, ∀ l ≥ 4, Λ k l = ⊤
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/436.lean, line 132.
Sources
TheoremErdős Problem 437#
References: - erdosproblems.com/437 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [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. - [Ta24] Tao, Terence, A result of Bui–Pratt–Zaharescu, and Erdős problem #437. Blog post (2024).
Quoted from FormalConjectures/ErdosProblems/437.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/437.
The file states 3 research or textbook statements: 3 solved.
Erdos437.erdos_437
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos437.lean#L746.
Let \(1\leq a_1\lt \cdots\lt a_k\leq x\). How many of the partial products \(a_1,a_1a_2,\ldots,a_1\cdots a_k\) can be squares? Is it true that, for any \(\epsilon>0\), there can be more than \(x^{1-\epsilon}\) squares?
The answer is yes, which follows from work of Bui, Pratt, and Zaharescu [BPZ24], as noted by Tao [Ta24].
theorem erdos_437 :
∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℕ in atTop, (x : ℝ) ^ (1 - ε) < L x
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/437.lean, line 62.
Erdos437.erdos_437.variants.little_o
Solved: stated here without proof.
Erdős and Graham write it is 'trivial' that there are \(o(x)\) many such squares, although this is not quite trivial, using Siegel's theorem.
theorem erdos_437.variants.little_o :
(fun x : ℕ ↦ (L x : ℝ)) =o[atTop] fun x : ℕ ↦ (x : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/437.lean, line 71.
Erdos437.erdos_437.variants.tao
Solved: stated here without proof.
Tao [Ta24] shows that, if \(u(x)=(\log x\log\log x)^{1/2}\), then
\[x\exp(-(2^{1/2}+o(1))u(x)) \leq L(x) \leq x\exp(-(2^{-1/2}+o(1))u(x)).\]
theorem erdos_437.variants.tao :
∃ o₁ o₂ : ℕ → ℝ, Tendsto o₁ atTop (nhds 0) ∧ Tendsto o₂ atTop (nhds 0) ∧
∀ᶠ x : ℕ in atTop,
x * exp (-(√2 + o₁ x) * √(log x * log (log x))) ≤ L x ∧
L x ≤ x * exp (-((√2)⁻¹ + o₂ x) * √(log x * log (log x)))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/437.lean, line 80.
Sources
TheoremErdős Problem 438#
References: - erdosproblems.com/438 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [Er80c] Erdős, Paul, Nine little known problems in combinatorial number theory. Normat (1980), 155-164, 180. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [LOS83] Lagarias, J. C. and Odlyzko, A. M. and Shearer, J. B., On the density of sequences of integers the sum of no two of which is a square. II. General sequences. J. Combin. Theory Ser. A (1983), 123-139. - [KLS02] Khalfalah, A. and Lodha, S. and Szemerédi, E., Tight bound for the density of sequence of integers the sum of no two of which is a perfect square. Discrete Math. (2002), 243-255.
Quoted from FormalConjectures/ErdosProblems/438.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/438.
The file states 1 research or textbook statement: 1 solved.
Erdos438.erdos_438
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos438.lean#L46.
How large can \(A \subseteq \{1, \ldots, N\}\) be if \(A + A\) contains no square numbers?
A problem of Erdős [Er80, Er80c, ErGr80]. Taking all integers \(\equiv 1 \pmod 3\) gives \(|A| \ge N/3\), and Massias observed that all integers \(\equiv 1, 5, 9, 13, 14, 17, 21, 25, 26, 29, 30 \pmod{32}\) give \(|A| \ge \frac{11}{32} N\). Lagarias, Odlyzko and Shearer [LOS83] proved that \(11/32\) is sharp for the modular version of the problem, and Khalfalah, Lodha and Szemerédi [KLS02] proved that it is sharp in general: the maximal such \(A\) satisfies \(|A| \le (\frac{11}{32} + o(1)) N\).
theorem erdos_438 :
Tendsto (fun N : ℕ ↦ (extremalSize N : ℝ) / (N : ℝ)) atTop (𝓝 ((11 : ℝ) / 32))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/438.lean, line 69.
Sources
TheoremErdős Problem 440#
References: - erdosproblems.com/440 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [ErSz80] Erdős, Pál and Szemerédi, Endre, Remarks on a problem of the American Mathematical Monthly. Mat. Lapok (1980), 121-124.
Quoted from FormalConjectures/ErdosProblems/440.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/440.
The file states 3 research or textbook statements: 3 solved.
Erdos440.erdos_440.parts.i
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos440.lean#L602.
Let \(A=\{a_1\lt a_2\lt \cdots\}\subseteq \mathbb{N}\) be infinite and let \(A(x)\) count the number of indices for which \(\mathrm{lcm}(a_i,a_{i+1})\leq x\). Is it true that \(A(x) \ll x^{1/2}\)?
The answer is yes: Tao has given a simple proof, and Erdős and Szemerédi [ErSz80] proved the sharp bound \(A(x)\leq (c+o(1))x^{1/2}\) (see
erdos_440.variants.erdos_szemeredi).
theorem erdos_440.parts.i :
∀ a : ℕ → ℕ, StrictMono a → (∀ i, 0 < a i) →
(fun x : ℕ ↦ (count a x : ℝ)) =O[atTop] fun x : ℕ ↦ √x
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/440.lean, line 52.
Erdos440.erdos_440.parts.ii
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos440.lean#L602.
How large can
\[\liminf \frac{A(x)}{x^{1/2}}\]be?
Taking \(A=\mathbb{N}\) shows that \(\liminf A(x)/x^{1/2}=1\) is possible. Erdős and Szemerédi [ErSz80] proved that it is always \(\leq 1\).
theorem erdos_440.parts.ii :
IsGreatest {l : ℝ | ∃ a : ℕ → ℕ, StrictMono a ∧ (∀ i, 0 < a i) ∧
l = liminf (fun x : ℕ ↦ (count a x : ℝ) / √x) atTop} erdos_440.parts.ii.answer
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/440.lean, line 70.
Erdos440.erdos_440.variants.erdos_szemeredi
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos440.lean#L602.
Erdős and Szemerédi [ErSz80] proved that \(A(x)\leq (c+o(1))x^{1/2}\) where
\[c=\sum_{n\geq 1}\frac{1}{n^{1/2}(n+1)}\approx 1.86,\]and that this constant is best possible (this was later rediscovered by van Doorn).
theorem erdos_440.variants.erdos_szemeredi :
IsGreatest {l : ℝ | ∃ a : ℕ → ℕ, StrictMono a ∧ (∀ i, 0 < a i) ∧
l = limsup (fun x : ℕ ↦ (count a x : ℝ) / √x) atTop} erdosSzemerediConstant
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/440.lean, line 87.
Sources
TheoremErdős Problem 441#
References: - erdosproblems.com/441 - [Er51b] P. Erdős, Problem. Mat. Lapok (1951), 233. - [Er65] Erdős, P., Extremal problems in number theory. Proc. Sympos. Pure Math., Vol. VIII (1965), 181-189. - [Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Er98] Erdős, Paul, Some of my new and almost new problems and results in combinatorial number theory. Number theory (Eger, 1996) (1998), 169-180. - [Ch72b] Choi, S. L. G., The largest subset in \([1,n]\) whose integers have pairwise L.C.M. not exceeding \(n\). Mathematika (1972), 221-230. - [Ch98] Chen, Yong-Gao, Sequences with bounded l.c.m. of each pair of terms. Acta Arith. (1998), 71-95. - [DaCh06] Dai, Li-Xia and Chen, Yong-Gao, Sequences with bounded l.c.m. of each pair of terms. II. Acta Arith. (2006), 315-326. - [ChDa07] Chen, Yong-Gao and Dai, Li-Xia, Sequences with bounded l.c.m. of each pair of terms. III. Acta Arith. (2007), 125-133. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.
Quoted from FormalConjectures/ErdosProblems/441.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/441.
The file states 6 research or textbook statements: 6 solved.
Erdos441.erdos_441
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos441.lean#L453.
Let \(N\geq 1\). What is the size of the largest \(A\subset \{1,\ldots,N\}\) such that \([a,b]\leq N\) for all \(a,b\in A\), where \([a,b]\) is the least common multiple of \(a\) and \(b\)?
Is it attained by choosing all integers in \([1,(N/2)^{1/2}]\) together with all even integers in \([(N/2)^{1/2},(2N)^{1/2}]\)?
Let \(g(N)\) denote the size of the largest such \(A\). The construction mentioned proves that \(g(N) \geq \left(\tfrac{9}{8}N\right)^{1/2}+O(1)\). Erdős [Er51b] proved \(g(N) \leq (4N)^{1/2}+O(1)\), which was improved by Choi [Ch72b]. Chen [Ch98] established the asymptotic \(g(N) \sim \left(\tfrac{9}{8}N\right)^{1/2}\). Chen and Dai [DaCh06] proved that
\[g(N)\leq \left(\tfrac{9}{8}N\right)^{1/2}+ O\left(\left(\frac{N}{\log N}\right)^{1/2}\log\log N\right).\]In [ChDa07] the same authors prove that, infinitely often, Erdős' construction is not optimal: if \(B\) is that construction and \(A\) is such that \(\lvert A\rvert=g(N)\) then, for infinitely many \(N\), \(\lvert A\rvert\geq \lvert B\rvert+t-2\), where \(t\geq 0\) is defined such that the \(t\)-fold iterated logarithm of \(N\) is in \([0,1)\). (erdosproblems.com omits the \(-2\); [ChDa07] proves the bound with it.)
This is discussed in problems B26 and E2 of Guy's collection [Gu04].
theorem erdos_441 :
¬ ∀ N : ℕ, 1 ≤ N → g N = (erdosConstruction N).card
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/441.lean, line 91.
Erdos441.erdos_441.variants.chen_dai_infinitely_often
Solved: stated here without proof.
Chen and Dai [ChDa07] proved that, infinitely often, Erdős' construction is not optimal: for infinitely many \(N\), \(g(N) \geq \lvert B\rvert+t-2\), where \(B\) is the construction and \(t\geq 0\) is such that the \(t\)-fold iterated logarithm of \(N\) is in \([0,1)\). (erdosproblems.com omits the \(-2\); [ChDa07] proves the bound with it.)
theorem erdos_441.variants.chen_dai_infinitely_often :
∃ᶠ N : ℕ in atTop, (erdosConstruction N).card + Real.iteratedLog N ≤ g N + 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/441.lean, line 102.
Erdos441.erdos_441.variants.lower_bound
Solved: stated here without proof.
Erdős' construction proves that \(g(N) \geq \left(\tfrac{9}{8}N\right)^{1/2}+O(1)\).
theorem erdos_441.variants.lower_bound :
∃ C : ℝ, ∀ N : ℕ, √(9 / 8 * N) - C ≤ g N
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/441.lean, line 108.
Erdos441.erdos_441.variants.erdos_upper_bound
Solved: stated here without proof.
Erdős [Er51b] proved \(g(N) \leq (4N)^{1/2}+O(1)\).
theorem erdos_441.variants.erdos_upper_bound :
∃ C : ℝ, ∀ N : ℕ, (g N : ℝ) ≤ √(4 * N) + C
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/441.lean, line 114.
Erdos441.erdos_441.variants.chen
Solved: stated here without proof.
Chen [Ch98] established the asymptotic \(g(N) \sim \left(\tfrac{9}{8}N\right)^{1/2}\).
theorem erdos_441.variants.chen :
(fun N : ℕ ↦ (g N : ℝ)) ~[atTop] fun N ↦ √(9 / 8 * N)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/441.lean, line 120.
Erdos441.erdos_441.variants.chen_dai_upper_bound
Solved: stated here without proof.
Chen and Dai [DaCh06] proved that \(g(N)\leq \left(\tfrac{9}{8}N\right)^{1/2}+ O\left(\left(\frac{N}{\log N}\right)^{1/2}\log\log N\right)\).
theorem erdos_441.variants.chen_dai_upper_bound :
(fun N : ℕ ↦ (g N : ℝ) - √(9 / 8 * N)) =O[atTop]
fun N ↦ √(N / Real.log N) * Real.log (Real.log N)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/441.lean, line 130.
Sources
TheoremErdős Problem 442#
Reference: erdosproblems.com/442
Quoted from FormalConjectures/ErdosProblems/442.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/442.
The file states 2 research or textbook statements: 2 solved.
Erdos442.erdos_442
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos442.lean#L995.
Let \(\operatorname{Log} x := \max\{\log x, 1\}\), \(\operatorname{Log}_2x = \operatorname{Log} (\operatorname{Log} x)\), and \(\operatorname{Log}_3x = \operatorname{Log}(\operatorname{Log}(\operatorname{Log} x)).\) Is it true that if \(A\subseteq\mathbb{N}\) is such that
\[ \frac{1}{\operatorname{Log}_2 x} \sum_{n\in A: n\leq x} \frac{1}{n}\to\infty \]then
\[ \left(\sum_{n\in A: n\leq x} \frac{1}{n}\right)^2 \sum_{n, m \in A: n < m \leq x} \frac{1}{\operatorname{lcm}(n, m)}\to\infty \]as \(x\to\infty\)?
Tao [Ta24b] has shown this is false.
[Ta24b] Tao, T., Dense sets of natural numbers with unusually large least common multiples. arXiv:2407.04226 (2024).
Note: the informal and formal statements follow the solution paper https://arxiv.org/pdf/2407.04226
theorem erdos_442 : ¬ ∀ (A : Set ℕ),
Tendsto (fun (x : ℝ) =>
1 / x.maxLogOne.maxLogOne * ∑ n ∈ (A ∩ Icc 1 ⌊x⌋₊ : Set ℕ), (1 : ℝ) / n) atTop atTop →
Tendsto (fun (x : ℝ) => 1 / (∑ n ∈ (A ∩ Icc 1 ⌊x⌋₊ : Set ℕ), (1 : ℝ) / n) ^ 2 *
∑ nm ∈ A.bddProdUpper x, (1 : ℝ) / nm.1.lcm nm.2) atTop atTop
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/442.lean, line 89.
Erdos442.erdos_442.variants.tao
Solved: stated here without proof.
Tao resolved erdos_442 in the negative in Theorem 1 of https://arxiv.org/pdf/2407.04226. The following is a formalisation of that theorem with \(C_0 = 1\).
Let \(\operatorname{Log} x := \max\{\log x, 1\}\), \(\operatorname{Log}_2x = \operatorname{Log} (\operatorname{Log} x)\), and \(\operatorname{Log}_3x = \operatorname{Log}(\operatorname{Log}(\operatorname{Log} x)).\) There exists a set \(A\) of natural numbers such that
\[ \sum_{n\in A: n\leq x} \frac{1}{n} = \exp\left(\left(\left(\frac{1}{2} + o(1)\right)\operatorname{Log}_2^{1/2}x \operatorname{Log}_3x\right)\right) \]and
\[ \sum_{n, m\in A: n, m\leq x} \frac{1}{\operatorname{lcm}(n, m)}\ll\left(\sum_{n\in A: n\leq x} \frac{1}{n}\right)^2 \]
theorem erdos_442.variants.tao :
∃ (A : Set ℕ) (f : ℝ → ℝ) (C: ℝ) (hC : 0 < C) (hf : f =o[atTop] (1 : ℝ → ℝ)),
∀ᶠ (x : ℝ) in atTop,
∑ n ∈ (A ∩ Icc 1 ⌊x⌋₊ : Set ℕ), (1 : ℝ) / n =
Real.exp ((1 / 2 + f x) * √x.maxLogOne.maxLogOne * x.maxLogOne.maxLogOne.maxLogOne) ∧
|∑ nm ∈ ((A ∩ Icc 1 ⌊x⌋₊) ×ˢ (A ∩ Icc 1 ⌊x⌋₊)).toFinset, (1 : ℝ) / nm.1.lcm nm.2| ≤
C * (∑ n ∈ (A ∩ Icc 1 ⌊x⌋₊ : Set ℕ), (1 : ℝ) / n) ^ 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/442.lean, line 114.
Sources
TheoremErdős Problem 443#
References: - erdosproblems.com/443 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [He25] Hegyvári, Norbert, An elementary question of Erdős and Graham. arXiv:2503.24201 (2025).
Quoted from FormalConjectures/ErdosProblems/443.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/443.
The file states 2 research or textbook statements: 2 solved.
Erdos443.erdos_443.parts.i
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos443.lean.
Let \(m,n\geq 1\). What is
\[\# \{ k(m-k) : 1\leq k\leq m/2\} \cap \{ l(n-l) : 1\leq l\leq n/2\}?\]Can it be arbitrarily large?
This was solved independently by Hegyvári [He25] and Cambie (unpublished), who show that if \(m>n\) then the set in question has size
\[\leq m^{O(1/\log\log m)},\]and that for any integer \(s\) there exist infinitely many pairs \((m,n)\) such that the set in question has size \(s\).
theorem erdos_443.parts.i :
∀ s : ℕ, ∃ m n : ℕ, n < m ∧ s ≤ (A n ∩ A m).card
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/443.lean, line 53.
Erdos443.erdos_443.parts.ii
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos443.lean.
Let \(m,n\geq 1\). What is
\[\# \{ k(m-k) : 1\leq k\leq m/2\} \cap \{ l(n-l) : 1\leq l\leq n/2\}?\]Is it \(\leq (mn)^{o(1)}\) for all sufficiently large \(m,n\)?
This was solved independently by Hegyvári [He25] and Cambie (unpublished), who show that if \(m>n\) then the set in question has size
\[\leq m^{O(1/\log\log m)},\]and that for any integer \(s\) there exist infinitely many pairs \((m,n)\) such that the set in question has size \(s\).
theorem erdos_443.parts.ii :
∀ ε : ℝ, 0 < ε → ∃ n₀ : ℕ, ∀ m n : ℕ, n₀ < n → n < m →
((A n ∩ A m).card : ℝ) < ((m : ℝ) * n) ^ ε
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/443.lean, line 70.
Sources
TheoremErdős Problem 444#
References: - erdosproblems.com/444 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [ErSa80] Erdős, P. and Sárközy, A., Some asymptotic formulas on generalized divisor functions. IV. Studia Sci. Math. Hungar. (1980), 467-479.
Quoted from FormalConjectures/ErdosProblems/444.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/444.
The file states 1 research or textbook statement: 1 solved. It also has 2 test statements, counted here but not shown.
Erdos444.erdos_444
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos444.lean#L38.
Let \(A\subseteq\mathbb{N}\) be infinite and \(d_A(n)\) count the number of \(a\in A\) which divide \(n\). Is it true that, for every \(k\),
\[\limsup_{x\to \infty} \frac{\max_{n\lt x}d_A(n)}{\left(\sum_{n\in A\cap[1,x)}\frac{1}{n}\right)^k} =\infty?\]This is asked in [ErGr80, p.88]. The answer is yes, proved by Erdős and Sárközy [ErSa80].
The maximum is over \(1 \le n < x\), since every \(a \in A\) divides \(0\).
theorem erdos_444 : ∀ A : Set ℕ, A.Infinite → ∀ k : ℕ,
atTop.limsup (fun x : ℝ ↦ (((Ico 1 ⌈x⌉₊).sup (divisorCount A) /
(∑ n ∈ Ico 1 ⌈x⌉₊ with n ∈ A, (n : ℝ)⁻¹) ^ k : ℝ) : EReal)) = ⊤
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/444.lean, line 65.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.