Erdős Problem 269 to Erdős Problem 290
TheoremErdős Problem 269#
Reference: erdosproblems.com/269
Quoted from FormalConjectures/ErdosProblems/269.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/269.
The file states 3 research or textbook statements: 2 open and 1 solved.
Erdos269.erdos_269.variants.rational
Open: stated without proof.
Let \(P\) be a finite set of primes with \(|P| \ge 2\) and let \(\{a_1 < a_2 < \dots\}\) be the set of positive integers whose prime factors are all in \(P\). Is the sum
\[ \sum_{n=1}^\infty \frac{1}{[a_1,\ldots,a_n]} \]rational?
theorem erdos_269.variants.rational :
∀ᵉ (P : Finset ℕ) (h : ∀ p ∈ P, p.Prime) (h_card : P.card ≥ 2),
∃ (q : ℚ), q = (series (P : Set ℕ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/269.lean, line 63.
Erdos269.erdos_269.variants.irrational
Open: stated without proof.
Let \(P\) be a finite set of primes with \(|P| \ge 2\) and let \(\{a_1 < a_2 < \dots\}\) be the set of positive integers whose prime factors are all in \(P\). Is the sum
\[ \sum_{n=1}^\infty \frac{1}{[a_1,\ldots,a_n]} \]irrational?
theorem erdos_269.variants.irrational :
∀ᵉ (P : Finset ℕ) (h : ∀ p ∈ P, p.Prime) (h_card : P.card ≥ 2),
Irrational (series (P : Set ℕ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/269.lean, line 76.
Erdos269.erdos_269.variants.infinite
Solved: stated here without proof.
This theorem addresses the case where the set of primes \(P\) is infinite. In this case the sum is irrational.
theorem erdos_269.variants.infinite (P : Set ℕ) (h : ∀ p ∈ P, p.Prime) (h_inf : P.Infinite) :
Irrational (series P)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/269.lean, line 86.
Sources
TheoremErdős Problem 270#
References: - erdosproblems.com/270 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Ha75] Hansen, E. R., A Table of Series and Products. Prentice-Hall (1975), 87. - [CrKo25] T. Crmarić and V. Kovač, On the irrationality of certain super-polynomially decaying series. arXiv:2504.18712 (2025). - [Ko26] V. Kovač, solution of the linear case (2026).
Quoted from FormalConjectures/ErdosProblems/270.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/270.
The file states 4 research or textbook statements: 1 open and 3 solved.
Erdos270.erdos_270
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos270.lean#L1027.
Let \(f(n)\to \infty\) as \(n\to \infty\). Is it true that
\[\sum_{n\geq 1} \frac{1}{(n+1)\cdots (n+f(n))}\]is irrational?
Erdős and Graham [ErGr80] write 'the answer is almost surely in the affirmative if \(f(n)\) is assumed to be nondecreasing'. The case \(f(n)=n\) was subsequently settled by Crmarić and Kovač [Ko26]. Hansen [Ha75] has shown that
\[\sum_n \frac{1}{\binom{2n}{n}}=\sum_n \frac{n!}{(n+1)\cdots (n+n)}=\frac{1}{3}+\frac{2\pi}{3^{5/2}}\]is transcendental.
Crmarić and Kovač [CrKo25] have shown that the answer to this question is no in a strong sense: for any \(\alpha \in (0,\infty)\) there exists a function \(f:\mathbb{N}\to\mathbb{N}\) such that \(f(n)\to \infty\) as \(n\to\infty\) and
\[\sum_{n\geq 1} \frac{1}{(n+1)\cdots (n+f(n))}=\alpha.\]
theorem erdos_270 :
¬ ∀ f : ℕ → ℕ, Tendsto f atTop atTop → Irrational (series f)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/270.lean, line 64.
Erdos270.erdos_270.variants.every_value
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos270.lean#L1009.
Crmarić and Kovač [CrKo25]: for any \(\alpha \in (0,\infty)\) there exists a function \(f:\mathbb{N}\to\mathbb{N}\) such that \(f(n)\to \infty\) as \(n\to\infty\) and
\[\sum_{n\geq 1} \frac{1}{(n+1)\cdots (n+f(n))}=\alpha.\]
theorem erdos_270.variants.every_value (α : ℝ) (hα : 0 < α) :
∃ f : ℕ → ℕ, Tendsto f atTop atTop ∧
HasSum (fun n : ℕ => (∏ i ∈ Finset.Icc (n + 2) (n + 1 + f (n + 1)), (i : ℝ))⁻¹) α
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/270.lean, line 76.
Erdos270.erdos_270.variants.monotone
Open: stated without proof.
It is still possible that this sum is always irrational if \(f\) is assumed to be non-decreasing; Crmarić and Kovač [CrKo25] show that the set of the possible values of such a sum has Lebesgue measure zero.
theorem erdos_270.variants.monotone :
∀ f : ℕ → ℕ, Monotone f → Tendsto f atTop atTop → Irrational (series f)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/270.lean, line 87.
Erdos270.erdos_270.variants.linear
Solved: stated here without proof.
The case \(f(n)=n\) has a positive answer, as observed by Crmarić and Kovač [Ko26]: \(\sum_{n\geq 1} n!/(2n)!\) is irrational.
theorem erdos_270.variants.linear : Irrational (series id)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/270.lean, line 94.
Sources
TheoremErdős Problem 272#
Reference: erdosproblems.com/272
Quoted from FormalConjectures/ErdosProblems/272.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/272.
The file states 4 research or textbook statements: 2 open and 2 solved.
Erdos272.erdos_272
Open: stated without proof.
Let \(N\geq 1\). What is the largest \(t\) such that there are \(A_1,\ldots,A_t\subseteq \{1,\ldots,N\}\) with \(A_i\cap A_j\) a non-empty arithmetic progression for all \(i\neq j\)?
theorem erdos_272 :
∀ N ≥ 1, maxArithInterCard N = erdos_272.answer N
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/272.lean, line 53.
Erdos272.erdos_272.variants.isBigO_sq
Solved: stated here without proof.
Simonovits and Sós have shown that \(t\ll N^2\).
theorem erdos_272.variants.isBigO_sq :
(fun N ↦ (maxArithInterCard N : ℝ)) =O[atTop] fun N ↦ (N : ℝ) ^ 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/272.lean, line 61.
Erdos272.erdos_272.variants.szabo
Solved: stated here without proof.
Szabo showed that the maximal \(t\) is equal to
\[ \frac{N^2}{2} + O(N^{5/3}\log^3N). \]
theorem erdos_272.variants.szabo :
(fun N ↦ (maxArithInterCard N - N ^ 2 / 2 : ℝ)) =O[atTop]
fun N : ℕ ↦ N ^ ((5 : ℝ) / 3) * (Real.log N) ^ 3
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/272.lean, line 71.
Erdos272.erdos_272.variants.szabo_strong
Open: stated without proof.
Szabo asks whether the maximal \(t\) is given by
\[ \frac{N^2}{2} + O(N) \]
theorem erdos_272.variants.szabo_strong :
(fun N ↦ (maxArithInterCard N - N ^ 2 / 2 : ℝ)) =O[atTop] fun N : ℕ ↦ (N : ℝ)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/272.lean, line 82.
Sources
TheoremErdős Problem 273#
Reference: erdosproblems.com/273
Quoted from FormalConjectures/ErdosProblems/273.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/273.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos273.erdos_273
Open: stated without proof.
Is there a covering system all of whose moduli are of the form \(p-1\) for some primes \(p \geq 5\)?
theorem erdos_273 : ∃ c : StrictCoveringSystem ℤ, ∀ i, ∃ (p : ℕ), p.Prime ∧ 5 ≤ p ∧
c.moduli i = Ideal.span {↑(p - 1)}
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/273.lean, line 33.
Erdos273.erdos_273.variants.three
Solved: stated here without proof.
Is there a covering system all of whose moduli are of the form \(p-1\) for some primes \(p \geq 3\)?
theorem erdos_273.variants.three : ∃ c : StrictCoveringSystem ℕ, ∀ i, ∃ p, p.Prime ∧ 3 ≤ p ∧
c.moduli i = Ideal.span {↑(p - 1)}
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/273.lean, line 41.
Sources
TheoremErdős Problem 274#
References: * erdosproblems.com/274 * Wikipedia * arXiv:1803.08301 * arXiv:1803.03569 * PMC7247885 * arXiv:1804.11103
Quoted from FormalConjectures/ErdosProblems/274.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/274.
The file states 3 research or textbook statements: 2 open and 1 solved.
Erdos274.erdos_274
Open: stated without proof.
If \(G\) is a group, can there exist an exact covering of \(G\) by more than one coset of different sizes? (i.e. each element is contained in exactly one of the cosets.)
The conjectured answer is no: in every such exact covering, two of the subgroups have the same cardinality.
theorem erdos_274 : ∃ (G : Type*) (_ : Group G),
1 < ENat.card G ∧ ∃ (ι : Type*) (_ : Fintype ι) (P : Group.ExactCovering G ι),
1 < Fintype.card ι ∧ ∀ i j, i ≠ j → #(P.parts i) ≠ #(P.parts j)
Category research open; AMS 20 Group theory and generalizations. Declared in FormalConjectures/ErdosProblems/274.lean, line 63.
Erdos274.erdos_274.variants.abelian
Solved: stated here; a Lean proof is at https://github.com/Jostamon/erdos274-hs-abelian/blob/2ab8a2e39e7dd7836adf577b52555f069244466f/Erdos274/Main.lean.
If
Gis a finite abelian group then there cannot exist an exact covering ofGby more than one cosets of different sizes? (i.e. each element is contained in exactly one of the cosets.)
theorem erdos_274.variants.abelian {G : Type*} [Fintype G] [CommGroup G]
(hG : 1 < Fintype.card G) {ι : Type*} [Fintype ι] (P : Group.ExactCovering G ι)
(hι : 1 < Fintype.card ι) :
∃ i j, i ≠ j ∧ #(P.parts i) = #(P.parts j)
Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/ErdosProblems/274.lean, line 76.
Erdos274.herzog_schonheim
Open: stated without proof.
Let \(G\) be a group, and let \(A = \{a_1G_1, \dots, a_kG_k\}\) be a finite system of left cosets of subgroups \(G_1, \dots, G_k\) of \(G\).
Herzog and Schönheim conjectured that if \(A\) forms a partition of \(G\) with \(k > 1\), then the indices \([G:G_1], \dots, [G:G_k]\) cannot be distinct.
theorem herzog_schonheim {G : Type*} [Group G] (hG : 1 < ENat.card G) {ι : Type*} [Fintype ι]
(hι : 1 < Fintype.card ι) (P : Group.ExactCovering G ι) :
∃ i j, i ≠ j ∧ (P.parts i).index = (P.parts j).index
Category research open; AMS 20 Group theory and generalizations. Declared in FormalConjectures/ErdosProblems/274.lean, line 90.
Sources
TheoremErdős Problem 275#
References: - erdosproblems.com/275 - [CrVE70] R.B. Crittenden and C.L. Vanden Eynden, Any n arithmetic progressions covering the first 2^n integers cover all integers, Proc. Amer. Math. Soc. 24 (1970), 475-481.
Quoted from FormalConjectures/ErdosProblems/275.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/275.
The file states 1 research or textbook statement: 1 solved.
Erdos275.erdos_275
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos275.lean.
If a finite system of \(r\) congruences \(\{ a_i\pmod{n_i} : 1\leq i\leq r\}\) (the \(n_i\) are not necessarily distinct) covers \(2^r\) consecutive integers then it covers all integers.
This is best possible as the system \(2^{i-1}\pmod{2^i}\) shows. This was proved independently by Selfridge and Crittenden and Vanden Eynden [CrVE70].
This was formalized in Lean by Alexeev using Aristotle.
theorem erdos_275 (r : ℕ) (a : Fin r → ℤ) (n : Fin r → ℕ)
(H : ∃ k : ℤ, ∀ x ∈ Ico k (k + 2 ^ r), ∃ i, x ≡ a i [ZMOD n i]) (x : ℤ) :
∃ i, x ≡ a i [ZMOD n i]
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/275.lean, line 46.
Sources
TheoremErdős Problem 276#
References: erdosproblems.com/276
Quoted from FormalConjectures/ErdosProblems/276.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/276.
The file states 1 research or textbook statement: 1 open.
Erdos276.erdos_276
Open: stated without proof.
Is there an infinite Lucas sequence \(a_0, a_1, \ldots\) where \(a_{n+2} = a_{n+1} + a_n\) for \(n \ge 0\) such that all \(a_k\) are composite, and yet no integer has a common factor with every term of the sequence?
theorem erdos_276 :
∃ (a : ℕ → ℕ),
IsLucasSequence a ∧ (∀ k, (a k).Composite) ∧ (∀ n > 1, ∃ k, Nat.gcd n (a k) = 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/276.lean, line 49.
Sources
TheoremErdős Problem 277#
References: - erdosproblems.com/277 - [Ha79] Haight, J. A., Covering systems of congruences, a negative result. Mathematika (1979), 53--61.
Quoted from FormalConjectures/ErdosProblems/277.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/277.
The file states 1 research or textbook statement: 1 solved.
Erdos277.erdos_277
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1268917deaaaa0d674f651287027baa26cea9920/src/latest/ErdosProblems/Erdos277.lean#L1294.
Is it true that, for every \(c\), there exists an \(n\) such that \(\sigma(n)>cn\) but there is no covering system whose moduli all divide \(n\)?
This was answered affirmatively by Haight [Ha79].
theorem erdos_277 :
∀ c : ℝ, ∃ n : ℕ, (σ 1 n : ℝ) > c * n ∧
∀ (m : StrictCoveringSystem ℤ), ∃ i, (n : ℤ) ∉ m.moduli i
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/277.lean, line 43.
Sources
TheoremErdős Problem 279#
Reference: erdosproblems.com/279
Quoted from FormalConjectures/ErdosProblems/279.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/279.
The file states 1 research or textbook statement: 1 open.
Erdos279.erdos_279
Open: stated without proof.
Let \(k\geq 3\). Is there a choice of congruence classes \(a_p\pmod{p}\) for every prime \(p\) such that all sufficiently large integers can be written as \(a_p+tp\) for some prime \(p\) and integer \(t\geq k\)?
theorem erdos_279 : ∀ k : Nat, k ≥ 3 →
∃ a : Nat → Nat, ∃ N : Nat, (∀ p : Nat, p.Prime → a p < p) ∧
∀ n ≥ N, ∃ p : Nat, ∃ t ≥ k, p.Prime ∧ n = a p + t * p
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/279.lean, line 35.
Sources
TheoremErdős Problem 280#
References: - erdosproblems.com/280 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
Quoted from FormalConjectures/ErdosProblems/280.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/280.
The file states 1 research or textbook statement: 1 solved.
Erdos280.erdos_280
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos280.lean.
Let $n_1\lt n_2\lt \cdots $ be an infinite sequence of integers with associated \(a_k\pmod{n_k}\), such that for some \(\epsilon>0\) we have \(n_k>(1+\epsilon)k\log k\) for all \(k\). Then
\[ \#\{ m\lt n_k : m\not\equiv a_i\pmod{n_i} \textrm{ for }1\leq i\leq k\}\neq o(k). \]Cambie observed that this is false.
theorem erdos_280 :
¬ ∀ (n a : ℕ → ℕ), StrictMono n → (∀ i, 1 ≤ i → a i < n i) →
(∃ ε : ℝ, 0 < ε ∧
∀ k, 1 ≤ k → (n k : ℝ) > (1 + ε) * (k : ℝ) * Real.log (k : ℝ)) →
¬ Tendsto
(fun k : ℕ => (uncoveredCount n a k : ℝ) / (k : ℝ))
atTop (nhds 0)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/280.lean, line 55.
Sources
TheoremErdős Problem 281#
References: - erdosproblems.com/281 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [DaEr36] Davenport, H. and Erdős, P., On sequences of positive integers. Acta Arithmetica (1936), 147-151. - [HaRo66] Halberstam, H. and Roth, K. F., Sequences. Vol. I. (1966), xx+291.
Quoted from FormalConjectures/ErdosProblems/281.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/281.
The file states 1 research or textbook statement: 1 solved.
Erdos281.erdos_281
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos281.lean.
Let \(n_1\lt n_2\lt \cdots\) be an infinite sequence such that, for any choice of congruence classes \(a_i\pmod{n_i}\), the set of integers not satisfying any of the congruences \(a_i\pmod{n_i}\) has density \(0\). Is it true that for every \(\epsilon>0\) there exists some \(k\) such that, for every choice of congruence classes \(a_i\), the density of integers not satisfying any of the congruences \(a_i\pmod{n_i}\) for \(1\leq i\leq k\) is less than \(\epsilon\)?
The answer is yes; the linked Lean proof formalizes Somani's argument.
theorem erdos_281 :
∀ (n : ℕ → ℕ), StrictMono n → (∀ i, 0 < n i) →
(∀ a : ResidueChoice n, Set.HasIntDensity (avoidAll n a) 0) →
∀ ε : ℝ, 0 < ε →
∃ k : ℕ, ∀ a : ResidueChoice n,
∃ d : ℝ, Set.HasIntDensity (avoidPrefix n a k) d ∧ d < ε
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/281.lean, line 60.
Sources
TheoremErdős Problem 282#
Reference: erdosproblems.com/282
Quoted from FormalConjectures/ErdosProblems/282.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/282.
The file states 5 research or textbook statements: 4 open and 1 textbook result. It also has 3 test statements, counted here but not shown.
Erdos282.erdos_282
Open: stated without proof.
Let \(A\subseteq \mathbb{N}\) be an infinite set and consider the following greedy algorithm for a rational \(x\in (0,1)\): choose the minimal \(n\in A\) not used so far such that \(n\geq 1/x\) and repeat with \(x\) replaced by \(x-\frac{1}{n}\). If this terminates after finitely many steps then this produces a representation of \(x\) as the sum of distinct unit fractions with denominators from \(A\).
Does this process always terminate if \(x\) has odd denominator and \(A\) is the set of odd numbers?
theorem erdos_282 {x : ℚ} (hx : x ∈ Set.Ioo 0 1) (hx_den : Odd x.den) :
greedyUnitFractionRem { n | Odd n } x =ᶠ[atTop] 0
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/282.lean, line 67.
Erdos282.erdos_282.variants.general
Open: stated without proof.
More generally, for which pairs \(x\) and \(A\) does this process terminate?
theorem erdos_282.variants.general (x : ℚ) (A : Set ℕ) :
greedyUnitFractionRem A x =ᶠ[atTop] 0 ↔ (x, A) ∈ erdos_282.variants.general.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/282.lean, line 75.
Erdos282.erdos_282.variants.fibonacci
Textbook result, stated without proof.
In 1202 Fibonacci observed that this process terminates for any \(x\) when \(A=\mathbb{N}\).
theorem erdos_282.variants.fibonacci {x : ℚ} (hx : x ∈ Set.Ioo 0 1) :
greedyUnitFractionRem .univ x =ᶠ[atTop] 0
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/282.lean, line 81.
Erdos282.erdos_282.variants.graham
Open: stated without proof.
Graham has shown that \(\frac{m}{n}\) is the sum of distinct unit fractions with denominators \(\equiv a\pmod{d}\) if and only if
\[\left(\frac{n}{(n,a,d)},\frac{d}{(a,d)}\right)=1.\]Does the greedy algorithm always terminate in such cases?
theorem erdos_282.variants.graham :
∀ x : ℚ, x ∈ Set.Ioo 0 1 → ∀ a d : ℕ, 1 < d →
(x.den / x.den.gcd (a.gcd d)).gcd (d / a.gcd d) = 1 →
greedyUnitFractionRem { n | n ≡ a [MOD d] } x =ᶠ[atTop] 0
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/282.lean, line 93.
Erdos282.erdos_282.variants.sq
Open: stated without proof.
Graham has also shown that \(x\) is the sum of distinct unit fractions with square denominators if and only if \(x\in [0,\pi^2/6-1)\cup [1,\pi^2/6)\). Does the greedy algorithm for this always terminate? Erdős and Graham believe not - indeed, perhaps it fails to terminate almost always.
theorem erdos_282.variants.sq :
∀ x : ℚ, (x : ℝ) ∈ Set.Ico 0 (π ^ 2 / 6 - 1) ∪ Set.Ico 1 (π ^ 2 / 6) →
greedyUnitFractionRem { n | IsSquare n } x =ᶠ[atTop] 0
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/282.lean, line 111.
Sources
TheoremErdős Problem 283#
References: - erdosproblems.com/283 - [Al19] Alekseyev, Max A., On partitions into squares of distinct integers whose reciprocals sum to 1. (2019), 213--221. - [Ca60] Cassels, J. W. S., On the representation of integers as the sums of distinct summands taken from a fixed set. Acta Sci. Math. (Szeged) (1960), 111-124. - [Gr63] Graham, R. L., A theorem on partitions. J. Austral. Math. Soc. (1963), 435-441. - [vD25] W. van Doorn, Partitions with prescribed sum of rationals: asymptotic bounds. arXiv:2502.02200 (2025).
Quoted from FormalConjectures/ErdosProblems/283.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/283.
The file states 8 research or textbook statements: 8 solved.
Erdos283.erdos_283
Solved: stated here; a Lean proof is at https://github.com/Shashi456/erdos-formalizations/blob/286f856aa3fc08957b80950fd18a45aab8d045ea/Erdos/P283/Proof_flat.lean#L9738-L9746.
Let \(p\colon \mathbb{Z} \rightarrow \mathbb{Z}\) be a polynomial (with rational coefficients, taking integer values at all integers) whose leading coefficient is positive and such that there exists no \(d≥2\) with \(d ∣ p(n)\) for all \(n≥1\). Is it true that, for all sufficiently large \(m\), there exist integers \(1≤n_1\lt \dots < n_k\) such that
\[1=\frac{1}{n_1}+\cdots+\frac{1}{n_k}\]and
\[m=p(n_1)+\cdots+p(n_k)\]?
GPT 5.5 Pro (prompted by Price) has given a proof that the answer is yes, for the stronger version with \(1\) replaced by any rational \(\alpha>0\).
This was formalized in Lean by Ammanamanchi using Opus 4.6 and GPT 5.5 Pro.
theorem erdos_283 : ∀ p : ℚ[X], Condition p
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/283.lean, line 67.
Erdos283.erdos_283.variants.graham
Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_Erdos283_erdos_283_variants_graham.lean#L383.
Graham [Gr63] has proved this when \(p(x)=x\).
theorem erdos_283.variants.graham : Condition X
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/283.lean, line 75.
Erdos283.erdos_283.variants.graham_alpha
Solved: stated here without proof.
Graham also conjectures that this remains true with \(1\) replaced by an arbitrary rational \(\alpha>0\) (provided \(m\) is taken sufficiently large depending on \(\alpha\)).
theorem erdos_283.variants.graham_alpha :
∀ (p : ℚ[X]) (α : ℚ),
(∀ n : ℤ, ∃ z : ℤ, p.eval (n : ℚ) = z) →
0 < p.leadingCoeff →
(¬ ∃ (d : ℤ), d ≥ 2 ∧ ∀ (n : ℤ), n ≥ 1 → ∃ z : ℤ, p.eval (n : ℚ) = d * z) →
α > 0 →
∀ᶠ (m : ℕ) in atTop,
∃ S : Finset ℕ, (∀ n ∈ S, 1 ≤ n) ∧
(∑ n ∈ S, (1 / (n : ℚ))) = α ∧
(∑ n ∈ S, p.eval (n : ℚ)) = (m : ℚ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/283.lean, line 83.
Erdos283.erdos_283.variants.cassels
Solved: stated here without proof.
Cassels [Ca60] has proved that these conditions on the polynomial imply every sufficiently large integer is the sum of \(p(n_i)\) with distinct \(n_i\).
theorem erdos_283.variants.cassels :
∀ (p : ℚ[X]),
(∀ n : ℤ, ∃ z : ℤ, p.eval (n : ℚ) = z) →
0 < p.leadingCoeff →
(¬ ∃ (d : ℤ), d ≥ 2 ∧ ∀ (n : ℤ), n ≥ 1 → ∃ z : ℤ, p.eval (n : ℚ) = d * z) →
∀ᶠ (m : ℕ) in atTop,
∃ S : Finset ℕ, (∀ n ∈ S, 1 ≤ n) ∧
(∑ n ∈ S, p.eval (n : ℚ)) = (m : ℚ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/283.lean, line 100.
Erdos283.erdos_283.variants.burr
Solved: stated here without proof.
Burr has proved this if \(p(x)=x^k\) with \(k\geq 1\) and if we allow \(n_i=n_j\).
theorem erdos_283.variants.burr :
∀ (k : ℕ), k ≥ 1 →
∀ᶠ (m : ℕ) in atTop,
∃ M : Multiset ℕ, (∀ n ∈ M, 1 ≤ n) ∧
(M.map (fun n ↦ 1 / (n : ℚ))).sum = 1 ∧
(M.map (fun n ↦ (n : ℤ)^k)).sum = (m : ℤ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/283.lean, line 114.
Erdos283.erdos_283.variants.alekseyev
Solved: stated here without proof.
Alekseyev [Al19] has proved this when \(p(x)=x^2\), for all \(m>8542\).
theorem erdos_283.variants.alekseyev :
∀ (m : ℕ), m > 8542 →
∃ S : Finset ℕ, (∀ n ∈ S, 1 ≤ n) ∧
(∑ n ∈ S, (1 / (n : ℚ))) = 1 ∧
(∑ n ∈ S, (n : ℤ)^2) = (m : ℤ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/283.lean, line 126.
Erdos283.erdos_283.variants.van_doorn_linear
Solved: stated here without proof.
van Doorn [vD25] has investigated the question of what 'sufficiently large' means for \(p(x)=x\). van Doorn has also proved the original conjecture for many linear and quadratic polynomials. For example, if \(p(x) = x + b\) with \(1 \leq b \leq 5000\), then the conjecture is true.
theorem erdos_283.variants.van_doorn_linear :
∀ b : ℤ, 1 ≤ b → b ≤ 5000 → Condition (X + C (b : ℚ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/283.lean, line 139.
Erdos283.erdos_283.variants.van_doorn_quadratic
Solved: stated here without proof.
van Doorn [vD25] has proved the original conjecture for many linear and quadratic polynomials. For example, if \(p(x) = x^2 + b\) with \(1 \leq b \leq 800\), then the conjecture is true.
theorem erdos_283.variants.van_doorn_quadratic :
∀ b : ℤ, 1 ≤ b → b ≤ 800 → Condition (X^2 + C (b : ℚ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/283.lean, line 148.
Sources
TheoremErdős Problem 284#
References: - erdosproblems.com/284 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique 28 (1980). - [Cr01] Croot, III, Ernest S., On unit fractions with denominators in short intervals. Acta Arith. 99 (2001), 99-114. arXiv:math/9904181
Quoted from FormalConjectures/ErdosProblems/284.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/284.
The file states 1 research or textbook statement: 1 solved. It also has 1 API statement, counted here but not shown.
Erdos284.erdos_284
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos284.lean#L97.
Let \(f(k)\) be the maximal value of \(n_1\) such that there exist \(n_1\lt n_2\lt \cdots \lt n_k\) with
\[1=\frac{1}{n_1}+\cdots+\frac{1}{n_k}.\]Is it true that
\[f(k)=(1+o(1))\frac{k}{e-1}?\]Asked by Erdős and Graham [ErGr80, p. 33]. We state it as \(f(k)/k\to 1/(e-1)\), which is equivalent. Essentially solved by Croot [Cr01], who showed that for any \(N>1\) there exists some \(k\geq 1\) and
\[N\lt n_1\lt \cdots \lt n_k \leq (e+o(1))N\]with \(1=\sum \frac{1}{n_i}\). See also erdosproblems.com/286.
theorem erdos_284 :
Tendsto (fun k : ℕ ↦ (f k : ℝ) / k) atTop (nhds (1 / (Real.exp 1 - 1)))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/284.lean, line 77.
Sources
TheoremErdős Problem 285#
Reference: erdosproblems.com/285
Quoted from FormalConjectures/ErdosProblems/285.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/285.
The file states 2 research or textbook statements: 2 solved.
Erdos285.erdos_285
Solved: stated here without proof.
Let \(f(k)\) be the minimal value of \(n_k\) such that there exist \(n_1 < n_2 < \dots < n_k\) with
\[ 1 = \frac{1}{n_1} + \cdots + \frac{1}{n_k}. \]Is it true that
\[ f(k) = (1 + o(1)) \frac{e}{e - 1} k ? \]Proved by Martin [Ma00].
[Ma00] Martin, Greg, Denser Egyptian fractions. Acta Arith. (2000), 231-260.
theorem erdos_285 :
∀ᵉ (f : ℕ → ℕ)
(S : Set ℕ)
(hS : S = {k | ∃ (n : Fin k.succ → ℕ), StrictMono n ∧ 0 ∉ Set.range n ∧
1 = ∑ i, (1 : ℝ) / n i })
(h : ∀ k ∈ S,
IsLeast
{ n (Fin.last k) | (n : Fin k.succ → ℕ) (_ : StrictMono n) (_ : 0 ∉ Set.range n)
(_ : 1 = ∑ i, (1 : ℝ) / n i) }
(f k)),
∃ (o : ℕ → ℝ) (_ : o =o[atTop] (1 : ℕ → ℝ)),
∀ k ∈ S, f k = (1 + o k) * rexp 1 / (rexp 1 - 1) * (k + 1)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/285.lean, line 49.
Erdos285.erdos_285.variants.lb
Solved: stated here without proof.
It is trivial that \(f(k)\geq (1 + o(1)) \frac{e}{e - 1}k\).
theorem erdos_285.variants.lb (f : ℕ → ℕ)
(S : Set ℕ)
(hS : S = {k | ∃ (n : Fin k.succ → ℕ), StrictMono n ∧ 0 ∉ Set.range n ∧
1 = ∑ i, (1 : ℝ) / n i })
(h : ∀ k ∈ S,
IsLeast
{ n (Fin.last k) | (n : Fin k.succ → ℕ) (_ : StrictMono n) (_ : 0 ∉ Set.range n)
(_ : 1 = ∑ i, (1 : ℝ) / n i) }
(f k)) :
∃ (o : ℕ → ℝ) (_ : o =o[atTop] (1 : ℕ → ℝ)),
∀ k ∈ S, (1 + o k) * rexp 1 / (rexp 1 - 1) * (k + 1) ≤ f k
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/285.lean, line 67.
Sources
TheoremErdős Problem 286#
References: - erdosproblems.com/286 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Cr01] Croot, III, Ernest S., On unit fractions with denominators in short intervals. Acta Arith. (2001), 99-114.
Quoted from FormalConjectures/ErdosProblems/286.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/286.
The file states 1 research or textbook statement: 1 solved.
Erdos286.erdos_286
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos286.lean#L163.
Let \(k\geq 2\). Is it true that there exists an interval \(I\) of width \((e-1+o(1))k\) and integers \(n_1\lt \cdots\lt n_k\in I\) such that
\[1=\frac{1}{n_1}+\cdots+\frac{1}{n_k}?\]The answer is yes, proved by Croot [Cr01].
theorem erdos_286 : ∃ o : ℕ → ℝ, Tendsto o atTop (nhds 0) ∧
∀ᶠ k : ℕ in atTop, ∃ a b : ℝ, b - a = (exp 1 - 1 + o k) * k ∧
∃ S : Finset ℕ, S.card = k ∧ 0 ∉ S ∧ ∑ n ∈ S, (1 : ℝ) / n = 1 ∧
∀ n ∈ S, (n : ℝ) ∈ Set.Icc a b
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/286.lean, line 47.
Sources
TheoremErdős Problem 287#
Reference: erdosproblems.com/287
Quoted from FormalConjectures/ErdosProblems/287.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/287.
The file states 4 research or textbook statements: 2 open, 1 solved and 1 textbook result. It also has 1 test statement, counted here but not shown.
Erdos287.erdos_287
Open: stated without proof.
Let \(k\geq2\). Is it true that, for any distinct integers \(1 < n_1 < \cdots < n_k\) such that \(\sum_{i=1}^k \frac{1}{n_i} = 1\), we must have \(\max(n_{i+1} - n_i) \geq 3\)?
theorem erdos_287 :
∀ (k : ℕ) (hk : 2 ≤ k) (s : Fin k → ℕ),
StrictMono s → 1 < s ⟨0, by omega⟩ →
∑ i : Fin k, 1/ (s i : ℝ) = 1 →
3 ≤ max_gap k s
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/287.lean, line 43.
Erdos287.erdos_287.variants.gap_at_least_two
Solved: stated here; a Lean proof is at https://github.com/Zed-Rez/erdos-287-lean/blob/8bf27b1915ffbd155f071acbc57ba223451dc8ef/P287/gap_full.lean#L276-L281.
The lower bound of \(\geq 2\) is equivalent to saying that \(1\) is not the sum of reciprocals of consecutive integers, proved by Erdős [Er32].
theorem erdos_287.variants.gap_at_least_two :
∀ (k : ℕ) (_ : 2 ≤ k) (s : Fin k → ℕ),
StrictMono s → 1 < s ⟨0, by omega⟩ →
∑ i : Fin k, 1 / (s i : ℝ) = 1 →
2 ≤ max_gap k s
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/287.lean, line 58.
Erdos287.erdos_287.variants.prime_conjecture
Open: stated without proof.
For all large \(N\), there exists a prime \(p \in [N, 2N]\) such that \(\frac{p+1}{2}\) is also prime.
This is an open conjecture. If true, it would imply
erdos_287for all but at most finitely many exceptions (seeerdos_287.variants.prime_conjecture_implies).
theorem erdos_287.variants.prime_conjecture :
∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N →
∃ p : ℕ, Nat.Prime p ∧ N ≤ p ∧ p ≤ 2 * N ∧ Nat.Prime ((p + 1) / 2)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/287.lean, line 92.
Erdos287.erdos_287.variants.prime_conjecture_implies
Textbook result, stated without proof. A Lean proof is at https://github.com/Zed-Rez/erdos-287-lean/blob/43c2ef1c8f534d1c7547b1e18310daacba936083/P287/Part3.lean#L39-L47.
The conjecture
erdos_287would follow for all but at most finitely many exceptions if it were known that, for all large \(N\), there exists a prime \(p \in [N, 2N]\) such that \(\frac{p+1}{2}\) is also prime.More precisely: if the prime conjecture holds, then there exists \(k_0\) such that for all \(k \geq k_0\), any Egyptian fraction representation of \(1\) with \(k\) terms and all terms \(> 1\) must have \(\max(n_{i+1} - n_i) \geq 3\).
theorem erdos_287.variants.prime_conjecture_implies : type_of% erdos_287.variants.prime_conjecture →
∃ (k₀ : ℕ), ∀ᵉ (k : ℕ) (hk₀ : k₀ ≤ k) (hk : 2 ≤ k) (s : Fin k → ℕ),
StrictMono s → 1 < s ⟨0, by omega⟩ →
∑ i : Fin k, 1 / (s i : ℝ) = 1 →
3 ≤ max_gap k s
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/287.lean, line 109.
Sources
TheoremErdős Problem 288#
Reference: erdosproblems.com/288
Quoted from FormalConjectures/ErdosProblems/288.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/288.
The file states 4 research or textbook statements: 4 open.
Erdos288.erdos_288
Open: stated without proof.
Is it true that there are only finitely many pairs of intervals \(I_1\), \(I_2\) such that
\[ \sum_{n_1 \in I_1} \frac{1}{n_1} + \sum_{n_2 \in I_2} \frac{1}{n_2} \in \mathbb{N}? \]
theorem erdos_288 : Set.Finite { I : Fin 2 → ℕ+ × ℕ+ |
∀ j, (I j).1 ≤ (I j).2 ∧
∃ n : ℕ+, (∑ j : Fin 2, ∑ nⱼ ∈ Set.Icc (I j).1 (I j).2, (nⱼ⁻¹ : ℚ)) = n }
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/288.lean, line 37.
Erdos288.erdos_288.variants.i2_card_eq_1
Open: stated without proof.
This is still open even if \(|I_2| = 1\).
theorem erdos_288.variants.i2_card_eq_1 : Set.Finite { (I, n₂) : (ℕ+ × ℕ+) × ℕ+ |
I.1 ≤ I.2 ∧ ∃ n : ℕ+, ∑ n₁ ∈ Set.Icc I.1 I.2, (n₁⁻¹ : ℚ) + (n₂⁻¹ : ℚ) = n }
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/288.lean, line 46.
Erdos288.erdos_288.variants.k_intervals
Open: stated without proof.
It is perhaps true with two intervals replaced by any \(k\) intervals.
theorem erdos_288.variants.k_intervals : ∀ k, Set.Finite { I : Fin k → ℕ+ × ℕ+ |
∀ j, (I j).1 ≤ (I j).2 ∧
∃ n : ℕ+, (∑ j : Fin k, ∑ nⱼ ∈ Set.Icc (I j).1 (I j).2, (nⱼ⁻¹ : ℚ)) = n }
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/288.lean, line 54.
Erdos288.erdos_288.variants.exists_k_gt_2
Open: stated without proof.
Is it true for any \(k > 2\) that only finitely many \(k\) intervals satisfy this condition?
theorem erdos_288.variants.exists_k_gt_2 :
∃ k > 2, Set.Finite { I : Fin k → ℕ+ × ℕ+ |
∀ j, (I j).1 ≤ (I j).2 ∧
∃ n : ℕ+, (∑ j : Fin k, ∑ nⱼ ∈ Set.Icc (I j).1 (I j).2, (nⱼ⁻¹ : ℚ)) = n }
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/288.lean, line 63.
Sources
TheoremErdős Problem 289#
References: - erdosproblems.com/289 - [Ku+26] Kung, P.-N., Song, L., Hwang, D., Yoon, J., Li, C.-L., Severini, S., Olšák, M., Lockhart, E., Le, Q. V., Gokturk, B., Luong, T., Pfister, T., & Peng, N. (2026). LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks. arXiv:2606.03303.
Quoted from FormalConjectures/ErdosProblems/289.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/289.
The file states 1 research or textbook statement: 1 solved.
Erdos289.erdos_289
Solved: stated here; a Lean proof is at https://github.com/lfsong-google/formal-conjectures/blob/ff33e501bb78a90ae4703e22e052f8bb38e10146/FormalConjectures/ErdosProblems/289.lean#L9514.
Is it true that, for all sufficiently large \(k\), there exist finite intervals \(I_1, \dotsc, I_k \subset \mathbb{N}\), distinct, not overlapping or adjacent, with \(|I_i| \geq 2\) for \(1 \leq i \leq k\) such that
\[ 1 = \sum_{i=1}^k \sum_{n \in I_i} \frac{1}{n}? \]Here two intervals are adjacent if their union is again an interval, so any two of the \(I_i\) must be separated by at least one integer.
This is true: a formal proof in Lean 4 was produced by the LEAP prover agent [Ku+26] (see the linked
formal_proof). We note that other recent solutions were also posted ahead of this one (see erdosproblems.com/forum/thread/289/proof-claims); this formalization follows an independent, different proof path.
theorem erdos_289 :
(∀ᶠ k : ℕ in atTop, ∃ I : Fin k → ℕ × ℕ,
(∀ i, (I i).1 < (I i).2) ∧
(∀ i j, i ≠ j → (I i).2 + 1 < (I j).1 ∨ (I j).2 + 1 < (I i).1) ∧
∑ i, ∑ n ∈ .Icc (I i).1 (I i).2, (n⁻¹ : ℚ) = 1)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/289.lean, line 55.
Sources
TheoremErdős Problem 290#
References: - erdosproblems.com/290 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique (1980), p.34. - [vD24] van Doorn, W., On the non-monotonicity of the denominator of generalized harmonic sums. arXiv:2411.03073 (2024).
Quoted from FormalConjectures/ErdosProblems/290.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/290.
The file states 1 research or textbook statement: 1 solved.
Erdos290.erdos_290
Solved: stated here; a Lean proof is at https://github.com/Woett/Lean-files/blob/main/ErdosProblem290.lean.
Let \(a\geq 1\). Must there exist some \(b>a\) such that
\[\sum_{a\leq n\leq b}\frac{1}{n}=\frac{r_1}{s_1}\textrm{ and } \sum_{a\leq n\leq b+1}\frac{1}{n}=\frac{r_2}{s_2},\]with \((r_i,s_i)=1\) and \(s_2\lt s_1\)? If so, how does this \(b(a)\) grow with \(a\)?
This was resolved in the affirmative by van Doorn [vD24], who proved \(b=b(a)\) always exists, and in fact \(b(a) \ll a\). Indeed, if \(a\in (3^k,3^{k+1}]\) then one can take \(b=2\cdot 3^{k+1}-1\). van Doorn also proves that \(b(a)>a+(1/2-o(1))\log a\), and considers various generalisations of the original problem.
theorem erdos_290 :
(∀ a : ℕ, 1 ≤ a → ∃ b : ℕ, a < b ∧ harmonicDen a (b + 1) < harmonicDen a b)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/290.lean, line 52.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.