Erdős Problem 348 to Erdős Problem 368
TheoremErdős Problem 348#
References: - erdosproblems.com/348 - [Ge26] Geneson, J., Deletion thresholds and exponential examples for complete sequences. arXiv:2609.25107 (2026).
Quoted from FormalConjectures/ErdosProblems/348.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/348.
The file states 1 research or textbook statement: 1 solved.
Erdos348.erdos_348
Solved: stated here without proof.
For what values of \(0 \leq m < n\) is there a complete sequence \(A = \{a_1 \leq a_2 \leq \cdots\}\) of integers such that 1. \(A\) remains complete after removing any \(m\) elements, but 2. \(A\) is not complete after removing any \(n\) elements.
Geneson [Ge26, Theorem 1] proved that the pairs are exactly those with \(m \leq 1\). Completeness allows finitely many exceptions, and deletions remove indexed occurrences.
theorem erdos_348 :
{ (m, n) | (m) (n) (_ : m < n) (a : ℕ → ℕ) (_ : Monotone a)
(_ : ∀ s, s.card = m → IsAddCompleteNatSeq' (Function.updateFinset a s 0))
(_ : ∀ t, t.card = n → ¬IsAddCompleteNatSeq' (Function.updateFinset a t 0)) } =
erdos_348.answer
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/348.lean, line 47.
Sources
TheoremErdős Problem 349#
Reference: erdosproblems.com/349
Quoted from FormalConjectures/ErdosProblems/349.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/349.
The file states 13 research or textbook statements: 4 open, 8 solved and 1 textbook result.
Erdos349.erdos_349
Open: stated without proof.
For what values of \(t,\alpha \in (0,\infty)\) is the sequence \(\lfloor t\alpha^n\rfloor\) complete (that is, all sufficiently large integers are the sum of distinct integers of the form \(\lfloor t\alpha^n\rfloor\))?
theorem erdos_349 :
{(t, α) | 0 < t ∧ 0 < α ∧ IsGoodPair t α} = erdos_349.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/349.lean, line 46.
Erdos349.complete_for_alpha_in_Ioo_one_to_goldenRatio
Open: stated without proof.
It seems likely that the sequence is complete for all for all \(t>0\) and all \(1 < \alpha < \frac{1+\sqrt{5}}{2}\).
theorem complete_for_alpha_in_Ioo_one_to_goldenRatio (t α : ℝ) (ht : 0 < t)
(hα : α ∈ Set.Ioo 1 ((1 + √5) / 2)) : IsGoodPair t α
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/349.lean, line 55.
Erdos349.exists_t_for_k_disjoint_segments
Solved: stated here without proof.
For any \(k\) there exists some \(t_k\in (0,1)\) such that the set of \(\alpha > 0\) such that the sequence \(\lfloor t_k\alpha^n\rfloor\) is complete consists of at least \(k\) disjoint line segments, that is, it has at least \(k\) connected components.
theorem exists_t_for_k_disjoint_segments (k : ℕ) :
∃ t ∈ Ioo 0 1,
let S := {α | 0 < α ∧ IsGoodPair t α}
k ≤ (connectedComponentIn S '' S).encard
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/349.lean, line 65.
Erdos349.erdos_349.variants.floor_3_halves_odd
Open: stated without proof.
Is it true that the terms of the sequence \(\lfloor (3/2)^n\rfloor\) are odd infinitely often and even infinitely often?
theorem erdos_349.variants.floor_3_halves_odd :
{n | Odd ⌊(3/2 : ℝ) ^ n⌋}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/349.lean, line 76.
Erdos349.erdos_349.variants.floor_3_halves_even
Open: stated without proof.
Is it true that the terms of the sequence \(\lfloor (3/2)^n\rfloor\) are even infinitely often?
theorem erdos_349.variants.floor_3_halves_even :
{n | Even ⌊(3/2 : ℝ) ^ n⌋}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/349.lean, line 84.
Erdos349.alpha_gt_two_not_isGoodPair
Solved: stated here; a Lean proof is at https://github.com/cepadugato/formal-conjectures/blob/23c629bc2347864782ce88f957a64d6567b978a1/FormalConjectures/ErdosProblems/349.lean#L87.
For \(\alpha > 2\) and any \(t > 0\), the sequence \(\lfloor t\alpha^n\rfloor\) is not additively complete; equivalently \((t, \alpha)\) is not a "good pair". A partial result on the open Erdős Problem 349: it complements
complete_for_alpha_in_Ioo_one_to_goldenRatio.The proof is recorded via the
formal_proofmechanism rather than written inline, as it exceeds the repository's proof-length guideline.
theorem alpha_gt_two_not_isGoodPair (t α : ℝ) (ht : 0 < t) (hα : 2 < α) : ¬ IsGoodPair t α
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/349.lean, line 98.
Erdos349.alpha_le_one_not_isGoodPair
Solved: stated here; a Lean proof is at https://github.com/cepadugato/formal-conjectures/blob/19e39e33be27d46713a423263d38312fe40c9e78/FormalConjectures/ErdosProblems/349.lean.
For \(0 < \alpha \le 1\) and any \(t > 0\), \((t, \alpha)\) is not a good pair: every term \(\lfloor t\alpha^n\rfloor\) lies in the finite interval \([0, \lfloor t\rfloor]\) (since \(\alpha^n \le 1\)), so every subset sum is bounded by the constant \(\sum_{i \in [0,\lfloor t\rfloor]} i\), and no large integer can be a subset sum. A partial result on the open Erdős Problem 349, complementing the \(2 < \alpha\) and integer-coefficient cases.
theorem alpha_le_one_not_isGoodPair (t α : ℝ) (ht : 0 < t) (hα0 : 0 < α) (hα1 : α ≤ 1) :
¬ IsGoodPair t α
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/349.lean, line 110.
Erdos349.exists_finsetSum_two_pow
Textbook result, stated without proof. A Lean proof is at https://github.com/cepadugato/formal-conjectures/blob/19e39e33be27d46713a423263d38312fe40c9e78/FormalConjectures/ErdosProblems/349.lean#L319.
Binary expansion. Every natural number \(k\) is a sum of distinct powers of two: there is a finite set \(E\) of exponents with \(k = \sum_{i \in E} 2^i\). Proved by strong induction: subtract the largest power \(2^m \le k\), recurse on the remainder. A textbook-level building block for
one_two_isGoodPairbelow; it says nothing aboutIsGoodPairitself.
theorem exists_finsetSum_two_pow (k : ℕ) :
∃ E : Finset ℕ, k = ∑ i ∈ E, 2 ^ i
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/349.lean, line 121.
Erdos349.one_two_isGoodPair
Solved: stated here; a Lean proof is at https://github.com/cepadugato/formal-conjectures/blob/19e39e33be27d46713a423263d38312fe40c9e78/FormalConjectures/ErdosProblems/349.lean.
The pair \((1, 2)\) is good. The powers of two \(\lfloor 1\cdot 2^n\rfloor = 2^n\) form an additively complete set: every \(k \ge 1\) is a finite sum of distinct powers of two.
theorem one_two_isGoodPair : IsGoodPair 1 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/349.lean, line 131.
Erdos349.dyadic_two_isGoodPair
Solved: stated here; a Lean proof is at https://github.com/cepadugato/formal-conjectures/blob/19e39e33be27d46713a423263d38312fe40c9e78/FormalConjectures/ErdosProblems/349.lean.
The dyadic fiber at \(\alpha = 2\). For every \(k\), the pair \((1/2^k, 2)\) is good: the sequence \(\lfloor 2^n / 2^k\rfloor\) is additively complete because at index \(n = m + k\) it equals the exact power \(2^m\), so its range contains all powers of two, which already form an additively complete set. Uses monotonicity
IsAddComplete.mono.
theorem dyadic_two_isGoodPair (k : ℕ) : IsGoodPair (1 / 2 ^ k) 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/349.lean, line 142.
Erdos349.int_coeff_ge_two_not_isGoodPair
Solved: stated here; a Lean proof is at https://github.com/cepadugato/formal-conjectures/blob/19e39e33be27d46713a423263d38312fe40c9e78/FormalConjectures/ErdosProblems/349.lean.
Integer leading coefficient \(t \ge 2\) blocks completeness. For every integer base \(\alpha\), the pair \((t, \alpha)\) with integer \(t \ge 2\) is not good: \(\lfloor t\alpha^n\rfloor = t\alpha^n\) is a multiple of \(t\), so every subset sum is too, but two consecutive large integers cannot both be multiples of \(t\). Generalizes the parity obstruction (\(t = 2\)). A partial result on Erdős Problem 349.
theorem int_coeff_ge_two_not_isGoodPair (t : ℤ) (ht : 2 ≤ t) (α : ℤ) :
¬ IsGoodPair (t : ℝ) (α : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/349.lean, line 154.
Erdos349.integer_isGoodPair_iff
Solved: stated here; a Lean proof is at https://github.com/cepadugato/formal-conjectures/blob/19e39e33be27d46713a423263d38312fe40c9e78/FormalConjectures/ErdosProblems/349.lean.
Erdős Problem 349, complete characterization on positive integer pairs. For integers \(t \ge 1\), \(\alpha \ge 1\), the pair \((t, \alpha)\) is good (i.e. \(\lfloor t\alpha^n\rfloor\) is additively complete) iff \((t, \alpha) = (1, 2)\). Assembles the four partial results: \((1,2)\) is good, \(\alpha \le 1\) fails, \(2 < \alpha\) fails (
alpha_gt_two_not_isGoodPair), and integer \(t \ge 2\) fails.
theorem integer_isGoodPair_iff (t α : ℤ) (ht : 1 ≤ t) (hα : 1 ≤ α) :
IsGoodPair (t : ℝ) (α : ℝ) ↔ t = 1 ∧ α = 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/349.lean, line 167.
Erdos349.three_halves_two_not_isGoodPair
Solved: stated here; a Lean proof is at https://github.com/cepadugato/formal-conjectures/blob/erdos-349-three-halves-fiber-proof/FormalConjectures/ErdosProblems/349.lean.
The pair \((3/2, 2)\) is NOT good. The negative companion of
dyadic_two_isGoodPair: while every dyadic coefficient \(1/2^k\) gives a good pair at \(\alpha = 2\), the non-dyadic rational \(t = 3/2\) does not. The sequence \(\lfloor (3/2)\cdot 2^n\rfloor = 1, 3, 6, 12, 24, \ldots\) is not additively complete because every term but the first \(\lfloor 3/2\rfloor = 1\) is a multiple of \(3\) (namely \(\lfloor (3/2)\cdot 2^{n+1}\rfloor = 3\cdot 2^n\)), so every subset sum is \(\equiv 0\) or \(1 \pmod 3\); the infinitely many integers \(\equiv 2 \pmod 3\) are never reached. A partial result on Erdős Problem 349 in the same divisibility family asint_coeff_ge_two_not_isGoodPair(here the modulus is \(3\)).
theorem three_halves_two_not_isGoodPair : ¬ IsGoodPair (3 / 2) 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/349.lean, line 183.
Sources
TheoremErdős Problem 350#
References: - erdosproblems.com/350 - [BeEr74] Benkoski, S. J. and Erdős, P., On weird and pseudoperfect numbers. Math. Comp. (1974), 617-623. - [HSS77] Hanson, F. and Steele, J. M. and Stenger, F., Distinct sums over subsets. Proc. Amer. Math. Soc. (1977), 179-180.
Quoted from FormalConjectures/ErdosProblems/350.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/350.
The file states 2 research or textbook statements: 2 solved. It also has 2 test statements and 1 API statement, counted here but not shown.
Erdos350.erdos_350
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos350.lean; a Lean proof is at https://github.com/XC0R/formal-conjectures/blob/ba788c9124b563bce98a3413d474b3a2731fd0af/FormalConjectures/ErdosProblems/350.lean#L226.
If
A ⊂ ℕis a finite set of integers all of whose subset sums are distinct then∑ n ∈ A, 1/n < 2. Proved by Ryavec.This was proved by Ryavec, who did not appear to ever publish the proof. Ryavec's proof is reproduced in [BeEr74]. More generally, Ryavec's proof delivers that \(\sum_{n\in A}\frac{1}{n}\leq 2-2^{1-\lvert A\rvert},\) with equality if and only if \(A=\{1,2,\ldots,2^k\}\).
This was formalized in Lean by Alexeev using Aristotle.
theorem erdos_350 (A : Finset ℕ) (hA : DecidableDistinctSubsetSums A) :
∑ n ∈ A, (1 / n : ℝ) < 2
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/350.lean, line 77.
Erdos350.erdos_350.variants.strengthening
Solved: stated here without proof.
If
A ⊂ ℕis a finite set of integers all of whose subset sums are distinct then∑ n ∈ A, 1/n^s < 1/(1 - 2^(-s)), for anys > 0. Proved by Hanson, Steele, and Stenger [HSS77].We exclude here the case
s = 0, because in the informal formulation then the right hand side is to be interpreted as∞, while the left hand side counts the elements inA.
theorem erdos_350.variants.strengthening (A : Finset ℕ) (hA : DecidableDistinctSubsetSums A)
(s : ℝ) (hs : 0 < s) : ∑ n ∈ A, (1 / n : ℝ)^s < 1 / (1 - 2^(-s))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/350.lean, line 88.
Sources
TheoremErdős Problem 351#
Reference: erdosproblems.com/351
Quoted from FormalConjectures/ErdosProblems/351.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/351.
The file states 3 research or textbook statements: 3 solved.
Erdos351.erdos_351
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos351.lean.
Let \(p(x) \in \mathbb{Q}[x]\) be a non-constant rational polynomial with positive leading coefficient. Is it true that
\[A=\{ p(n)+1/n : n \in \mathbb{N}\}\]is strongly complete, in the sense that, for any finite set \(B\),
\[\left\{\sum_{a \in X} a : X \subseteq A \setminus B, X \textrm{ is finite}\right\}\]contains all sufficiently large integers?
theorem erdos_351 :
∀ P : ℚ[X], 0 < P.natDegree → 0 < P.leadingCoeff → HasCompleteImage P
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/351.lean, line 58.
Erdos351.erdos_351.variants.X
Solved: stated here without proof.
Let \(p(x) = x \in \mathbb{Q}[x]\). It has been shown that
\[A=\{ p(n)+1/n : n \in \mathbb{N}\}\]is strongly complete, in the sense that, for any finite set \(B\),
\[\left\{\sum_{a \in X} a : X \subseteq A \setminus B, X \textrm{ is finite}\right\}\]contains all sufficiently large integers.
protected theorem erdos_351.variants.X : HasCompleteImage X
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/351.lean, line 70.
Erdos351.erdos_351.variants.X_sq
Solved: stated here without proof.
Let \(p(x) = x ^ 2 \in \mathbb{Q}[x]\). It has been shown that
\[A=\{ p(n)+1/n : n \in \mathbb{N}\}\]is strongly complete, in the sense that, for any finite set \(B\),
\[\left\{\sum_{a \in X} a : X \subseteq A \setminus B, X \textrm{ is finite}\right\}\]contains all sufficiently large integers.
theorem erdos_351.variants.X_sq : HasCompleteImage (X ^ 2)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/351.lean, line 79.
Sources
TheoremErdős Problem 352#
Reference: erdosproblems.com/352
Quoted from FormalConjectures/ErdosProblems/352.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/352.
The file states 1 research or textbook statement: 1 open.
Erdos352.erdos_352
Open: stated without proof.
Is there some \(c > 0\) such that every measurable \(A \subseteq \mathbb{R}^2\) of measure \(\geq c\) contains the vertices of a triangle of area 1?
theorem erdos_352 :
∃ c > (0: ℝ), ∀ A : Set ℝ², MeasurableSet A → ℙ A ≥ c.toEReal
→ (∃ t : Affine.Triangle ℝ ℝ²,
(∀ p : Fin 3, t.points p ∈ A) ∧
EuclideanGeometry.triangle_area (t.points 0) (t.points 1) (t.points 2) = 1)
Category research open; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/352.lean, line 38.
Sources
TheoremErdős Problem 353#
References: - erdosproblems.com/353 - [Er83d] Erdős, Paul, Some combinatorial, geometric and set theoretic problems in measure theory. Measure Theory, Oberwolfach 1983 (1984), 321-327. - [Ko23] Kovač, V., Coloring and density theorems for configurations of a given volume. arXiv:2309.09973 (2023). - [KoPr24] Kovač, V. and B. Predojević, Polygons of unit area with vertices in sets of infinite planar measure. arXiv:2412.11725 (2024). - [Ko25] J. Koizumi, Isosceles trapezoids of unit area with vertices in sets of infinite planar measure. arXiv:2501.01914 (2025).
Quoted from FormalConjectures/ErdosProblems/353.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/353.
The file states 5 research or textbook statements: 5 solved.
Erdos353.erdos_353
Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/110d489ed5c07e5b216453e092e9113127c98c9a/problems/353/Erdos353.lean.
Let \(A\subseteq \mathbb{R}^2\) be a measurable set with infinite measure. Must \(A\) contain the vertices of an isosceles trapezoid of area \(1\)? What about an isosceles triangle, or a right-angled triangle, or a cyclic quadrilateral, or a convex polygon with congruent sides?
Koizumi [Ko25] has resolved this question, proving that any set with infinite measure must contain the vertices of an isosceles trapezoid, an isosceles triangle, and a right-angled triangle, all of area \(1\).
This statement formalizes the leading question, for isosceles trapezoids; the remaining configurations are given as variants below. The area of a polygon is taken to be the Lebesgue measure of the convex hull of its vertices.
theorem erdos_353 :
∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ →
∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, ∃ d ∈ A,
IsIsoscelesTrapezoid a b c d ∧
volume (convexHull ℝ {a, b, c, d}) = 1
Category research solved; AMS 28 Measure and integration, 51 Geometry. Declared in FormalConjectures/ErdosProblems/353.lean, line 58.
Erdos353.erdos_353.variants.isosceles_triangle
Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/110d489ed5c07e5b216453e092e9113127c98c9a/problems/353/Erdos353.lean.
Every measurable \(A\subseteq \mathbb{R}^2\) with infinite measure contains the vertices of an isosceles triangle of area \(1\).
Koizumi [Ko25] has resolved this question, proving that any set with infinite measure must contain the vertices of an isosceles trapezoid, an isosceles triangle, and a right-angled triangle, all of area \(1\).
Note the area condition forces
a,b,cto be affinely independent, so no separate non-degeneracy hypothesis is needed.
theorem erdos_353.variants.isosceles_triangle :
∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ →
∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A,
IsIsosceles a b c ∧
volume (convexHull ℝ {a, b, c}) = 1
Category research solved; AMS 28 Measure and integration, 51 Geometry. Declared in FormalConjectures/ErdosProblems/353.lean, line 78.
Erdos353.erdos_353.variants.right_angled_triangle
Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/110d489ed5c07e5b216453e092e9113127c98c9a/problems/353/Erdos353.lean.
Every measurable \(A\subseteq \mathbb{R}^2\) with infinite measure contains the vertices of a right-angled triangle of area \(1\).
Koizumi [Ko25] has resolved this question, proving that any set with infinite measure must contain the vertices of an isosceles trapezoid, an isosceles triangle, and a right-angled triangle, all of area \(1\).
Note the area condition forces
a,b,cto be affinely independent, so no separate non-degeneracy hypothesis is needed.
theorem erdos_353.variants.right_angled_triangle :
∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ →
∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A,
IsRightAngled a b c ∧
volume (convexHull ℝ {a, b, c}) = 1
Category research solved; AMS 28 Measure and integration, 51 Geometry. Declared in FormalConjectures/ErdosProblems/353.lean, line 98.
Erdos353.erdos_353.variants.cyclic_quadrilateral
Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/110d489ed5c07e5b216453e092e9113127c98c9a/problems/353/Erdos353.lean.
Every measurable \(A\subseteq \mathbb{R}^2\) with infinite measure contains the vertices of a cyclic quadrilateral of area \(1\).
Kovač and Predojević [KoPr24] have proved that this is true for cyclic quadrilaterals - that is, every set with infinite measure contains four distinct points on a circle such that the quadrilateral determined by these four points has area \(1\). The quadrilateral determined by four distinct concyclic points is their convex hull.
theorem erdos_353.variants.cyclic_quadrilateral :
∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ →
∃ Q : Set ℝ², Q ⊆ A ∧ Q.ncard = 4 ∧ Cospherical Q ∧
volume (convexHull ℝ Q) = 1
Category research solved; AMS 28 Measure and integration, 51 Geometry. Declared in FormalConjectures/ErdosProblems/353.lean, line 116.
Erdos353.erdos_353.variants.congruent_sides
Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/110d489ed5c07e5b216453e092e9113127c98c9a/problems/353/Erdos353.lean.
The answer is negative for convex polygons with congruent sides: Kovač and Predojević [KoPr24] prove that there exists a set of infinite measure such that every convex polygon with congruent sides and all vertices in the set has area \(<1\).
theorem erdos_353.variants.congruent_sides :
∃ A : Set ℝ², MeasurableSet A ∧ volume A = ⊤ ∧
∀ (n : ℕ) (v : Fin (n + 3) → ℝ²),
IsCcwConvexPolygon v → (∀ i, v i ∈ A) →
(∀ i, dist (v i) (v (i + 1)) = dist (v 0) (v 1)) →
volume (convexHull ℝ (Set.range v)) < 1
Category research solved; AMS 28 Measure and integration, 51 Geometry. Declared in FormalConjectures/ErdosProblems/353.lean, line 129.
Sources
TheoremErdős Problem 354#
References: - erdosproblems.com/354 - [YC26] Yingzhe Yu and Kani Chen, Erdős Problem 354(i): Strong Completeness of Two Dyadic Floor Sequences (2026). Manuscript
Quoted from FormalConjectures/ErdosProblems/354.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/354.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos354.erdos_354.parts.i
Solved: stated here; a Lean proof is at https://github.com/Andrewyzzz/erdos354/blob/c735d9389a79a2aa20fc04103d8890dd330b531e/formalization/Dyadic354/UpstreamBridge.lean#L34.
Let \(\alpha,\beta\in \mathbb{R}_{>0}\) such that \(\alpha/\beta\) is irrational. Is the multiset
\[\{ \lfloor \alpha\rfloor,\lfloor 2\alpha\rfloor,\lfloor 4\alpha\rfloor,\ldots\}\cup \{ \lfloor \beta\rfloor,\lfloor 2\beta\rfloor,\lfloor 4\beta\rfloor,\ldots\}\]complete?
Yu and Chen [YC26] prove an affirmative answer. They also prove that the set of nonzero values remains complete after deletion of any finite set of values.
theorem erdos_354.parts.i : ∀ᵉ (α > 0) (β > 0), Irrational (α / β) →
IsAddCompleteNatSeq' (FloorMultiples.interleave α β 2)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/354.lean, line 53.
Erdos354.erdos_354.parts.ii
Open: stated without proof.
Let \(\alpha,\beta\in \mathbb{R}_{>0}\) such that \(\alpha/\beta\) is irrational. Is
\[\{ \lfloor \alpha\rfloor,\lfloor \gamma\alpha\rfloor,\lfloor \gamma^2\alpha\rfloor,\ldots\}\cup \{ \lfloor \beta\rfloor,\lfloor \gamma\beta\rfloor,\lfloor \gamma^2\beta\rfloor,\ldots\}\]complete?
theorem erdos_354.parts.ii : ∃ γ ∈ Set.Ioo (1 : ℝ) 2, ∀ᵉ (α > 0) (β > 0), Irrational (α / β) →
IsAddCompleteNatSeq' (FloorMultiples.interleave α β γ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/354.lean, line 61.
Sources
TheoremErdős Problem 355#
References: - erdosproblems.com/355 - [DoKo25] W. van Doorn and V. Kovač, Lacunary sequences whose reciprocal sums represent all rationals in an interval. arXiv:2509.24971 (2025).
Quoted from FormalConjectures/ErdosProblems/355.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/355.
The file states 1 research or textbook statement: 1 solved.
Erdos355.erdos_355
Solved: stated here; a Lean proof is at https://github.com/Woett/Lean-files/blob/main/ErdosProblem355.lean.
Is there a lacunary sequence \(A\subseteq \mathbb{N}\) (so that \(A=\{a_1 < \cdots\}\) and there exists some \(\lambda > 1\) such that \(a_{n+1}/a_n\geq \lambda\) for all \(n\geq 1\)) such that
\[\left\{ \sum_{a\in A'}\frac{1}{a} : A'\subseteq A\textrm{ finite}\right\}\]contain all rationals in some open interval?
Bleicher and Erdős conjectured the answer is no.
In fact the answer is yes, with any lacunarity constant \(\lambda\in (1,2)\) (though not \(\lambda=2\)), as proved by van Doorn and Kova\v{c} [DoKo25].
This was formalized in Lean by van Doorn using Aristotle.
theorem erdos_355 :
∃ A : ℕ → ℕ, IsLacunary A ∧ ∃ u v : ℝ, u < v ∧ ∀ q : ℚ, ↑q ∈ Set.Ioo u v →
q ∈ {∑ a ∈ A', (1 / a : ℚ) | (A' : Finset ℕ) (_ : ↑A' ⊆ Set.range A)}
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/355.lean, line 49.
Sources
TheoremErdős Problem 357#
References: - erdosproblems.com/357 - [He86] Hegyvári, Norbert, On consecutive sums in sequences. Acta Math. Hungar. (1986), 193--200.
Quoted from FormalConjectures/ErdosProblems/357.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/357.
The file states 17 research or textbook statements: 14 open and 3 solved.
Erdos357.erdos_357.parts.i
Open: stated without proof.
Let \(f(n)\) be the maximal \(k\) such that there exist integers \(1 \le a_1 < \dotsc < a_k \le n\) such that all sums of the shape \(\sum_{u \le i \le v} a_i\) are distinct. Is \(f(n)=o(n)\)?
theorem erdos_357.parts.i : (fun n ↦ (f n : ℝ)) =o[atTop] (fun n ↦ (n : ℝ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 45.
Erdos357.erdos_357.parts.ii.bigO_version
Open: stated without proof.
Let \(f(n)\) be the maximal \(k\) such that there exist integers \(1 \le a_1 < \dotsc < a_k \le n\) such that all sums of the shape \(\sum_{u \le i \le v} a_i\) are distinct. How does \(f(n)\) grow? Can we find a (good) explicit function \(g\) such that \(g = O(f)\) ?
theorem erdos_357.parts.ii.bigO_version :
erdos_357.parts.ii.bigO_version.answer =O[atTop] (fun n ↦ (f n : ℝ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 65.
Erdos357.erdos_357.parts.ii.bigO_version_symm
Open: stated without proof.
Let \(f(n)\) be the maximal \(k\) such that there exist integers \(1 \le a_1 < \dotsc < a_k \le n\) such that all sums of the shape \(\sum_{u \le i \le v} a_i\) are distinct. How does \(f(n)\) grow? Can we find a (good) explicit function \(g\) such that \(f = O(g)\) ?
theorem erdos_357.parts.ii.bigO_version_symm :
(fun n ↦ (f n : ℝ)) =O[atTop] erdos_357.parts.ii.bigO_version_symm.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 75.
Erdos357.erdos_357.parts.ii.bigTheta_version
Open: stated without proof.
Let \(f(n)\) be the maximal \(k\) such that there exist integers \(1 \le a_1 < \dotsc < a_k \le n\) such that all sums of the shape \(\sum_{u \le i \le v} a_i\) are distinct. How does \(f(n)\) grow? Can we find a (good) explicit function \(g\) such that \(f = \Theta(g)\) ?
theorem erdos_357.parts.ii.bigTheta_version :
(fun n ↦ (f n : ℝ)) =Θ[atTop] erdos_357.parts.ii.bigTheta_version.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 85.
Erdos357.erdos_357.parts.ii.littleO_version
Open: stated without proof.
Let \(f(n)\) be the maximal \(k\) such that there exist integers \(1 \le a_1 < \dotsc < a_k \le n\) such that all sums of the shape \(\sum_{u \le i \le v} a_i\) are distinct. How does \(f(n)\) grow? Can we find a (good) explicit function \(g\) such that \(g = o(f)\) ?
theorem erdos_357.parts.ii.littleO_version :
erdos_357.parts.ii.littleO_version.answer =o[atTop] (fun n ↦ (f n : ℝ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 95.
Erdos357.erdos_357.parts.ii.littleO_version_symm
Open: stated without proof.
Let \(f(n)\) be the maximal \(k\) such that there exist integers \(1 \le a_1 < \dotsc < a_k \le n\) such that all sums of the shape \(\sum_{u \le i \le v} a_i\) are distinct. How does \(f(n)\) grow? Can we find a (good) explicit function \(g\) such that \(f = o(g)\) ?
theorem erdos_357.parts.ii.littleO_version_symm :
(fun n ↦ (f n : ℝ)) =o[atTop] erdos_357.parts.ii.littleO_version_symm.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 105.
Erdos357.erdos_357.variants.weisenberg
Solved: stated here without proof.
Let \(f(n)\) be the maximal \(k\) such that there exist integers \(1 \le a_1 < \dotsc < a_k \le n\) such that all sums of the shape \(\sum_{u \le i \le v} a_i\) are distinct. It is known that \(f(n) \geq (2+o(1))\sqrt{n}\). Source: See comment by Desmond Weisenberg here: https://www.erdosproblems.com/forum/thread/357.
theorem erdos_357.variants.weisenberg : ∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧
∀ᶠ n in atTop, (2 + o n) * √n ≤ f n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 115.
Erdos357.erdos_357.variants.infinite_set_lower_density
Solved: stated here without proof.
Suppose \(A\) is an infinite set such that all finite sums of consecutive terms of \(A\) are distinct. Then \(A\) has lower density 0.
theorem erdos_357.variants.infinite_set_lower_density (A : ℕ → ℕ) (hA : StrictMono A)
(hA : HasDistinctSums A) : (Set.range A).lowerDensity = 0
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 122.
Erdos357.erdos_357.variants.infinite_set_density
Open: stated without proof.
Suppose \(A\) is an infinite set such that all finite sums of consecutive terms of \(A\) are distinct. Then it is conjectured that \(A\) has density 0.
theorem erdos_357.variants.infinite_set_density (A : ℕ → ℕ) (hA : StrictMono A)
(hA : HasDistinctSums A) :
(Set.range A).HasDensity 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 129.
Erdos357.erdos_357.variants.infinite_set_sum
Open: stated without proof.
Suppose \(A\) is an infinite set such that all finite sums of consecutive terms of \(A\) are distinct. Then it is conjectured that the sum \(\sum_k \frac{1}{a_k}\) converges.
theorem erdos_357.variants.infinite_set_sum (A : ℕ → ℕ) (hA : StrictMono A)
(hA : HasDistinctSums A) :
Summable (fun i ↦ (1 : ℝ) / A i)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 138.
Erdos357.erdos_357.variants.hegyvari
Solved: stated here without proof.
Let \(g(n)\) be the maximal \(k\) such that there exist integers \(1 \le a_1, \dotsc, a_k \le n\) such that all sums of the shape \(\sum_{u \le i \le v} a_i\) are distinct. Hegyvári [He86] proved that
\[\left(\frac 1 3 + o(1) \right)n \leq g(n) \leq \left(\frac 2 3 + o(1) \right)n.\]
theorem erdos_357.variants.hegyvari : ∃ (o o' : ℕ → ℝ), o =o[atTop] (1 : ℕ → ℝ) ∧
o' =o[atTop] (1 : ℕ → ℝ) ∧
∀ᶠ n in atTop, (g n : ℝ) ∈ Set.Icc ((1 / 3 + o n) * n) ((2 / 3 + o' n)*n)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 153.
Erdos357.erdos_357.variants.monotone.parts.i
Open: stated without proof.
Let \(h(n)\) be the maximal \(k\) such that there exist integers \(1 \le a_1 \leq \dotsc \leq a_k \le n\) such that all sums of the shape \(\sum_{u \le i \le v} a_i\) are distinct. Is \(h(n)=o(n)\)?
theorem erdos_357.variants.monotone.parts.i : (fun n ↦ (h n : ℝ)) =o[atTop] (fun n ↦ (n : ℝ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 170.
Erdos357.erdos_357.variants.monotone.parts.ii.bigO_version
Open: stated without proof.
Let \(h(n)\) be the maximal \(k\) such that there exist integers \(1 \le a_1 \leq \dotsc \leq a_k \le n\) such that all sums of the shape \(\sum_{u \le i \le v} a_i\) are distinct. How does \(h(n)\) grow? Can we find a (good) explicit function \(g\) such that \(g = O(h)\) ?
theorem erdos_357.variants.monotone.parts.ii.bigO_version :
erdos_357.variants.monotone.parts.ii.bigO_version.answer =O[atTop] (fun n ↦ (h n : ℝ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 179.
Erdos357.erdos_357.variants.monotone.parts.ii.bigO_version_symm
Open: stated without proof.
Let \(h(n)\) be the maximal \(k\) such that there exist integers \(1 \le a_1 \leq \dotsc \leq a_k \le n\) such that all sums of the shape \(\sum_{u \le i \le v} a_i\) are distinct. How does \(h(n)\) grow? Can we find a (good) explicit function \(g\) such that \(h = O(g)\) ?
theorem erdos_357.variants.monotone.parts.ii.bigO_version_symm :
(fun n ↦ (h n : ℝ)) =O[atTop] erdos_357.variants.monotone.parts.ii.bigO_version_symm.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 189.
Erdos357.erdos_357.variants.monotone.parts.ii.bigTheta_version
Open: stated without proof.
Let \(h(n)\) be the maximal \(k\) such that there exist integers \(1 \le a_1 \leq \dotsc \leq a_k \le n\) such that all sums of the shape \(\sum_{u \le i \le v} a_i\) are distinct. How does \(h(n)\) grow? Can we find a (good) explicit function \(g\) such that \(h = \Theta(g)\) ?
theorem erdos_357.variants.monotone.parts.ii.bigTheta_version :
(fun n ↦ (h n : ℝ)) =Θ[atTop] erdos_357.variants.monotone.parts.ii.bigTheta_version.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 200.
Erdos357.erdos_357.variants.monotone.parts.ii.littleO_version
Open: stated without proof.
Let \(h(n)\) be the maximal \(k\) such that there exist integers \(1 \le a_1 \leq \dotsc \leq a_k \le n\) such that all sums of the shape \(\sum_{u \le i \le v} a_i\) are distinct. How does \(h(n)\) grow? Can we find a (good) explicit function \(g\) such that \(g = o(h)\) ?
theorem erdos_357.variants.monotone.parts.ii.littleO_version :
erdos_357.variants.monotone.parts.ii.littleO_version.answer =o[atTop] (fun n ↦ (h n : ℝ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 210.
Erdos357.erdos_357.variants.monotone.parts.ii.littleO_version_symm
Open: stated without proof.
Let \(h(n)\) be the maximal \(k\) such that there exist integers \(1 \le a_1 \leq \dotsc \leq a_k \le n\) such that all sums of the shape \(\sum_{u \le i \le v} a_i\) are distinct. How does \(h(n)\) grow? Can we find a (good) explicit function \(g\) such that \(h = o(g)\) ?
theorem erdos_357.variants.monotone.parts.ii.littleO_version_symm :
(fun n ↦ (h n : ℝ)) =o[atTop] erdos_357.variants.monotone.parts.ii.littleO_version_symm.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/357.lean, line 220.
Sources
TheoremErdős Problem 358#
References: - erdosproblems.com/358 - [Ta26] T. Tao, Erdős problem 358 (2026)
Quoted from FormalConjectures/ErdosProblems/358.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/358.
The file states 6 research or textbook statements: 2 open, 3 solved and 1 textbook result. It also has 1 API statement, counted here but not shown.
Erdos358.f_id
Textbook result, stated without proof.
When \(A_n = n\), the function \(f\) defined above counts the number of odd divisors of \(n\).
theorem f_id : f id = fun n ↦ #{d ∈ n.divisors | Odd d}
Category textbook; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/358.lean, line 66.
Erdos358.erdos_358.parts.i
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1268917deaaaa0d674f651287027baa26cea9920/src/latest/ErdosProblems/Erdos358.lean#L9111.
Let \(A=\{a_1 < \cdots\}\) be an infinite sequence of integers. Let \(f(n)\) count the number of solutions to
\[n=\sum_{u\leq i\leq v}a_i.\]Is there such an \(A\) for which \(f(n)\to \infty\) as \(n\to \infty\)?
Tao [Ta26] constructed such a sequence with \(f(n) \gg \log n\) for all sufficiently large \(n\).
theorem erdos_358.parts.i :
∃ A, StrictMono A ∧ atTop.Tendsto (f A) atTop
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/358.lean, line 78.
Erdos358.erdos_358.parts.ii
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1268917deaaaa0d674f651287027baa26cea9920/src/latest/ErdosProblems/Erdos358.lean#L9115.
Let \(A=\{a_1 < \cdots\}\) be an infinite sequence of integers. Let \(f(n)\) count the number of solutions to
\[n=\sum_{u\leq i\leq v}a_i.\]Is there an \(A\) such that \(f(n)\geq 2\) for all large \(n\)?
This also follows from Tao's construction with \(f(n) \gg \log n\) [Ta26].
theorem erdos_358.parts.ii :
∃ A, StrictMono A ∧ ∀ᶠ n in atTop, 2 ≤ f A n
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/358.lean, line 91.
Erdos358.erdos_358.variants.prime_set
Open: stated without proof.
When \(A =\{a_1 < \cdots\}\) corresponds to the set of primes, it is conjectured that the \(\limsup\) of the number of representations
\[n=\sum_{u\leq i\leq v}a_i\]is infinite.
theorem erdos_358.variants.prime_set :
atTop.limsup (fun n ↦ (f (Nat.nth Nat.Prime) n : ℕ∞)) = ⊤
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/358.lean, line 100.
Erdos358.erdos_358.variants.prime_set_density_representation
Open: stated without proof.
When \(A =\{a_1 < \cdots\}\) corresponds to the set of primes, it is conjectured that the set of numbers \(n\) that have representations
\[n=\sum_{u\leq i\leq v}a_i\]has positive upper density.
theorem erdos_358.variants.prime_set_density_representation :
0 < {n : ℕ | intervalRepresentations (Nat.nth Nat.Prime) n |>.Nonempty}.upperDensity
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/358.lean, line 109.
Erdos358.erdos_358.variants.one_le
Proved here.
In [ErGr80] Erdős and Graham further asked whether there is an \(A\) with \(f(n)\geq 1\) for all large \(n\). Egami observed that this holds trivially for \(a_n=n\), so they may have intended to count only those representations
\[n=\sum_{u\leq i\leq v}a_i\]that use at least two consecutive terms, which is what \(g\) counts.
This follows from Tao's construction [Ta26], which gives \(f(n)\gg\log n\): see
erdos_358.parts.iiandone_le_g_of_two_le_f.
theorem erdos_358.variants.one_le :
∃ A, StrictMono A ∧ ∀ᶠ n in atTop, 1 ≤ g A n
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/358.lean, line 170.
Sources
TheoremErdős Problem 359#
Reference: erdosproblems.com/359
Quoted from FormalConjectures/ErdosProblems/359.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/359.
The file states 3 research or textbook statements: 3 open. It also has 1 test statement, counted here but not shown.
Erdos359.erdos_359.parts.i
Open: stated without proof.
Let $a_1< a_2 < ⋯ $ be an infinite sequence of integers such that \(a_1=1\) and \(a_{i+1}\) is the least integer which is not a sum of consecutive earlier \(a_j\)s. Show that \(a_k / k \to \infty\).
theorem erdos_359.parts.i (A : ℕ → ℕ) (hA : IsGoodFor A 1) :
atTop.Tendsto (fun k ↦ (A k : ℝ) / k) atTop
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/359.lean, line 42.
Erdos359.erdos_359.parts.ii
Open: stated without proof.
Let $a_1< a_2 < ⋯ $ be an infinite sequence of integers such that \(a_1=1\) and \(a_{i+1}\) is the least integer which is not a sum of consecutive earlier \(a_j\)s. Show that \(a_k / k ^ {1 + c} \to 0\) for any \(c > 0\).
theorem erdos_359.parts.ii (A : ℕ → ℕ) (hA : IsGoodFor A 1) (c : ℝ) (hc : 0 < c):
atTop.Tendsto (fun k ↦ A k / (k : ℝ) ^ (1 + c)) (nhds 0)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/359.lean, line 50.
Erdos359.erdos_359.variants.isGoodFor_1_asymptotic
Open: stated without proof.
Suppose monotone sequence \(A\) satisfies the following:
A 0 = 1and for allj,A (j + 1)is the smallest natural number that cannot be written as a sum of consecutive terms ofA 0, ..., A j. Then it is conjectured that\[a_k ~ \frac{k \log k}{\log \log k}\].
theorem erdos_359.variants.isGoodFor_1_asymptotic (A : ℕ → ℕ) (hA : IsGoodFor A 1) :
(fun k ↦ (A k : ℝ)) ~[atTop] (fun k ↦ k * (k : ℝ).log / (k : ℝ).log.log)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/359.lean, line 66.
Sources
TheoremErdős Problem 360#
References: - erdosproblems.com/360 - [AlEr96] Alon, Noga and Erdős, Paul, Sure monochromatic subset sums. Acta Arith. 74 (1996), 269-272. - [CFP21] Conlon, D. and Fox, J. and Pham, H. T., Subset sums, completeness and colorings. arXiv:2104.14766 (2021). - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique (1980). - [Vu07] Vu, Van H., Some new results on subset sums. J. Number Theory 124 (2007), 229-233.
Quoted from FormalConjectures/ErdosProblems/360.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/360.
The file states 3 research or textbook statements: 3 solved.
Erdos360.erdos_360
Solved: stated here without proof.
Let \(f(n)\) be minimal such that \(\{1,\ldots,n-1\}\) can be partitioned into \(f(n)\) classes so that \(n\) cannot be expressed as a sum of distinct elements from the same class. How fast does \(f(n)\) grow?
A problem of Erdős and Graham [ErGr80]. Conlon, Fox, and Pham [CFP21, Theorem 1.5] determined the order of growth of \(f(n)\) up to a multiplicative constant, proving
\[f(n) \asymp \frac{n^{1/3}(n/\phi(n))}{(\log n)^{1/3}(\log\log n)^{2/3}}.\]Here \(\phi\) is Euler's totient function, and the statement is asymptotic (\(n \to \infty\)).
theorem erdos_360 : (fun n : ℕ ↦ (f n : ℝ)) =Θ[atTop] erdos_360.answer
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/360.lean, line 67.
Erdos360.erdos_360.variants.alon_erdos
Solved: stated here without proof.
Alon and Erdős [AlEr96] proved that \(f(n) = n^{1/3+o(1)}\), and more precisely
\[\frac{n^{1/3}}{(\log n)^{4/3}}\ll f(n) \ll \frac{n^{1/3}}{(\log n)^{1/3}}(\log\log n)^{1/3}.\]This is the two-sided bound, which implies the first claim.
theorem erdos_360.variants.alon_erdos :
(fun n : ℕ ↦ (n : ℝ) ^ (1 / 3 : ℝ) / Real.log n ^ (4 / 3 : ℝ)) =O[atTop]
(fun n : ℕ ↦ (f n : ℝ)) ∧
(fun n : ℕ ↦ (f n : ℝ)) =O[atTop]
(fun n : ℕ ↦ (n : ℝ) ^ (1 / 3 : ℝ) / Real.log n ^ (1 / 3 : ℝ) *
Real.log (Real.log n) ^ (1 / 3 : ℝ))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/360.lean, line 77.
Erdos360.erdos_360.variants.vu
Solved: stated here without proof.
Vu [Vu07] improved the lower bound to
\[f(n) \gg \frac{n^{1/3}}{\log n}.\]
theorem erdos_360.variants.vu :
(fun n : ℕ ↦ (n : ℝ) ^ (1 / 3 : ℝ) / Real.log n) =O[atTop] (fun n : ℕ ↦ (f n : ℝ))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/360.lean, line 90.
Sources
TheoremErdős Problem 361#
Reference: erdosproblems.com/361
Quoted from FormalConjectures/ErdosProblems/361.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/361.
The file states 1 research or textbook statement: 1 open. It also has 1 test statement, counted here but not shown.
Erdos361.erdos_361
Open: stated without proof.
Let \(c > 0\) and \(n\) be some large integer. What is the size of the largest set \(A \subseteq \{1, \ldots, \lfloor c n \rfloor\}\) such that \(n\) is not a sum of a subset of \(A\)? Does this depend on \(n\) in an irregular way?
theorem erdos_361 (c : ℝ) (hc : 0 < c) :
subsetSumAvoidanceNumber c = erdos_361.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/361.lean, line 70.
Sources
TheoremErdős Problem 362#
References: - erdosproblems.com/362 - [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). - [SaSz65] Sárközi, A. and Szemerédi, E., Über ein Problem von Erdős und Moser. Acta Arith. (1965), 205-208. - [St80] Stanley, Richard P., Weyl groups, the hard Lefschetz theorem, and the Sperner property. SIAM J. Algebraic Discrete Methods (1980), 168-184. - [Ha77] Halász, G., Estimates for the concentration function of combinatorial number theory and probability. Period. Math. Hungar. (1977), 197-211.
Quoted from FormalConjectures/ErdosProblems/362.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/362.
The file states 2 research or textbook statements: 2 solved.
Erdos362.erdos_362
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos362.lean#L2541.
Let \(A\subseteq \mathbb{N}\) be a finite set of size \(N\). Is it true that, for any fixed \(t\), there are
\[\ll \frac{2^N}{N^{3/2}}\]many \(S\subseteq A\) such that \(\sum_{n\in S}n=t\)?
Erdős and Moser [Er65] proved the first bound with an additional factor of \((\log n)^{3/2}\). This was removed by Sárközy and Szemerédi [SaSz65], thereby answering the first question in the affirmative. Stanley [St80] has shown that this quantity is maximised when \(A=\{-\lfloor \frac{N-1}{2}\rfloor,\ldots,\lfloor\frac{N}{2}\rfloor\}\).
theorem erdos_362 : ∃ C : ℝ, ∀ (A : Finset ℕ) (t : ℕ), A.Nonempty →
({S ∈ A.powerset | ∑ n ∈ S, n = t}.card : ℝ) ≤ C * 2 ^ A.card / (A.card : ℝ) ^ (3 / 2 : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/362.lean, line 58.
Erdos362.erdos_362.variants.fixed_card
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos362.lean#L2541.
If we further ask that \(\lvert S\rvert=l\) (for any fixed \(l\)) then is the number of solutions
\[\ll \frac{2^N}{N^2},\]with the implied constant independent of \(l\) and \(t\)?
The second question was answered in the affirmative by Halász [Ha77], as a consequence of a more general multi-dimensional result.
theorem erdos_362.variants.fixed_card : ∃ C : ℝ, ∀ (A : Finset ℕ) (l t : ℕ),
A.Nonempty →
({S ∈ A.powersetCard l | ∑ n ∈ S, n = t}.card : ℝ) ≤ C * 2 ^ A.card / (A.card : ℝ) ^ 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/362.lean, line 73.
Sources
TheoremErdős Problem 363#
References: - erdosproblems.com/363 - [BaBe07] Bauer, Mark and Bennett, Michael A., On a question of Erd\H{o}s and Graham. Enseign. Math. (2) (2007), 259--264. - [BeVL12] Bennett, Michael A. and Van Luijk, Ronald, Squares from blocks of consecutive integers: a problem of Erd\H{o}s and Graham. Indag. Math. (N.S.) (2012), 123--127. - [Ul05] Ulas, Maciej, On products of disjoint blocks of consecutive integers. Enseign. Math. (2) (2005), 331--334.
Quoted from FormalConjectures/ErdosProblems/363.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/363.
The file states 1 research or textbook statement: 1 solved.
Erdos363.erdos_363
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos363.lean.
Is it true that, for each fixed \(n\) and fixed sizes \(k_1,\ldots,k_n \geq 4\), there are only finitely many collections of disjoint intervals \(I_1,\ldots,I_n\) of size \(\lvert I_i\rvert = k_i\) for \(1\leq i\leq n\) such that
\[\prod_{1\leq i\leq n}\prod_{m\in I_i}m\]is a square?
The number of intervals and their sizes are fixed: the list
ksof sizes determines both. Without this restriction finiteness fails, by a result of Skałba (see [Ul05]).This is false: Ulas [Ul05] constructed infinitely many such collections with \(n = 4\) and \(k_1 = \cdots = k_4 = 4\).
theorem erdos_363 : ¬ ∀ ks : List ℕ,
{S : List (Finset ℕ) | IsValidCollection S ∧ S.map Finset.card = ks}.Finite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/363.lean, line 68.
Sources
TheoremErdős Problem 364#
Reference: erdosproblems.com/364
Quoted from FormalConjectures/ErdosProblems/364.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/364.
The file states 3 research or textbook statements: 2 open and 1 textbook result.
Erdos364.erdos_364
Open: stated without proof.
There is no consecutive triple of powerful numbers.
theorem erdos_364 :
¬ ∃ (n : ℕ), Powerful n ∧ Powerful (n + 1) ∧ Powerful (n + 2)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/364.lean, line 34.
Erdos364.erdos_364.variants.strong
Open: stated without proof.
Erdős [Er76d] conjectured a stronger statement: if \(n_k\) is the \(k\)th powerful number, then \(n_{k+2} - n_k > n_k^c\) for some constant \(c > 0\).
[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.
theorem erdos_364.variants.strong :
∃ (c : ℝ) (h : c > 0), ∀ (k : ℕ),
Nat.nth Powerful (k + 2) - Nat.nth Powerful k > (Nat.nth Powerful k : ℝ) ^ c
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/364.lean, line 45.
Erdos364.erdos_364.variants.weak
Textbook result, proved here.
There is no quadruple of powerful numbers, since at least one of the four numbers must be \(2 \pmod{4}\), which cannot be powerful (since \(2\) divides it, but \(2^2\) does not).
theorem erdos_364.variants.weak :
¬ ∃ (n : ℕ), Powerful n ∧ Powerful (n + 1) ∧ Powerful (n + 2) ∧ Powerful (n + 3)
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/364.lean, line 55.
Sources
TheoremErdős Problem 365#
References: - erdosproblems.com/365 - [Go70] Golomb, S. W., Powerful numbers. Amer. Math. Monthly (1970), 848-855. - [Gu04] Guy, R. K., Unsolved problems in number theory (2004), Problem B16. - [Wa76] Walker, D. T., Consecutive integer pairs of powerful numbers and related Diophantine equations. Fibonacci Quart. (1976), 111-116.
Quoted from FormalConjectures/ErdosProblems/365.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/365.
The file states 2 research or textbook statements: 1 open and 1 solved. It also has 1 test statement, counted here but not shown.
Erdos365.erdos_365.parts.i
Proved here.
Do all pairs of consecutive powerful numbers \(n\) and \(n+1\) come from solutions to Pell equations? In other words, must either \(n\) or \(n+1\) be a square?
The answer to the first question is no: Golomb [Go70] observed that both \(12167=23^3\) and \(12168=2^3 3^2 13^2\) are powerful.
We require \(n>0\) since
Nat.Powerfulalso includes \(0\).
theorem erdos_365.parts.i :
¬ ∀ n : ℕ, 0 < n → Nat.Powerful n → Nat.Powerful (n + 1) →
IsSquare n ∨ IsSquare (n + 1)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/365.lean, line 80.
Erdos365.erdos_365.parts.ii
Open: stated without proof.
Is the number of positive \(n\leq x\) such that \(n\) and \(n+1\) are both powerful bounded by \((\log x)^{O(1)}\)?
theorem erdos_365.parts.ii :
∃ C : ℝ, 0 < C ∧ ∃ k : ℕ, ∀ᶠ x : ℕ in Filter.atTop,
({n : ℕ | 0 < n ∧ n ≤ x ∧ Nat.Powerful n ∧ Nat.Powerful (n + 1)}.ncard : ℝ) ≤
C * (Real.log x) ^ k
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/365.lean, line 92.
Sources
TheoremErdős Problem 366#
Reference: erdosproblems.com/366
Quoted from FormalConjectures/ErdosProblems/366.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/366.
The file states 3 research or textbook statements: 2 open and 1 solved. It also has 1 test statement, counted here but not shown.
Erdos366.erdos_366
Open: stated without proof.
Are there any \(2\)-full \(n\) such that \(n+1\) is \(3\)-full?
theorem erdos_366 : ∃ n > 0, (2).Full n ∧ (3).Full (n + 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/366.lean, line 34.
Erdos366.erdos_366.variants.three_two
Proved here.
Erdős and Graham asked whether \((8, 9)\) is the only pair of consecutive integers \(n\), \(n+1\) with \(n\) \(3\)-full and \(n+1\) \(2\)-full. The answer is no: \(12167 = 23^3\) and \(12168 = 2^3 3^2 13^2\) is another such pair, already known to Golomb [Go70].
theorem erdos_366.variants.three_two :
¬ ∀ n > 0, (3).Full n ∧ (2).Full (n + 1) → n = 8
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/366.lean, line 51.
Erdos366.erdos_366.variants.weaker
Open: stated without proof.
Are there any consecutive pairs of \(3\)-full integers?
theorem erdos_366.variants.weaker :
∃ n > 0, (3).Full n ∧ (3).Full (n + 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/366.lean, line 60.
Sources
TheoremErdős Problem 367#
References: - erdosproblems.com/367 - [ErGr80] P. Erdős and R. L. Graham, Old and New Problems and Results in Combinatorial Number Theory, L'Enseignement Mathématique (1980).
Quoted from FormalConjectures/ErdosProblems/367.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/367.
The file states 5 research or textbook statements: 1 open and 4 solved.
Erdos367.erdos_367.parts.i
Open: stated without proof.
Let \(B_2(n)\) be the \(2\)-full part of \(n\) (that is, \(B_2(n)=n/n'\) where \(n'\) is the product of all primes that divide \(n\) exactly once). Is it true that, for every fixed \(k \geq 1\), \(\prod_{n \leq m < n+k} B_2(m) \ll n^{2+o(1)}\)?
theorem erdos_367.parts.i : ∀ k : ℕ, 1 ≤ k →
∃ e : ℕ → ℝ,
e =o[atTop] (1 : ℕ → ℝ) ∧
∀ᶠ n in atTop,
((∏ m ∈ .Ico n (n + k), B 2 m : ℕ) : ℝ) ≤ (n : ℝ) ^ (2 + e n)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/367.lean, line 46.
Erdos367.erdos_367.parts.ii
Solved: stated here without proof.
Or perhaps even \(\prod_{n \leq m < n+k} B_2(m) \ll_k n^2\)?
van Doorn notes in the comments that this fails for all \(k \geq 3\).
theorem erdos_367.parts.ii : ¬ ∀ k : ℕ, 1 ≤ k →
(fun n ↦ ((∏ m ∈ .Ico n (n + k), B 2 m : ℕ) : ℝ)) =O[atTop]
fun n ↦ (n : ℝ) ^ (2 : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/367.lean, line 59.
Erdos367.erdos_367.variants.k_le_two
Solved: stated here without proof.
van Doorn notes in the comments that for \(k \leq 2\) we trivially have \(\prod_{n \leq m < n+k} B_2(m) \ll n^2\).
theorem erdos_367.variants.k_le_two : ∀ k : ℕ, k ≤ 2 →
(fun n ↦ ((∏ m ∈ .Ico n (n + k), B 2 m : ℕ) : ℝ)) =O[atTop]
fun n ↦ (n : ℝ) ^ (2 : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/367.lean, line 69.
Erdos367.erdos_367.variants.k_ge_three_lower
Solved: stated here without proof.
But this fails for all \(k \geq 3\), and in fact \(\prod_{n \leq m < n+3} B_2(m) \gg n^2 \log n\) infinitely often.
theorem erdos_367.variants.k_ge_three_lower :
∃ c > (0 : ℝ), ∃ᶠ (n : ℕ) in atTop,
c * ((n : ℝ) ^ 2 * Real.log (n : ℝ)) ≤
((∏ m ∈ .Ico n (n + 3), B 2 m : ℕ) : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/367.lean, line 79.
Erdos367.erdos_367.variants.higher_full_parts
Solved: stated here; a Lean proof is at https://github.com/kusasyu36/erdos367-higher-full-parts/blob/9c995fbb1ec62bd675ac9bc162f9e2337d6db4f9/Erdos367HigherFullParts.lean#L57.
It would also be interesting to find upper and lower bounds for the analogous product with \(B_r\) for \(r \geq 3\), where \(B_r(n)\) is the \(r\)-full part of \(n\) (that is, the product of prime powers \(p^a \mid n\) such that \(p^{a+1} \nmid n\) and \(a \geq r\)). Is it true that, for every fixed \(r \geq 3\) and \(k \geq 2\), there is some \(\epsilon = \epsilon(r, k) > 0\) with \(\limsup \frac{\prod_{n \leq m < n+k} B_r(m)}{n^{1+\epsilon}} = \infty\)?
The webpage writes "for every fixed \(r,k \geq 2\) and \(\epsilon > 0\)", but van Doorn observes in the comments that the intended reading lets \(\epsilon\) depend on \(r\) and \(k\). Since \(B_r(m) \mid m\), the product is at most \(\prod_{n \leq m < n+k} m\), so the reading with \(\epsilon\) universally quantified is false.
The answer is yes: \(\epsilon = 1/(2r)\) works. For \(j \geq r\) let \(x = 2^j + 1\) and \(n = x^r - 1\); then \(B_r(n+1) = x^r\) and \(2^j \mid n\) gives \(B_r(n) \geq 2^j\), so the product over \([n, n+k)\) is at least \(2^j x^r \geq (\sqrt{x}/2)\, n^{1 + 1/(2r)}\), which is unbounded. A stronger exponent (any \(\epsilon < (r+1)/r^2\)) is claimed in the forum but is not formalised.
theorem erdos_367.variants.higher_full_parts :
∀ r k : ℕ, 3 ≤ r → 2 ≤ k → ∃ ε : ℝ, 0 < ε ∧
atTop.limsup (fun n ↦
((∏ m ∈ .Ico n (n + k), B r m : ℕ) / (n : ℝ) ^ (1 + ε) |>.toEReal)) = ⊤
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/367.lean, line 106.
Sources
TheoremErdős Problem 368#
References: - erdosproblems.com/368 - [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 (1976), 25–44. - [Po18] Pólya, Georg, Zur arithmetischen Untersuchung der Polynome. Math. Z. (1918), 143–148. - [Sc67b] Schinzel, A., On two theorems of Gelfond and some of their applications. Acta Arith. (1967/68), 177–236.
Quoted from FormalConjectures/ErdosProblems/368.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/368.
The file states 4 research or textbook statements: 2 open and 2 solved.
Erdos368.erdos_368.lower_bound
Open: stated without proof.
How large is the largest prime factor of \(n(n+1)\)? The truth is probably \(F(n)\gg (\log n)^2\) for all \(n\).
theorem erdos_368.lower_bound :
∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 1 ≤ n → c * Real.log n ^ 2 ≤ (F n : ℝ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/368.lean, line 48.
Erdos368.erdos_368.upper_bound
Open: stated without proof.
Erdős [Er76d] conjectured that, for every \(\epsilon>0\), there are infinitely many \(n\) such that \(F(n)<(\log n)^{2+\epsilon}\).
theorem erdos_368.upper_bound :
∀ ε : ℝ, 0 < ε → ∃ᶠ n : ℕ in atTop, (F n : ℝ) < Real.log n ^ (2 + ε)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/368.lean, line 57.
Erdos368.erdos_368.variants.tendsto
Solved: stated here without proof.
Pólya [Po18] proved that \(F(n)\to\infty\) as \(n\to\infty\).
theorem erdos_368.variants.tendsto : Tendsto F atTop atTop
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/368.lean, line 63.
Erdos368.erdos_368.variants.subpower
Solved: stated here without proof.
For every \(\delta>0\), there are infinitely many \(n\) with \(F(n)\leq n^\delta\). This follows from Schinzel's [Sc67b] observation that, for infinitely many \(n\), \(F(n)\leq n^{O(1/\log\log\log n)}\).
theorem erdos_368.variants.subpower :
∀ δ : ℝ, 0 < δ → ∃ᶠ n : ℕ in atTop, (F n : ℝ) ≤ (n : ℝ) ^ δ
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/368.lean, line 72.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.