Erdős Problem 300 to Erdős Problem 321

TheoremErdős Problem 300#

References: - erdosproblems.com/300 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999). - [Cr03] Croot, III, Ernest S., On a coloring conjecture about unit fractions. Ann. of Math. (2) (2003), 545-556. - [LiSa24] Liu, Y. and Sawhney, M., On further questions regarding unit fractions. arXiv:2404.07113 (2024).

Quoted from FormalConjectures/ErdosProblems/300.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/300.

The file states 2 research or textbook statements: 2 solved.

Erdos300.erdos_300

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos300.lean#L4356.

Let \(A(N)\) denote the maximal cardinality of \(A\subseteq \{1,\ldots,N\}\) such that \(\sum_{n\in S}\frac{1}{n}\neq 1\) for all \(S\subseteq A\). Estimate \(A(N)\).

Erdős and Graham [ErGr80] believe the answer is \(A(N)=(1+o(1))N\). Croot [Cr03] disproved this, showing the existence of some constant \(c<1\) such that \(A(N)\lt cN\) for all large \(N\). It is trivial that \(A(N)\geq (1-\frac{1}{e}+o(1))N\). Liu and Sawhney [LiSa24] have proved that \(A(N)=(1-1/e+o(1))N\).

theorem erdos_300 : Tendsto (fun N : ℕ => (A N : ℝ) / N) atTop (𝓝 (1 - 1 / Real.exp 1))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/300.lean, line 59.

Erdos300.erdos_300.variants.erdos_graham

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos300.lean#L4356.

Erdős and Graham [ErGr80] believed that \(A(N)=(1+o(1))N\); this was disproved by Croot [Cr03].

theorem erdos_300.variants.erdos_graham :
    ¬ Tendsto (fun N : ℕ => (A N : ℝ) / N) atTop (𝓝 1)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/300.lean, line 67.

Sources

• FormalConjectures/ErdosProblems/300.lean at 2055e5ad
• erdosproblems.com/300

LeanErdos300.erdos_300 · Erdos300.erdos_300.variants.erdos_graham

TheoremErdős Problem 302#

References: - erdosproblems.com/302 - [BrRo91] Brown, Tom C. and Rödl, Voijtech, Monochromatic solutions to equations with unit fractions. Bull. Austral. Math. Soc. (1991), 387-392. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - va25

Quoted from FormalConjectures/ErdosProblems/302.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/302.

The file states 6 research or textbook statements: 1 open and 5 solved.

Erdos302.erdos_302.parts.i

Open: stated without proof.

Let \(f(N)\) be the size of the largest \(A\subseteq \{1,\ldots,N\}\) such that there are no solutions to

\[\frac{1}{a}= \frac{1}{b}+\frac{1}{c}\]

with distinct \(a,b,c\in A\)? Estimate \(f(N)\).

The colouring version of this is [303], which was solved by Brown and Rödl [BrRo91].

theorem erdos_302.parts.i (f : ℕ → ℕ) (hf : ∀ N, IsMaxNoTripleCard N (f N)) :
    Tendsto (fun N : ℕ => (f N : ℝ) / N) atTop (𝓝 erdos_302.parts.i.answer)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/302.lean, line 65.

Erdos302.erdos_302.parts.ii

Solved: stated here without proof.

In particular, is \(f(N)=(\tfrac{1}{2}+o(1))N\)?

This is false: it is contradicted by Cambie's lower bound of \((5/8+o(1))N\) recorded below, since \(5/8 > 1/2\).

theorem erdos_302.parts.ii (f : ℕ → ℕ) (hf : ∀ N, IsMaxNoTripleCard N (f N)) :
    ¬ Tendsto (fun N : ℕ => (f N : ℝ) / N) atTop (𝓝 ((1 : ℝ) / 2))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/302.lean, line 76.

Erdos302.erdos_302.variants.lower_half

Proved here.

One can take either \(A\) to be all odd integers in \([1,N]\) or all integers in \([N/2,N]\) to show \(f(N)\geq (1/2+o(1))N\).

theorem erdos_302.variants.lower_half (f : ℕ → ℕ) (hf : ∀ N, IsMaxNoTripleCard N (f N))
    (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop, ((1 : ℝ) / 2 - ε) * N ≤ f N

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/302.lean, line 85.

Erdos302.erdos_302.variants.lower_five_eighths

Solved: stated here without proof.

Stijn Cambie has observed that

\[f(N)\geq (5/8+o(1))N,\]

taking \(A\) to be all odd integers \(\leq N/4\) and all integers in \([N/2,N]\).

theorem erdos_302.variants.lower_five_eighths (f : ℕ → ℕ) (hf : ∀ N, IsMaxNoTripleCard N (f N))
    (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop, ((5 : ℝ) / 8 - ε) * N ≤ f N

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/302.lean, line 127.

Erdos302.erdos_302.variants.upper_nine_tenths

Solved: stated here without proof.

Wouter van Doorn has proved [va25] that

\[f(N) \leq (9/10+o(1))N.\]

theorem erdos_302.variants.upper_nine_tenths (f : ℕ → ℕ) (hf : ∀ N, IsMaxNoTripleCard N (f N))
    (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop, (f N : ℝ) ≤ ((9 : ℝ) / 10 + ε) * N

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/302.lean, line 137.

Erdos302.erdos_302.variants.upper_0_8461739827964010

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-302-upper-bound/blob/9447ceb/lean/Erdos302ReflectiveUpperFC.lean#L92-L99.

Kenta Kitamura (KitaKen1 on GitHub) has given a Lean proof (erdos-302-upper-bound) that

\[f(N) \leq (0.8461739827964010+o(1))N.\]

theorem erdos_302.variants.upper_0_8461739827964010 (f : ℕ → ℕ)
    (hf : ∀ N, IsMaxNoTripleCard N (f N)) (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop, (f N : ℝ) ≤ ((8461739827964010 : ℝ) / 10000000000000000 + ε) * N

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/302.lean, line 151.

Sources

• FormalConjectures/ErdosProblems/302.lean at 2055e5ad
• erdosproblems.com/302

LeanErdos302.erdos_302.parts.i · Erdos302.erdos_302.parts.ii · Erdos302.erdos_302.variants.lower_half · Erdos302.erdos_302.variants.lower_five_eighths · Erdos302.erdos_302.variants.upper_nine_tenths · Erdos302.erdos_302.variants.upper_0_8461739827964010

TheoremErdős Problem 303#

References: - erdosproblems.com/303 - [BrRo91] Brown, Tom C. and Rödl, Voijtech, Monochromatic solutions to equations with unit fractions. Bull. Austral. Math. Soc. (1991), 387-392.

Quoted from FormalConjectures/ErdosProblems/303.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/303.

The file states 1 research or textbook statement: 1 solved.

Erdos303.erdos_303

Solved: stated here; a Lean proof is at https://www.erdosproblems.com/forum/thread/303.

Is it true that in any finite colouring of the integers there exists a monochromatic solution to \(\frac 1 a = \frac 1 b + \frac 1 c\) with distinct \(a, b, c\)?

This is true, as proved by Brown and Rödl [BrRo91].

This was formalized in Lean by Yuan using Seed-Prover.

theorem erdos_303 :
    -- For any finite colouring of the integers
    ∀ (𝓒 : ℤ → ℤ), (Set.range 𝓒).Finite →
      -- There exists integers `a, b, c`
      ∃ (a b c : ℤ),
      -- that are non-zero and distinct.
      [a, b, c, 0].Nodup ∧
      -- `a, b, c` satisfy the equation
      (1/a : ℝ) = 1/b + 1/c ∧
      -- `a, b, c` have the same color
      (𝓒 '' {a, b, c}).Subsingleton

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/303.lean, line 43.

Sources

• FormalConjectures/ErdosProblems/303.lean at 2055e5ad
• erdosproblems.com/303

LeanErdos303.erdos_303

TheoremErdős Problem 304#

Reference: erdosproblems.com/304

[OAI26a] OpenAI, Short Egyptian fractions. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Short-Egyptian-fractions-September-25-2026/Short-Egyptian-fractions-September-25-2026.pdf

Quoted from FormalConjectures/ErdosProblems/304.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/304.

The file states 4 research or textbook statements: 4 solved. It also has 1 test statement and 11 API statements, counted here but not shown.

Erdos304.erdos_304.variants.upper_1950

Solved: stated here without proof.

In 1950, Erdős [Er50c] proved the upper bound

\[N(b) \ll \log b / \log \log b\]

. [Er50c] Erdős, P., Az \({1}/{x_1} + {1}/{x_2} + \ldots + {1}/{x_n} =A/B\) egyenlet eg\'{E}sz sz\'{A}m\'{u} megold\'{A}sairól. Mat. Lapok (1950), 192-210.

theorem erdos_304.variants.upper_1950 :
    (fun b => (smallestCollectionTo b : ℝ)) =O[atTop]
      (fun b => Real.log b / Real.log (Real.log b))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/304.lean, line 150.

Erdos304.erdos_304.variants.lower_1950

Solved: stated here; a Lean proof is at https://github.com/thepriceisright/publications/blob/8f055eb3fd1485477c92cbfbdfa4b3c56f192610/erdos/304/Lower1950.lean.

In 1950, Erdős [Er50c] proved the lower bound

\[\log \log b \ll N(b)\]

. [Er50c] Erdős, P., Az \({1}/{x_1} + {1}/{x_2} + \ldots + {1}/{x_n} =A/B\) egyenlet eg\'{E}sz sz\'{A}m\'{u} megold\'{A}sairól. Mat. Lapok (1950), 192-210.

theorem erdos_304.variants.lower_1950 :
    (fun b : ℕ => Real.log (Real.log b)) =O[atTop]
      (fun b => (smallestCollectionTo b : ℝ))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/304.lean, line 161.

Erdos304.erdos_304.variants.upper_1985

Solved: stated here without proof.

In 1985 Vose [Vo85] proved the upper bound

\[N(b) \ll \sqrt{\log b}\]

. [Vo85] Vose, Michael D., Egyptian fractions. Bull. London Math. Soc. (1985), 21-24.

theorem erdos_304.variants.upper_1985 :
    (fun b => (smallestCollectionTo b : ℝ)) =O[atTop]
      (fun b => Real.sqrt (Real.log b))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/304.lean, line 171.

Erdos304.upper_bound

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/ShortEgyptian/Main.lean#L33.

Is it true that

\[N(b) \ll \log \log b\]

?

Yes. This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.

theorem upper_bound :
    (fun b : ℕ => (smallestCollectionTo b : ℝ)) =O[atTop] (fun b : ℕ => Real.log (Real.log b))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/304.lean, line 185.

Sources

• FormalConjectures/ErdosProblems/304.lean at 2055e5ad
• erdosproblems.com/304

LeanErdos304.erdos_304.variants.upper_1950 · Erdos304.erdos_304.variants.lower_1950 · Erdos304.erdos_304.variants.upper_1985 · Erdos304.upper_bound

TheoremErdős Problem 305#

References: - erdosproblems.com/305 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [BlEr76] Bleicher, M. N. and Erdős, P., Denominators of unit fractions. J. Number Th. (1976), 157-168. - [Yo88] Yokota, H., On a problem of Bleicher and Erdős. J. Number Theory (1988), 198-207. - [LiSa24] Liu, Y. and Sawhney, M., On further questions regarding unit fractions. arXiv:2404.07113 (2024).

Quoted from FormalConjectures/ErdosProblems/305.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/305.

The file states 5 research or textbook statements: 5 solved.

Erdos305.erdos_305

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos305.lean#L217.

For integers \(1\leq a\lt b\) let \(D(a,b)\) be the minimal value of \(n_k\) such that there exist integers \(1\leq n_1\lt \cdots \lt n_k\) with

\[\frac{a}{b}=\frac{1}{n_1}+\cdots+\frac{1}{n_k}.\]

Estimate \(D(b)=\max_{1\leq a\lt b}D(a,b)\). Is it true that

\[D(b) \ll b(\log b)^{1+o(1)}?\]

Bleicher and Erdős [BlEr76] have shown that \(D(b)\ll b(\log b)^2\). If \(b=p\) is a prime then \(D(p) \gg p\log p\).

This was solved by Yokota [Yo88], who proved that

\[D(b)\ll b(\log b)(\log\log b)^4(\log\log\log b)^2.\]

This was improved by Liu and Sawhney [LiSa24] to

\[D(b)\ll b(\log b)(\log\log b)^3(\log\log\log b)^{O(1)}.\]

theorem erdos_305 : ∃ δ : ℕ → ℝ, Tendsto δ atTop (nhds 0) ∧
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ b : ℕ in atTop,
      (Dmax b : ℝ) ≤ C * b * (log b) ^ (1 + δ b)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/305.lean, line 69.

Erdos305.erdos_305.variants.bleicher_erdos

Solved: stated here without proof.

Bleicher and Erdős [BlEr76] have shown that \(D(b)\ll b(\log b)^2\).

theorem erdos_305.variants.bleicher_erdos : ∃ C : ℝ, 0 < C ∧
    ∀ᶠ b : ℕ in atTop, (Dmax b : ℝ) ≤ C * b * (log b) ^ 2

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/305.lean, line 76.

Erdos305.erdos_305.variants.prime_lower_bound

Solved: stated here without proof.

If \(b=p\) is a prime then \(D(p) \gg p\log p\).

theorem erdos_305.variants.prime_lower_bound : ∃ c : ℝ, 0 < c ∧
    ∀ᶠ p : ℕ in atTop, p.Prime → c * p * log p ≤ Dmax p

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/305.lean, line 82.

Erdos305.erdos_305.variants.yokota

Solved: stated here without proof.

Yokota [Yo88] proved that \(D(b)\ll b(\log b)(\log\log b)^4(\log\log\log b)^2\).

theorem erdos_305.variants.yokota : ∃ C : ℝ, 0 < C ∧ ∀ᶠ b : ℕ in atTop,
    (Dmax b : ℝ) ≤ C * b * log b * log (log b) ^ 4 * log (log (log b)) ^ 2

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/305.lean, line 90.

Erdos305.erdos_305.variants.liu_sawhney

Solved: stated here without proof.

Liu and Sawhney [LiSa24] proved that \(D(b)\ll b(\log b)(\log\log b)^3(\log\log\log b)^{O(1)}\).

theorem erdos_305.variants.liu_sawhney : ∃ C K : ℝ, 0 < C ∧ ∀ᶠ b : ℕ in atTop,
    (Dmax b : ℝ) ≤ C * b * log b * log (log b) ^ 3 * log (log (log b)) ^ K

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/305.lean, line 98.

Sources

• FormalConjectures/ErdosProblems/305.lean at 2055e5ad
• erdosproblems.com/305

LeanErdos305.erdos_305 · Erdos305.erdos_305.variants.bleicher_erdos · Erdos305.erdos_305.variants.prime_lower_bound · Erdos305.erdos_305.variants.yokota · Erdos305.erdos_305.variants.liu_sawhney

TheoremErdős Problem 306#

References: - erdosproblems.com/306 - [Li26] S. Li, Unit fractions with semiprime denominators: an elementary proof of Erdős Problem 306. arXiv:2609.32140 (2026). - [Ta26] Tang, Yuren, A Lean 4 formalisation of Erdős Problem 306, a proof modulo two Rosser–Schoenfeld axioms.

Quoted from FormalConjectures/ErdosProblems/306.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/306.

The file states 2 research or textbook statements: 2 solved.

Erdos306.erdos_306

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/e1a5e2a3317007f0e31b98bf2e80383187b31238/erdos-306/Solution.lean#L34.

Let \(\frac a b\in \mathbb{Q}_{>0}\) with \(b\) squarefree. Are there integers \(1 < n_1 < \dots < n_k\), each the product of two distinct primes, such that \(\frac{a}{b}=\frac{1}{n_1}+\cdots+\frac{1}{n_k}\)?

The answer is yes [Li26].

theorem erdos_306 : ∀ (q : ℚ), 0 < q → Squarefree q.den →
    ∃ k : ℕ, ∃ (n : Fin (k + 1) → ℕ), n 0 = 1 ∧ StrictMono n ∧
    (∀ i ∈ Finset.Icc 1 (Fin.last k), ω (n i) = 2 ∧ Ω (n i) = 2) ∧
    q = ∑ i ∈ Finset.Icc 1 (Fin.last k), (1 : ℚ) / (n i)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/306.lean, line 48.

Erdos306.erdos_306.variants.integer_three_primes

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/e1a5e2a3317007f0e31b98bf2e80383187b31238/erdos-306/Solution.lean#L48.

Every positive integer can be expressed as an Egyptian fraction where each denominator is the product of three distinct primes.

theorem erdos_306.variants.integer_three_primes (m : ℕ) (h : 0 < m) :
    ∃ k > (0 : ℕ), ∃ (n : Fin (k + 1) → ℕ), n 0 = 1 ∧
    ∀ i, (hik : i < k) → n ⟨i, by omega⟩ < n ⟨(i + 1), by omega⟩ ∧
    (∀ i ∈ Finset.Icc 1 (Fin.last k), ω (n i) = 3 ∧ Ω (n i) = 3) ∧
    m = ∑ i ∈ Finset.Icc 1 (Fin.last k), (1 : ℚ) / (n i)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/306.lean, line 61.

Sources

• FormalConjectures/ErdosProblems/306.lean at 2055e5ad
• erdosproblems.com/306

LeanErdos306.erdos_306 · Erdos306.erdos_306.variants.integer_three_primes

TheoremErdős Problem 307#

Reference: erdosproblems.com/307

Quoted from FormalConjectures/ErdosProblems/307.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/307.

The file states 5 research or textbook statements: 2 open, 2 solved and 1 textbook result.

Erdos307.erdos_307

Open: stated without proof.

Are there two finite set of primes \(P\) and \(Q\) such that

\[ 1 = \left( \sum_{p \in P} \frac{1}{p} \right) \left( \sum_{q \in Q} \frac{1}{q} \right) \]

?

Asked by Barbeau [Ba76].

[Ba76] Barbeau, E. J., Computer challenge corner: Problem 477: A brute force program.

theorem erdos_307 : ∃ P Q : Finset ℕ, (∀ p ∈ P, p.Prime) ∧ (∀ q ∈ Q, q.Prime) ∧
    1 = (∑ p ∈ P, (p : ℚ)⁻¹) * (∑ q ∈ Q, (q : ℚ)⁻¹)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/307.lean, line 45.

Erdos307.erdos_307.variants.coprime

Textbook result, proved here.

Instead of asking for sets of primes, ask only that all elements in the sets be relatively coprime.

Cambie has found several examples when this weakened version is true. For example,

\[ 1=\left(1+\frac{1}{5}\right)\left(\frac{1}{2}+\frac{1}{3}\right) \]

and

\[ 1=\left(1+\frac{1}{41}\right)\left(\frac{1}{2}+\frac{1}{3}+\frac{1}{7}\right). \]

theorem erdos_307.variants.coprime : ∃ P Q : Finset ℕ, 0 ∉ P ∩ Q ∧ 1 < #P ∧ 1 < #Q ∧
    Set.Pairwise P Nat.Coprime ∧ Set.Pairwise Q Nat.Coprime ∧
    1 = (∑ p ∈ P, (p : ℚ)⁻¹) * (∑ q ∈ Q, (q : ℚ)⁻¹)

Category textbook; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/307.lean, line 62.

Erdos307.erdos_307.variants.coprime_one_notMem

Open: stated without proof.

There are no examples known of the weakened coprime version if we insist that \(1\not\in P\cup Q\).

theorem erdos_307.variants.coprime_one_notMem : ∃ P Q : Finset ℕ, 0 ∉ P ∩ Q ∧ 1 ∉ P ∪ Q ∧
    1 < #P ∧ 1 < #Q ∧ Set.Pairwise P Nat.Coprime ∧ Set.Pairwise Q Nat.Coprime ∧
    1 = (∑ p ∈ P, (p : ℚ)⁻¹) * (∑ q ∈ Q, (q : ℚ)⁻¹)

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/307.lean, line 73.

Erdos307.erdos_307.barrier

Solved: stated here; a Lean proof is at https://github.com/ElVec1o/erdos307/blob/76d242b024102f32d8411c714be4ad140a8b7c4b/lean/Erdos307/Closed.lean#L121.

A machine-checked barrier for Erdős 307 (Bonfioli, 2026): any solution with Q nonempty uses at least 59 primes in total, and (∏_{p ∈ P} p)² ≥ 4·10¹¹² — i.e. ∏_{p ∈ P} p ≥ 2·10⁵⁶ (and, by symmetry, the same for ∏ Q); so no solution lies below a prime-product of 2.09·10⁵⁶. The full sorry-free proof is in the linked repository (Closed.lean): the left conjunct is card_ge_59, the right is erdos307_barrier_closed. Both depend on propext, Classical.choice, Quot.sound and nothing further: the evaluation of the first 59 primes is kernel-checked by decide, so no native_decide enters this statement.

theorem erdos_307.barrier {P Q : Finset ℕ}
    (hP : ∀ p ∈ P, p.Prime) (hQ : ∀ q ∈ Q, q.Prime) (hQne : Q.Nonempty)
    (heq : 1 = (∑ p ∈ P, (p : ℚ)⁻¹) * (∑ q ∈ Q, (q : ℚ)⁻¹)) :
    59 ≤ #(P ∪ Q) ∧ (4 * 10 ^ 112 : ℚ) ≤ (∏ p ∈ P, (p : ℚ)) ^ 2

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/307.lean, line 90.

Erdos307.erdos_307.barrier_sixty

Solved: stated here; a Lean proof is at https://github.com/ElVec1o/erdos307/blob/080164a8db2eeb20f65c362894ec93f12448609a/lean/Erdos307/Sixty.lean#L367.

A stronger machine-checked barrier (Bonfioli, 2026), closing the 59-prime level: any solution of Erdős 307 in fact uses at least 60 primes in total. The full sorry-free proof is erdos307_sixty in the linked repository (Sixty.lean at tag v1.1.1); its only non-logical input is a native_decide depth-first search establishing that no admissible 59-prime support survives the Pythagorean plus-value square test, with axioms propext, Classical.choice, Quot.sound together with that native_decide.

theorem erdos_307.barrier_sixty {P Q : Finset ℕ}
    (hP : ∀ p ∈ P, p.Prime) (hQ : ∀ q ∈ Q, q.Prime)
    (heq : 1 = (∑ p ∈ P, (p : ℚ)⁻¹) * (∑ q ∈ Q, (q : ℚ)⁻¹)) :
    60 ≤ #(P ∪ Q)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/307.lean, line 107.

Sources

• FormalConjectures/ErdosProblems/307.lean at 2055e5ad
• erdosproblems.com/307

LeanErdos307.erdos_307 · Erdos307.erdos_307.variants.coprime · Erdos307.erdos_307.variants.coprime_one_notMem · Erdos307.erdos_307.barrier · Erdos307.erdos_307.barrier_sixty

TheoremErdős Problem 308#

References: - erdosproblems.com/308 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Cr99] Croot, III, Ernest S., On some questions of Erdős and Graham about Egyptian fractions. Mathematika (1999), 359-372.

Quoted from FormalConjectures/ErdosProblems/308.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/308.

The file states 5 research or textbook statements: 1 open and 4 solved.

Erdos308.erdos_308.parts.i

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos308.lean#L458.

Let \(N\geq 1\). What is the smallest integer not representable as the sum of distinct unit fractions with denominators from \(\{1,\ldots,N\}\)?

This was essentially solved by Croot [Cr99] (see erdos_308.variants.croot); in particular, for all sufficiently large \(N\), the smallest such integer is either \(m_N\) or \(m_N+1\), where \(m_N=\lfloor \sum_{n\leq N}\frac{1}{n}\rfloor\).

theorem erdos_308.parts.i : ∀ᶠ N : ℕ in atTop, f N = m N ∨ f N = m N + 1

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/308.lean, line 64.

Erdos308.erdos_308.parts.ii

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos308.lean#L458.

Let \(N\geq 1\). Is it true that the set of integers representable as the sum of distinct unit fractions with denominators from \(\{1,\ldots,N\}\) has the shape \(\{1,\ldots,m\}\) for some \(m\)?

It follows from Croot's bounds [Cr99] that this holds for all sufficiently large \(N\).

theorem erdos_308.parts.ii :
    ∀ᶠ N : ℕ in atTop, ∃ m, representable N = Set.Icc 1 m

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/308.lean, line 76.

Erdos308.erdos_308.variants.shape

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos308.lean#L458.

If \(m_N=\lfloor \sum_{n\leq N}\frac{1}{n}\rfloor\), then the set of integers representable is, for all \(N\) sufficiently large, either \(\{1,\ldots,m_N-1\}\) or \(\{1,\ldots,m_N\}\).

theorem erdos_308.variants.shape : ∀ᶠ N : ℕ in atTop,
    representable N = Set.Icc 1 (m N - 1) ∨ representable N = Set.Icc 1 (m N)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/308.lean, line 87.

Erdos308.erdos_308.variants.croot

Solved: stated here without proof.

Croot [Cr99] bounded \(\eta(N)\), the largest integer such that every integer in \(\{1,\ldots,\eta(N)\}\) is representable; this is \(f(N)-1\), so his bounds read

\[\left\lfloor\sum_{n\leq N}\frac{1}{n}-\frac{9}{2}(1+o(1))\frac{(\log\log N)^2}{\log N} \right\rfloor + 1 \leq f(N)\]

and

\[f(N)\leq \left\lfloor\sum_{n\leq N}\frac{1}{n}-\frac{1}{2}(1+o(1)) \frac{(\log\log N)^2}{\log N}\right\rfloor + 1.\]

theorem erdos_308.variants.croot :
    ∃ o₁ o₂ : ℕ → ℝ, Tendsto o₁ atTop (nhds 0) ∧ Tendsto o₂ atTop (nhds 0) ∧
      ∀ᶠ N : ℕ in atTop,
        ⌊(harmonic N : ℝ) - 9 / 2 * (1 + o₁ N) * (log (log N)) ^ 2 / log N⌋₊ + 1 ≤ f N ∧
        f N ≤ ⌊(harmonic N : ℝ) - 1 / 2 * (1 + o₂ N) * (log (log N)) ^ 2 / log N⌋₊ + 1

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/308.lean, line 101.

Erdos308.erdos_308.variants.all_N

Open: stated without proof.

Is it true that, for every \(N\geq 1\), the set of integers representable as the sum of distinct unit fractions with denominators from \(\{1,\ldots,N\}\) has the shape \(\{1,\ldots,m\}\) for some \(m\)?

theorem erdos_308.variants.all_N :
    ∀ N ≥ 1, ∃ m, representable N = Set.Icc 1 m

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/308.lean, line 114.

Sources

• FormalConjectures/ErdosProblems/308.lean at 2055e5ad
• erdosproblems.com/308

LeanErdos308.erdos_308.parts.i · Erdos308.erdos_308.parts.ii · Erdos308.erdos_308.variants.shape · Erdos308.erdos_308.variants.croot · Erdos308.erdos_308.variants.all_N

TheoremErdős Problem 309#

References: - erdosproblems.com/309 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Yo97] Yokota, Hisashi, On number of integers representable as a sum of unit fractions. II. J. Number Theory (1997), 162--169. - [Cr99] Croot, III, Ernest S., On some questions of Erdős and Graham about Egyptian fractions. Mathematika (1999), 359-372. - [Yo02] Yokota, Hisashi, On the number of integers representable as sums of unit fractions. III. J. Number Theory (2002), 351--372.

Quoted from FormalConjectures/ErdosProblems/309.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/309.

The file states 2 research or textbook statements: 2 solved.

Erdos309.erdos_309

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos309.lean#L374.

Let \(N\geq 1\). How many integers can be written as the sum of distinct unit fractions with denominators from \(\{1,\ldots,N\}\)? Are there \(o(\log N)\) such integers?

If the number of such integers is \(N(n)\) then it is trivial that \(N(n)\leq \log n+O(1)\). Yokota [Yo97] proved that \(N(n)\geq \log n-O(\log\log n)\).

Croot [Cr99] proved that every integer at most

\[\leq \sum_{n\leq N}\frac{1}{n}-(\tfrac{9}{2}+o(1))\frac{(\log\log N)^2}{\log N}\]

can be so represented.

If \(F(N)\) counts the number of integers which can be represented in this fashion, then the current best lower bound known is

\[F(N) \geq \log N+\gamma -\left(\frac{\pi^2}{3}+o(1)\right)\frac{(\log\log N)^2}{\log N}\]

due to Yokota [Yo02].

The answer to the question is no: \(F(N) \sim \log N\). Here \(0\) (the empty sum) is counted.

theorem erdos_309 :
    ¬ (fun N : ℕ => (F N : ℝ)) =o[atTop] fun N : ℕ => Real.log N

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/309.lean, line 67.

Erdos309.erdos_309.variants.asymptotic

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos309.lean#L374.

The number of representable integers satisfies \(F(N) \sim \log N\).

theorem erdos_309.variants.asymptotic :
    Tendsto (fun N : ℕ => (F N : ℝ) / Real.log N) atTop (𝓝 1)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/309.lean, line 75.

Sources

• FormalConjectures/ErdosProblems/309.lean at 2055e5ad
• erdosproblems.com/309

LeanErdos309.erdos_309 · Erdos309.erdos_309.variants.asymptotic

TheoremErdős Problem 310#

References: - erdosproblems.com/310 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [LiSa24] Liu, Y. and Sawhney, M., On further questions regarding unit fractions. arXiv:2404.07113 (2024). - [Bl21] Bloom, T. F., On a density conjecture about unit fractions. arXiv:2112.03726 (2021).

Quoted from FormalConjectures/ErdosProblems/310.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/310.

The file states 2 research or textbook statements: 2 solved.

Erdos310.erdos_310

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos310.lean#L240.

Let \(\alpha >0\) and \(N\geq 1\). Is it true that for any \(A\subseteq \{1,\ldots,N\}\) with \(\lvert A\rvert \geq \alpha N\) there exists some \(S\subseteq A\) such that

\[\frac{a}{b}=\sum_{n\in S}\frac{1}{n}\]

with \(a\leq b =O_\alpha(1)\)?

Liu and Sawhney [LiSa24] observed that the main result of Bloom [Bl21] implies a positive solution to this conjecture. They prove a more precise version, that if \((\log N)^{-1/7+o(1)}\leq \alpha \leq 1/2\) then there is some \(S\subseteq A\) such that \(\frac{a}{b}=\sum_{n\in S}\frac{1}{n}\) with \(a\leq b \leq \exp(O(1/\alpha))\). They also observe that the dependence \(b\leq \exp(O(1/\alpha))\) is sharp.

theorem erdos_310 : ∀ α : ℝ, 0 < α → ∃ C : ℕ, ∀ N : ℕ, 1 ≤ N →
    ∀ A ⊆ Finset.Icc 1 N, α * N ≤ A.card →
      ∃ S ⊆ A, ∃ a b : ℕ, 0 < a ∧ a ≤ b ∧ b ≤ C ∧ ∑ n ∈ S, (1 / n : ℚ) = a / b

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/310.lean, line 51.

Erdos310.erdos_310.variants.liu_sawhney

Solved: stated here without proof.

Liu and Sawhney [LiSa24] proved that if \((\log N)^{-1/7+o(1)}\leq \alpha \leq 1/2\) then there is some \(S\subseteq A\) such that \(\frac{a}{b}=\sum_{n\in S}\frac{1}{n}\) with \(a\leq b \leq \exp(O(1/\alpha))\).

theorem erdos_310.variants.liu_sawhney : ∃ C : ℝ, ∀ ε : ℝ, 0 < ε → ∀ᶠ N : ℕ in Filter.atTop,
    ∀ α : ℝ, Real.log N ^ (-(1 / 7 : ℝ) + ε) ≤ α → α ≤ 1 / 2 →
      ∀ A ⊆ Finset.Icc 1 N, α * N ≤ A.card →
        ∃ S ⊆ A, ∃ a b : ℕ, 0 < a ∧ a ≤ b ∧ (b : ℝ) ≤ Real.exp (C / α) ∧
          ∑ n ∈ S, (1 / n : ℚ) = a / b

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/310.lean, line 62.

Sources

• FormalConjectures/ErdosProblems/310.lean at 2055e5ad
• erdosproblems.com/310

LeanErdos310.erdos_310 · Erdos310.erdos_310.variants.liu_sawhney

TheoremErdős Problem 311#

References: - erdosproblems.com/311 - [ErGr80] P. Erdős and R. L. Graham, Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique (1980), p. 40.

Quoted from FormalConjectures/ErdosProblems/311.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/311.

The file states 3 research or textbook statements: 1 open and 2 textbook results. It also has 1 test statement, counted here but not shown.

Erdos311.erdos_311

Open: stated without proof.

Let \(\delta(N)\) be the minimal non-zero value of \(\lvert 1-\sum_{n\in A}\frac{1}{n}\rvert\) as \(A\) ranges over all subsets of \(\{1,\ldots,N\}\). Is it true that

\[\delta(N)=e^{-(c+o(1))N}\]

for some constant \(c\in (0,1)\)?

The formulation in [ErGr80] has the additional condition that \(A\) contains no \(S\) with \(\sum_{n\in S}\frac{1}{n}=1\); Kovac (in the comments on the problem page) showed that the formulation above is equivalent. We state \(\delta(N)=e^{-(c+o(1))N}\) as \(-\log \delta(N) / N \to c\).

theorem erdos_311 :
    ∃ c ∈ Set.Ioo (0 : ℝ) 1,
      Tendsto (fun N : ℕ => -Real.log (delta N) / N) atTop (𝓝 c)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/311.lean, line 55.

Erdos311.delta_ge_inv_lcm

Textbook result, stated without proof.

The trivial lower bound: every non-zero value of \(1 - \sum_{n \in A} 1/n\) is a non-zero rational with denominator dividing \([1, \ldots, N]\), so \(\delta(N) \geq 1/[1,\ldots,N]\).

theorem delta_ge_inv_lcm (N : ℕ) : 1 / (((Icc 1 N).lcm id : ℕ) : ℝ) ≤ delta N

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/311.lean, line 65.

Erdos311.delta_ge_exp

Textbook result, stated without proof.

Since \([1, \ldots, N] = e^{(1+o(1))N}\), the trivial bound gives \(\delta(N) \ge e^{-(1+o(1))N}\).

theorem delta_ge_exp : ∀ ε > 0, ∀ᶠ N : ℕ in atTop, Real.exp (-(1 + ε) * N) ≤ delta N

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/311.lean, line 70.

Sources

• FormalConjectures/ErdosProblems/311.lean at 2055e5ad
• erdosproblems.com/311

LeanErdos311.erdos_311 · Erdos311.delta_ge_inv_lcm · Erdos311.delta_ge_exp

TheoremErdős Problem 312#

Reference: erdosproblems.com/312

Quoted from FormalConjectures/ErdosProblems/312.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/312.

The file states 1 research or textbook statement: 1 open.

Erdos312.erdos_312

Open: stated without proof.

Does there exist a constant c > 0 such that, for any K > 1, whenever A is a sufficiently large finite multiset of integers with \(\sum_{n \in A} 1/n > K\) there exists some \(S \subseteq A\) such that \(1 - \exp(-(c*K)) < \sum_{n \in S} 1/n \le 1\)?

theorem erdos_312 :
    ∃ (c : ℝ), 0 < c ∧
      ∀ (K : ℝ), 1 < K →
        ∃ (N₀ : ℕ),
          ∀ (n : ℕ) (a : Fin n → ℕ),
            (n ≥ N₀ ∧ (∑ i : Fin n, (a i : ℝ)⁻¹) > K) →
              ∃ (S : Finset (Fin n)),
                1 - Real.exp (-(c * K)) < (∑ i ∈ S, (a i : ℝ)⁻¹) ∧
                ∑ i ∈ S, (a i : ℝ)⁻¹ ≤ 1

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/312.lean, line 36.

Sources

• FormalConjectures/ErdosProblems/312.lean at 2055e5ad
• erdosproblems.com/312

LeanErdos312.erdos_312

TheoremErdős Problem 313#

References: - erdosproblems.com/313 - A54377 (Primary pseudoperfect numbers)

Quoted from FormalConjectures/ErdosProblems/313.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/313.

The file states 3 research or textbook statements: 2 open and 1 textbook result. It also has 2 test statements, counted here but not shown.

Erdos313.erdos_313

Open: stated without proof.

Are there infinitely many pairs (m, P) where m ≥ 2 is an integer and P is a set of distinct primes such that the following equation holds: \(\sum_{p \in P} \frac{1}{p} = 1 - \frac{1}{m}\)?

theorem erdos_313 : erdos313Solutions.Infinite

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/313.lean, line 46.

Erdos313.erdos_313.variants.primary_pseudoperfect_are_infinite

Open: stated without proof.

It is conjectured that the set of primary pseudoperfect numbers is infinite.

theorem erdos_313.variants.primary_pseudoperfect_are_infinite :
    Set.Infinite {n | IsPrimaryPseudoperfect n}

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/313.lean, line 67.

Erdos313.erdos_313.variants.exists_at_least_eight_primary_pseudoperfect

Textbook result, proved here.

There are at least 8 primary pseudoperfect numbers. The first eight terms of A54377 are exhibited together with their explicit prime decompositions.

theorem erdos_313.variants.exists_at_least_eight_primary_pseudoperfect :
    8 ≤ (Set.encard {n | IsPrimaryPseudoperfect n})

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/313.lean, line 77.

Sources

• FormalConjectures/ErdosProblems/313.lean at 2055e5ad
• erdosproblems.com/313

LeanErdos313.erdos_313 · Erdos313.erdos_313.variants.primary_pseudoperfect_are_infinite · Erdos313.erdos_313.variants.exists_at_least_eight_primary_pseudoperfect

TheoremErdős Problem 314#

References: - erdosproblems.com/314 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [LiSt24] J. Lim and Steinerberger, S., On differences of two harmonic numbers. arXiv:2405.11354 (2024).

Quoted from FormalConjectures/ErdosProblems/314.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/314.

The file states 1 research or textbook statement: 1 solved.

Erdos314.erdos_314

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos314.lean.

Let \(n\geq 1\) and let \(m\) be minimal such that \(\sum_{n\leq k\leq m}\frac{1}{k}\geq 1\). We define

\[\epsilon(n) = \sum_{n\leq k\leq m}\frac{1}{k}-1.\]

How small can \(\epsilon(n)\) be? Is it true that

\[\liminf n^2\epsilon(n)=0?\]

This is true, and shown by Lim and Steinerberger [LiSt24], who further proved that, for any \(\delta>0\), there exist infinitely many \(n\) and \(m\) such that

\[n^2\left\lvert \sum_{n\leq k\leq m}\frac{1}{k}-1\right\rvert\ll \frac{1}{(\log n)^{5/4-\delta}}.\]

Erdős and Graham (and also Lim and Steinerberger) believe that the exponent of \(2\) is best possible here, in that \(\liminf \epsilon(n) n^{2+\delta}=\infty\) for all \(\delta>0\).

theorem erdos_314 :
    atTop.liminf (fun n : ℕ => (n : ℝ) ^ 2 * epsilon n) = 0

Category research solved; AMS 11 Number theory, 40 Sequences, series, summability. Declared in FormalConjectures/ErdosProblems/314.lean, line 59.

Sources

• FormalConjectures/ErdosProblems/314.lean at 2055e5ad
• erdosproblems.com/314

LeanErdos314.erdos_314

TheoremErdős Problem 315#

References: - erdosproblems.com/315 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Ka25] Y. Kamio, Asymptotic analysis of infinite decompositions of a unit fraction into unit fractions. arXiv:2503.02317 (2025). - [LiTa25] Z. Li and Q. Tang, On a conjecture of Erdős and Graham about the Sylvester's sequence. arXiv:2503.12277 (2025).

Quoted from FormalConjectures/ErdosProblems/315.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/315.

The file states 1 research or textbook statement: 1 solved.

Erdos315.erdos_315

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos315.lean.

Let \(u_1=1\) and \(u_{n+1}=u_n(u_n+1)\), so that \(\sum_{k\geq 1}\frac{1}{u_k+1}\) and \(u_k=\lfloor c_0^{2^k}+1\rfloor\) for \(k\geq 1\), where

\[c_0=\lim u_n^{1/2^n}=1.264085\cdots.\]

Let $a_1\lt a_2\lt \cdots $ be any other sequence with \(\sum \frac{1}{a_k}=1\). Is it true that

\[\liminf a_n^{1/2^n}\lt c_0=1.264085\cdots?\]

This is true, and was proved independently by Kamio [Ka25] and Li and Tang [LiTa25].

An earlier interpretation of this question on this site defined \(u_1=2\) and \(u_{n+1}=u_n^2-u_n+1\) (Sylvester's sequence), which is the same sequence shifted by \(1\); we use the phrasing above as more faithful to [ErGr80]. The constant \(c_0\) is called the Vardi constant.

theorem erdos_315 :
    ∀ a : ℕ → ℕ, (∀ i, 0 < a i) → StrictMono a → (∃ i, a i ≠ u i + 1) →
      ∑' i, (1 : ℝ) / a i = 1 →
      atTop.liminf (fun i => (a i : ℝ) ^ ((1 / 2 : ℝ) ^ (i + 1))) < c₀

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/315.lean, line 66.

Sources

• FormalConjectures/ErdosProblems/315.lean at 2055e5ad
• erdosproblems.com/315

LeanErdos315.erdos_315

TheoremErdős Problem 316#

References: - erdosproblems.com/316 - [Sa97] Sándor, Csaba, On a problem of Erdős. J. Number Theory (1997), 203-210.

Quoted from FormalConjectures/ErdosProblems/316.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/316.

The file states 3 research or textbook statements: 2 solved and 1 textbook result.

Erdos316.erdos_316

Proved here.

Is it true that if \(A \subseteq \mathbb{N}\setminus\{1\}\) is a finite set with \(\sum_{n \in A} \frac{1}{n} < 2\) then there is a partition \(A=A_1 \sqcup A_2\) such that \(\sum_{n \in A_i} \frac{1}{n} < 1\) for \(i=1,2\)?

This is not true in general, as shown by Sándor [Sa97].

The minimal counterexample is \(\{2,3,4,5,6,7,10,11,13,14,15\}\), found by Tom Stobart.

This was formalized in Lean by Mehta.

theorem erdos_316 : ¬ ∀ A : Finset ℕ, 0 ∉ A → 1 ∉ A →
    ∑ n ∈ A, (1 / n : ℚ) < 2 → ∃ (A₁ A₂ : Finset ℕ),
      Disjoint A₁ A₂ ∧ A = A₁ ∪ A₂ ∧
      ∑ n ∈ A₁, (1 / n : ℚ) < 1 ∧ ∑ n ∈ A₂, (1 / n : ℚ) <  1

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/316.lean, line 44.

Erdos316.erdos_316.variants.multiset

Textbook result, proved here.

This is not true if \(A\) is a multiset, for example \(2,3,3,5,5,5,5\).

lemma erdos_316.variants.multiset : ∃ A : Multiset ℕ, 0 ∉ A ∧ 1 ∉ A ∧
    (A.map ((1 : ℚ) / ·)).sum < 2 ∧ ∀ (A₁ A₂ : Multiset ℕ),
      A = A₁ + A₂ →
        1 ≤ (A₁.map ((1 : ℚ) / ·)).sum ∨ 1 ≤ (A₂.map ((1 : ℚ) / ·)).sum

Category textbook; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/316.lean, line 59.

Erdos316.erdos_316.variants.generalized

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_Erdos316_erdos_316_variants_generalized.lean#L252.

This is not true in general, as shown by Sándor [Sa97], who observed that the proper divisors of \(120\) form a counterexample. More generally, Sándor shows that for any \(n\geq 2\) there exists a finite set \(A\subseteq \mathbb{N}\backslash\{1\}\) with \(\sum_{k\in A}\frac{1}{k} < n\) and no partition into \(n\) parts each of which has \(\sum_{k\in A_i}\frac{1}{k}<1\).

A Finpartition has no empty parts, so partitions into at most \(n\) parts are tested. Testing exactly \(n\) parts would let the singleton \(\{2\}\) satisfy the statement vacuously.

theorem erdos_316.variants.generalized (n : ℕ) (hn : 2 ≤ n) : ∃ A : Finset ℕ,
    A.Nonempty ∧ 0 ∉ A ∧ 1 ∉ A ∧ ∑ k ∈ A, (1 / k : ℚ) < n ∧ ∀ P : Finpartition A,
    P.parts.card ≤ n → ∃ p ∈ P.parts, 1 ≤ ∑ n ∈ p, (1 / n : ℚ)

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/316.lean, line 85.

Sources

• FormalConjectures/ErdosProblems/316.lean at 2055e5ad
• erdosproblems.com/316

LeanErdos316.erdos_316 · Erdos316.erdos_316.variants.multiset · Erdos316.erdos_316.variants.generalized

TheoremErdős Problem 317#

Reference: erdosproblems.com/317

Quoted from FormalConjectures/ErdosProblems/317.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/317.

The file states 4 research or textbook statements: 2 open and 2 textbook results.

Erdos317.erdos_317

Open: stated without proof.

Is there some constant \(c>0\) such that for every \(n\geq 1\) there exists some \(\delta_k\in \{-1,0,1\}\) for \(1\leq k\leq n\) with

\[0< \left\lvert \sum_{1\leq k\leq n}\frac{\delta_k}{k}\right\rvert < \frac{c}{2^n}?\]

theorem erdos_317 :
    ∃ c > 0, ∀ n ≥ 1, ∃ δ : Fin n → ℚ,
      Set.range δ ⊆ {-1, 0, 1} ∧
      letI lhs : ℝ := |∑ k, (δ k) / (k + 1)|
      0 < lhs ∧ lhs < c / 2^n

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/317.lean, line 37.

Erdos317.erdos_317.variants.claim2

Open: stated without proof.

Is it true that for sufficiently large \(n\), for any \(\delta_k\in \{-1,0,1\}\),

\[\left\lvert \sum_{1\leq k\leq n}\frac{\delta_k}{k}\right\rvert > \frac{1}{[1,\ldots,n]}\]

whenever the left-hand side is not zero?

theorem erdos_317.variants.claim2 :
    ∀ᶠ n in atTop, ∀ δ : (Fin n) → ℚ, δ '' Set.univ ⊆ {-1,0,1} →
    letI lhs := |∑ k, ((δ k : ℚ) / (k + 1))|
    lhs ≠ 0 → lhs > 1 / (Icc 1 n).lcm id

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/317.lean, line 50.

Erdos317.claim2_inequality

Textbook result, stated without proof.

Inequality in erdos_317.variants.claim2 is obvious, the problem is strict inequality.

lemma claim2_inequality : ∀ᶠ n in atTop,
    ∀ δ : (Fin n) → ℚ, δ '' Set.univ ⊆ {-1,0,1} →
    letI lhs := |∑ k, ((δ k : ℚ) / (k + 1))|
    lhs ≠ 0 → lhs ≥ 1 / (Icc 1 n).lcm id

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/317.lean, line 60.

Erdos317.erdos_317.variants.counterexample

Textbook result, proved here.

erdos_317.variants.claim2 fails for small \(n\), for example

\[\frac{1}{2}-\frac{1}{3}-\frac{1}{4}=-\frac{1}{12}.\]

theorem erdos_317.variants.counterexample : ¬ (∀  δ : (Fin 4) → ℚ, δ '' Set.univ ⊆ {-1,0,1} →
    letI lhs := |∑ k, ((δ k : ℚ) / (k + 1))|
    lhs ≠ 0 → lhs > (1 : ℚ) / ((Icc 1 4).lcm id : ℕ))

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/317.lean, line 71.

Sources

• FormalConjectures/ErdosProblems/317.lean at 2055e5ad
• erdosproblems.com/317

LeanErdos317.erdos_317 · Erdos317.erdos_317.variants.claim2 · Erdos317.claim2_inequality · Erdos317.erdos_317.variants.counterexample

TheoremErdős Problem 318#

References: - erdosproblems.com/318 - [ErSt75] Erdős, P. and Straus, E. G., Solution to Problem 387. Nieuw Arch. Wisk. (1975), 183. - [Sa75] Sattler, R., Solution to Problem 387. Nieuw Arch. Wisk. (1975), 184-189. - [Sa82b] Sattler, R., On Erdős property P₁ for the arithmetical sequence. Nederl. Akad. Wetensch. Indag. Math. (1982), 347--352. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [La26] D. Larsen, Erdős problem 318 (2026)

Quoted from FormalConjectures/ErdosProblems/318.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/318.

The file states 6 research or textbook statements: 6 solved. It also has 1 test statement, counted here but not shown.

Erdos318.erdos_318.variants.univ

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos318.lean#L761.

ℕ has property P₁. This is proved in [ErSt75].

theorem erdos_318.variants.univ : P₁ univ

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/318.lean, line 53.

Erdos318.erdos_318.variants.odd

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos318.lean#L782.

Sattler proved in [Sa75] that the set of odd numbers has property P₁.

theorem erdos_318.variants.odd : P₁ {n | Odd n}

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/318.lean, line 60.

Erdos318.erdos_318.variants.contain_single_even

Solved: stated here without proof.

For any infinite set A containing exactly one positive even number, A does not have property P₁. Sattler [Sa82] credits this observation to Erdős, who presumably found this after [ErGr80]. The element 0 is not counted, since P₁ ignores it, and the infinitude hypothesis excludes degenerate sets such as {2}, on which P₁ holds vacuously.

theorem erdos_318.variants.contain_single_even {A : Set ℕ} (hA : A.Infinite)
    (hA' : {n | n ∈ A \ {0} ∧ Even n}.ncard = 1) : ¬ P₁ A

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/318.lean, line 114.

Erdos318.erdos_318.parts.i

Solved: stated here without proof.

There exists a set A with positive density that does not have property P₁.

TODO: prove this lemma by assuming erdos_318.contain_single_even.

The density sits in an existential, so HasPosDensity is the stronger reading here and weakening it to positive lower density would claim less, which is the opposite of the usual situation for Erdős' "positive density". It also costs nothing: by erdos_318.variants.contain_single_even a witness only needs exactly one even element, and the odd numbers together with one even number have density 1 / 2 on the nose.

theorem erdos_318.parts.i : ∃ A : Set ℕ, HasPosDensity A ∧ ¬ P₁ A

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/318.lean, line 127.

Erdos318.erdos_318.variants.infinite_AP

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos318.lean#L599.

Every infinite arithmetic progression has property P₁. This is proved in [Sa82b].

theorem erdos_318.variants.infinite_AP {A : Set ℕ} (hA : A.IsAPOfLength ⊤) : P₁ A

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/318.lean, line 134.

Erdos318.erdos_318.parts.ii

Solved: stated here without proof.

Does the set of squares excluding 1 have property P₁?

Larsen [La26] proved that this set does have property P₁.

theorem erdos_318.parts.ii : P₁ ({n | IsSquare n} \ {1})

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/318.lean, line 143.

Sources

• FormalConjectures/ErdosProblems/318.lean at 2055e5ad
• erdosproblems.com/318

LeanErdos318.erdos_318.variants.univ · Erdos318.erdos_318.variants.odd · Erdos318.erdos_318.variants.contain_single_even · Erdos318.erdos_318.parts.i · Erdos318.erdos_318.variants.infinite_AP · Erdos318.erdos_318.parts.ii

TheoremErdős Problem 319#

Reference: erdosproblems.com/319

Quoted from FormalConjectures/ErdosProblems/319.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/319.

The file states 3 research or textbook statements: 1 open and 2 solved.

Erdos319.erdos_319

Open: stated without proof.

What is the size of the largest \(A\subseteq\{1, \dots, N\}\) such that there is a function \(\delta : A \to \{-1, 1\}\) such that

\[ \sum_{n\in A} \frac{\delta n}{n} = 0 \]

and

\[ \sum_{n\in A'}\frac{\delta n}{n} \neq 0 \]

for all non-empty \(A'\subsetneq A\).

theorem erdos_319 (N : ℕ) : IsGreatest
    { #A | (A) (_ : A ⊆ Finset.Icc 1 N)
      (_ : ∃ δ : ℕ → ℤˣ, ∑ n ∈ A, (δ n : ℚ) / n = 0 ∧
        ∀ A' ⊂ A, A'.Nonempty → ∑ n ∈ A', (δ n : ℚ) / n ≠ 0) }
    erdos_319.answer

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/319.lean, line 47.

Erdos319.erdos_319.variants.isTheta

Solved: stated here without proof.

Let \(c(N)\) be the size of the largest \(A\subseteq\{1, \dots, N\}\) such that there is a function \(\delta : A \to \{-1, 1\}\) such that

\[ \sum_{n\in A} \frac{\delta n}{n} = 0 \]

and

\[ \sum_{n\in A'}\frac{\delta n}{n} \neq 0 \]

for all non-empty \(A'\subsetneq A\). What is \(\Theta(c(N))\)?

Trivially \(c(N) \leq N\), and erdos_319.variants.lb gives \(c(N) \geq (1 - \frac{1}{e} + o(1))N\), so \(c(N) = \Theta(N)\).

theorem erdos_319.variants.isTheta (N : ℕ) (c : ℕ → ℝ)
    (h : ∀ N, IsGreatest
    { (#A : ℝ) | (A) (_ : A ⊆ Finset.Icc 1 N)
      (_ : ∃ δ : ℕ → ℤˣ, ∑ n ∈ A, (δ n : ℚ) / n = 0 ∧
        ∀ A' ⊂ A, A'.Nonempty → ∑ n ∈ A', (δ n : ℚ) / n ≠ 0) } (c N)) :
    c =Θ[atTop] erdos_319.variants.isTheta.answer

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/319.lean, line 73.

Erdos319.erdos_319.variants.lb

Solved: stated here without proof.

Adenwalla has observed that a lower bound (on the maximum size of \(A\)) of

\[ |A| \geq (1 - \frac{1}{e} + o(1))N \]

follows from the main result of Croot [Cr01].

[Cr01] Croot, III, Ernest S., On unit fractions with denominators in short intervals. Acta Arith. (2001), 99-114.

theorem erdos_319.variants.lb : ∃ (o : ℕ → ℝ), (o =o[atTop] (1 : ℕ → ℝ)) ∧
    ∀ᶠ N in atTop, (1 - 1 / rexp 1 + o N) * N ≤ sSup { (#A : ℝ) | (A) (_ : A ⊆ Finset.Icc 1 N)
      (_ : ∃ δ : ℕ → ℤˣ, ∑ n ∈ A, (δ n : ℚ) / n = 0 ∧
        ∀ A' ⊂ A, A'.Nonempty → ∑ n ∈ A', (δ n : ℚ) / n ≠ 0) }

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/319.lean, line 91.

Sources

• FormalConjectures/ErdosProblems/319.lean at 2055e5ad
• erdosproblems.com/319

LeanErdos319.erdos_319 · Erdos319.erdos_319.variants.isTheta · Erdos319.erdos_319.variants.lb

TheoremErdős Problem 321#

Reference: erdosproblems.com/321

Quoted from FormalConjectures/ErdosProblems/321.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/321.

The file states 6 research or textbook statements: 4 open and 2 solved.

Erdos321.erdos_321

Open: stated without proof.

Let \(R(N)\) be the size of the largest \(A\subseteq\{1, ..., N\}\) such that all sums \(\sum_{n\in S} \frac{1}{n}\) are distinct for \(S\subseteq A\). What is \(R(N)\)?

theorem erdos_321 (N : ℕ) :
    R N = erdos_321.answer

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/321.lean, line 49.

Erdos321.erdos_321.variants.isTheta

Open: stated without proof.

Let \(R(N)\) be the size of the largest \(A\subseteq\{1, ..., N\}\) such that all sums \(\sum_{n\in S} \frac{1}{n}\) are distinct for \(S\subseteq A\). What is \(\Theta(R(N))\)?

theorem erdos_321.variants.isTheta :
    (fun N ↦ (R N : ℝ)) =Θ[atTop] erdos_321.variants.isTheta.answer

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/321.lean, line 69.

Erdos321.erdos_321.variants.isBigO

Open: stated without proof.

Let \(R(N)\) be the size of the largest \(A\subseteq\{1, ..., N\}\) such that all sums \(\sum_{n\in S} \frac{1}{n}\) are distinct for \(S\subseteq A\). Find the simplest \(g(N)\) such that \(R(N) = O(g(N))\).

theorem erdos_321.variants.isBigO :
    (fun N ↦ (R N : ℝ)) =O[atTop] erdos_321.variants.isBigO.answer

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/321.lean, line 79.

Erdos321.erdos_321.variants.isLittleO

Open: stated without proof.

Let \(R(N)\) be the size of the largest \(A\subseteq\{1, ..., N\}\) such that all sums \(\sum_{n\in S} \frac{1}{n}\) are distinct for \(S\subseteq A\). Find the simplest \(g(N)\) such that \(R(N) = o(g(N))\).

theorem erdos_321.variants.isLittleO :
    (fun N ↦ (R N : ℝ)) =o[atTop] erdos_321.variants.isLittleO.answer

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/321.lean, line 89.

Erdos321.erdos_321.variants.lower

Solved: stated here without proof.

Let \(R(N)\) be the maximal such size. Results of Bleicher and Erdős from [BlEr75] and [BlEr76b] imply that

\[ \frac{N}{\log N} \prod_{i=3}^{k} \log_i N \le R(N), \]

valid for any \(k \ge 4\) with \(\log_k N \ge k\) and any \(r \ge 1\) with \(\log_{2r} N \ge 1\). (In these bounds \(\log_i n\) denotes the \(i\)-fold iterated logarithm.)

[BlEr75] Bleicher, M. N. and Erdős, P., The number of distinct subsums of \(\sum \sb{1}\spN\,1/i\). Math. Comp. (1975), 29-42. [BlEr76b] Bleicher, Michael N. and Erdős, Paul, Denominators of Egyptian fractions. II. Illinois J. Math. (1976), 598-613.

theorem erdos_321.variants.lower (N k : ℕ) (hk : 4 ≤ k) (hkN : k ≤ log^[k] N) :
    N / log N * ∏ i ∈ Finset.Icc 3 k, (log^[i] N) ≤ R N

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/321.lean, line 104.

Erdos321.erdos_321.variants.upper

Solved: stated here without proof.

Let \(R(N)\) be the maximal such size. Results of Bleicher and Erdős from [BlEr75] and [BlEr76b] imply that

\[ R(N) \le \frac{1}{\log 2} \log_r N \left( \frac{N}{\log N} \prod_{i=3}^{r} \log_i N \right), \]

valid for any \(k \ge 4\) with \(\log_k N \ge k\) and any \(r \ge 1\) with \(\log_{2r} N \ge 1\). (In these bounds \(\log_i n\) denotes the \(i\)-fold iterated logarithm.)

Since Real.log is defined on all of \(\mathbb{R}\), the condition \(\log_{2r} N \ge 1\) is formalised as \(\log_i N \ge 1\) for all \(i \le 2r\), which is equivalent to it for the genuine iterated logarithm and ensures that every intermediate iterate is positive.

[BlEr75] Bleicher, M. N. and Erdős, P., The number of distinct subsums of \(\sum \sb{1}\spN\,1/i\). Math. Comp. (1975), 29-42. [BlEr76b] Bleicher, Michael N. and Erdős, Paul, Denominators of Egyptian fractions. II. Illinois J. Math. (1976), 598-613.

theorem erdos_321.variants.upper (N r : ℕ) (hr : 1 ≤ r) (hrN : ∀ i ≤ 2 * r, 1 ≤ log^[i] N) :
    R N ≤ 1 / log 2 * log^[r] N * N / log N * ∏ i ∈ Finset.Icc 3 r, (log^[i] N)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/321.lean, line 123.

Sources

• FormalConjectures/ErdosProblems/321.lean at 2055e5ad
• erdosproblems.com/321

LeanErdos321.erdos_321 · Erdos321.erdos_321.variants.isTheta · Erdos321.erdos_321.variants.isBigO · Erdos321.erdos_321.variants.isLittleO · Erdos321.erdos_321.variants.lower · Erdos321.erdos_321.variants.upper

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.