Problems 1200 to 1299
The Erdős problems numbered 1200 to 1299 that Formal Conjectures states, one article each.
TheoremErdős Problem 1201#
Reference: erdosproblems.com/1201
Quoted from FormalConjectures/ErdosProblems/1201.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/1201.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos1201.erdos_1201
Open: stated without proof.
Is it true that for every \(\epsilon,\eta>0\) there exists a \(k\) such that the density of \(n\) for which \(P(n(n+1)\cdots(n+k))>n^{1-\epsilon}\) is at least \(1-\eta\) (where \(P(m)\) is the greatest prime divisor of \(m\))?
theorem erdos_1201 :
∀ ε > 0, ∀ η > 0, ∃ k : ℕ,
atTop.liminf (fun x : ℕ ↦
(((count (· ∈ Erdos1201Set ε k) x : ℝ) / (x : ℝ)) : EReal)) ≥ (1 - η : EReal)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1201.lean, line 47.
Erdos1201.erdos_1201.variants.epsilon_half
Solved: stated here without proof.
Erdős wrote he could prove this for \(\epsilon=1/2\).
theorem erdos_1201.variants.epsilon_half :
∀ η > 0, ∃ k : ℕ,
atTop.liminf (fun x : ℕ ↦
(((count (· ∈ Erdos1201Set (1 / 2 : ℝ) k) x : ℝ) / (x : ℝ)) : EReal)) ≥ (1 - η : EReal)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1201.lean, line 58.
Sources
TheoremErdős Problem 1202#
References: - erdosproblems.com/1202 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [Gr24] Ben Green's 100 Open Problems, Problem 44
Quoted from FormalConjectures/ErdosProblems/1202.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/1202.
The file states 1 research or textbook statement: 1 solved.
Erdos1202.erdos_1202
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1202.lean.
Let \(\epsilon > 0\). Does there exist \(k\) such that, for every \(n\), any primes \(p_1 < \cdots < p_k < n^{1-\epsilon}\) and any sets \(A_i\) of \(\frac{p_i - 1}{2}\) residue classes modulo \(p_i\), the number of \(m \le n\) that avoid \(A_i \pmod{p_i}\) for every \(i\) is at most \(\epsilon n\)?
The answer is negative: according to erdosproblems.com/1202, Price (with GPT-5.4 Pro) gave a construction in which the \(A_i\) are intervals of residues and at least \((1/2 - c) n\) integers in \([1, n]\) survive. The large sieve gives a positive answer when \(p_k < n^{1/2}\) instead. See also
Green44for a related special case.
theorem erdos_1202 :
¬ ∀ ε : ℝ, 0 < ε → ∃ k : ℕ, ∀ (n : ℕ) (p : Fin k → ℕ) (A : (i : Fin k) → Finset (ZMod (p i))),
(∀ i, (p i).Prime) →
StrictMono p →
(∀ i, (p i : ℝ) < (n : ℝ) ^ (1 - ε)) →
(∀ i, (A i).card = (p i - 1) / 2) →
((((Finset.Icc 1 n).filter (fun m => ∀ i, (m : ZMod (p i)) ∉ A i)).card : ℕ) : ℝ) ≤ ε * n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1202.lean, line 48.
Sources
TheoremErdős Problem 1203#
References: - erdosproblems.com/1203
Quoted from FormalConjectures/ErdosProblems/1203.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/1203.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos1203.erdos_1203
Open: stated without proof.
Prove that \(F(n)\to \infty\) as \(n\to \infty\).
theorem erdos_1203 :
Tendsto F atTop atTop
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1203.lean, line 45.
Erdos1203.erdos_1203.variants.lower_bound
Solved: stated here without proof.
It is easy to prove that \(F(n)\geq 1-o(1)\).
theorem erdos_1203.variants.lower_bound :
∀ ε > 0, ∀ᶠ n in atTop, F n ≥ 1 - ε
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1203.lean, line 53.
Sources
TheoremErdős Problem 1204#
References: - erdosproblems.com/1204 - [El65] Elliott, P. D. T. A., On sequences of integers. Quart. J. Math. Oxford Ser. (2) 16 (1965), 35-45. - [Er80] Erdős, P., A survey of problems in combinatorial number theory. Ann. Discrete Math. 6 (1980), 89-115. - [Po14c] Polymath, D. H. J., Variants of the Selberg sieve, and bounded intervals containing many primes. Res. Math. Sci. 1 (2014), Art. 12. arXiv:1407.4897
Quoted from FormalConjectures/ErdosProblems/1204.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/1204.
The file states 5 research or textbook statements: 2 open and 3 solved. It also has 1 API statement, counted here but not shown.
Erdos1204.erdos_1204.parts.i
Open: stated without proof.
We call a sequence of integers \(0\leq a_1\lt \cdots \lt a_k\) admissible if it is missing at least one congruence class modulo every prime \(p\). Let \(A(k)=\min a_k\). Estimate \(A(k)\) - in particular, is it true that
\[A(k)\sim k\log k?\]
theorem erdos_1204.parts.i :
(fun k : ℕ ↦ (A k : ℝ)) ~[atTop] fun k : ℕ ↦ (k : ℝ) * Real.log k
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1204.lean, line 71.
Erdos1204.erdos_1204.parts.ii
Open: stated without proof.
We call a sequence of integers \(0\leq a_1\lt \cdots \lt a_k\) admissible if it is missing at least one congruence class modulo every prime \(p\). Estimate
\[B(k)=\min \frac{a_1+\cdots+a_k}{k}.\]We read "estimate" as finding an asymptotic formula, since \(B(k)\asymp k\log k\) already follows from the known bounds for \(A(k)\) (as \(a_j\geq A(j)\)).
theorem erdos_1204.parts.ii : B ~[atTop] erdos_1204.parts.ii.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1204.lean, line 86.
Erdos1204.erdos_1204.variants.A_lower
Solved: stated here without proof.
It is known that \((1/2+o(1))k\log k \leq A(k)\). This lower bound is originally due to Elliott [El65], but was rediscovered by the Polymath project on bounded gaps between primes [Po14c].
theorem erdos_1204.variants.A_lower :
∀ ε > (0 : ℝ), ∀ᶠ k : ℕ in atTop, (1 / 2 - ε) * k * Real.log k ≤ (A k : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1204.lean, line 94.
Erdos1204.erdos_1204.variants.A_upper
Solved: stated here without proof.
It is known that \(A(k)\leq (1+o(1))k\log k\), by taking the \(k\) smallest primes \(>k\).
theorem erdos_1204.variants.A_upper :
∀ ε > (0 : ℝ), ∀ᶠ k : ℕ in atTop, (A k : ℝ) ≤ (1 + ε) * k * Real.log k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1204.lean, line 102.
Erdos1204.erdos_1204.variants.B_upper
Solved: stated here without proof.
Taking the first \(k\) primes which are \(>k\) implies \(B(k)\leq (1/2+o(1))k\log k\).
theorem erdos_1204.variants.B_upper :
∀ ε > (0 : ℝ), ∀ᶠ k : ℕ in atTop, B k ≤ (1 / 2 + ε) * k * Real.log k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1204.lean, line 110.
Sources
TheoremErdős Problem 1205#
References: - erdosproblems.com/1205 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. PDF
Quoted from FormalConjectures/ErdosProblems/1205.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/1205.
The file states 2 research or textbook statements: 2 solved. It also has 2 API statements, counted here but not shown.
Erdos1205.erdos_1205
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1205.lean#L1065.
Let \(F(x)\) be maximal such that there exists, for all \(n\leq x\), a congruence class \(a_n\pmod{n}\) such that every \(m\leq x\) satisfies at least \(F(x)\) of these congruences.
Estimate \(F(x)\).
Erdős [Er80, p. 108] describes \(F(x)\to\infty\) as a simple exercise and asks how fast \(F(x)\) tends to infinity. The estimate \(F(x)\sim\log x\) comes from the argument given on erdosproblems.com/1205 (a pigeonhole upper bound and a probabilistic lower bound), not from a paper.
theorem erdos_1205 : (fun x : ℕ ↦ (F x : ℝ)) ~[atTop] erdos_1205.answer
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1205.lean, line 95.
Erdos1205.erdos_1205.variants.upper_bound
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1205.lean#L235.
The pigeonhole principle implies \(F(x)\leq \sum_{n\leq x}\frac{1}{n}= \log x+O(1)\).
We state the exact pigeonhole bound \(F(x)\leq H_x+1\), where \(H_x=\sum_{n\leq x}\frac{1}{n}\) is the \(x\)-th harmonic number. The \(+1\) is needed, since \(F(3)\geq 2>H_3\). By Mathlib's
harmonic_le_one_add_logthis gives \(F(x)\leq\log x+2\).
theorem erdos_1205.variants.upper_bound (x : ℕ) : (F x : ℝ) ≤ (harmonic x : ℝ) + 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1205.lean, line 108.
Sources
TheoremErdős Problem 1206#
References: - erdosproblems.com/1206 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [GGK26] M. Garaev, F. Garayev, and S. Konyagin, On Sidon sets with squares, cubes, and quartics in short intervals. arXiv:2602.08807 (2026). - [GaKo24] Gabdullin, M. R. and Konyagin, S. V., Trigonometric polynomials with frequencies in the set of cubes. Math. Notes (2024), 336--340.
Quoted from FormalConjectures/ErdosProblems/1206.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/1206.
The file states 2 research or textbook statements: 2 open.
Erdos1206.erdos_1206.parts.i
Open: stated without proof.
Does \(\{1,2^3,\ldots,N^3\}\) contain a Sidon set of size \(\gg N\)?
theorem erdos_1206.parts.i :
∃ c : ℝ, 0 < c ∧ ∀ᶠ N in Filter.atTop, ∃ S : Finset ℕ,
S ⊆ (Finset.Icc 1 N).image (fun n => n ^ 3) ∧
IsSidon (S : Set ℕ) ∧ c * (N : ℝ) ≤ (S.card : ℝ)
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1206.lean, line 41.
Erdos1206.erdos_1206.parts.ii
Open: stated without proof.
Is there an infinite set \(A\subset \mathbb{N}\) of positive density such that \(\{a^3 : a\in A\}\) is a Sidon set?
theorem erdos_1206.parts.ii :
∃ A : Set ℕ, A.Infinite ∧ 0 < A.lowerDensity ∧
IsSidon ((fun a : ℕ => a ^ 3) '' A)
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1206.lean, line 51.
Sources
TheoremErdős Problem 1207#
References: - erdosproblems.com/1207 - [BMP05] Brass, Peter and Moser, William and Pach, János, Research problems in discrete geometry. (2005), xii+499. - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [LPZ26] Lee, S., Pohoata, C., and Zhu, D. G., The Minkowski grid has robustly many repeated distances. arXiv:2607.05374 (2026). - [PaTa02] Pach, János and Tardos, Gábor, Isosceles triangles determined by a planar point set. Graphs Combin. (2002), 769--779.
Quoted from FormalConjectures/ErdosProblems/1207.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/1207.
The file states 1 research or textbook statement: 1 solved.
Erdos1207.erdos_1207
Solved: stated here without proof.
Let \(P_d(n)\) be such that in any set of \(n\) points in \(\mathbb{R}^d\) there exist at least \(P_d(n)\) many points which do not contain an isosceles triangle. Estimate \(P_d(n)\) - in particular, is it true that
\[P_2(n)\lt n^{1-c}\]for some constant \(c>0\)?
Lee, Pohoata, and Zhu [LPZ26] proved the stated planar bound. Their isosceles-free subsets also exclude degenerate triangles of equally spaced collinear points.
theorem erdos_1207 :
∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (P 2 n : ℝ) < (n : ℝ) ^ (1 - c)
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1207.lean, line 57.
Sources
TheoremErdős Problem 1209#
References: - erdosproblems.com/429 - erdosproblems.com/1102 - erdosproblems.com/1209 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
Quoted from FormalConjectures/ErdosProblems/1209.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/1209.
The file states 6 research or textbook statements: 3 open and 3 solved. It also has 5 API statements, counted here but not shown.
Erdos1209.erdos_1209.parts.i
Proved here.
Let \(A=\{a_1\lt a_2\lt \cdots\}\) be a sequence of integers which tends to infinity sufficiently fast. If there is an \(n\) such that all \(n+a_k\) are primes then must there exist infinitely many such \(n\)?
Erdős [Er80] wrote 'unless I overlook a trivial way of getting a counterexample these questions are quite hopeless'. There is indeed a trivial counterexample (a variant of the construction in [erdosproblems.com/429]): define \(a_1=2\) and for \(k\geq 2\) let \(a_k>a_{k-1}\) be a prime such that \(a_k+k\equiv 0\pmod{q_k}\), where \(q_k\) is some prime not dividing \(k\). This sequence can be made to grow arbitrarily fast
See also [erdosproblems.com/429] and [erdosproblems.com/1102].
theorem erdos_1209.parts.i :
¬ ∃ f : ℕ → ℕ, ∀ a : ℕ → ℕ, StrictMono a → (∀ k, f k ≤ a k) →
(∃ n, ∀ k, (n + a k).Prime) →
{n | ∀ k, (n + a k).Prime}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1209.lean, line 89.
Erdos1209.erdos_1209.parts.ii
Proved here.
What if we ask for \(n+a_k\) to be squarefree instead of prime?
A similar construction provides a counterexample to the squarefree question.
theorem erdos_1209.parts.ii :
¬ ∃ f : ℕ → ℕ, ∀ a : ℕ → ℕ, StrictMono a → (∀ k, f k ≤ a k) →
(∃ n, ∀ k, Squarefree (n + a k)) →
{n | ∀ k, Squarefree (n + a k)}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1209.lean, line 157.
Erdos1209.erdos_1209.parts.iii.a
Solved: stated here; a Lean proof is at https://github.com/ebarschkis/ErdosProblem/blob/main/Problem1209/Formalization.lean.
Are there \(n\) such that \(n+2^{2^k}\) is always a prime?
ebarschkis and GPT have proved that there are no \(n\) such that \(n+2^{2^k}\) is always prime: let \(n\geq 3\) be any odd integer. If \(k\) is chosen sufficiently large, and \(p=n+2^{2^{k}}\) is prime, then the multiplicative order of \(2^{2^k}\pmod{p}\), say \(m\) is odd, and hence if \(l\) is chosen such that \(2^l\equiv 1\pmod{m}\) then \(p\mid n+2^{2^{k+rl}}\) for all \(r\geq 1\).
This was formalized in Lean by Barschkis using ChatGPT.
theorem erdos_1209.parts.iii.a :
¬ ∃ n : ℕ, ∀ k : ℕ, (n + 2 ^ (2 ^ k)).Prime
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1209.lean, line 197.
Erdos1209.erdos_1209.parts.iii.b
Open: stated without proof.
Are there \(n\) such that \(n+2^{2^k}\) is always squarefree?
theorem erdos_1209.parts.iii.b :
∃ n : ℕ, ∀ k : ℕ, Squarefree (n + 2 ^ (2 ^ k))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1209.lean, line 205.
Erdos1209.erdos_1209.parts.iii.c
Open: stated without proof.
Are there \(n\) such that \(n+2^{2^k}\) is infinitely often a prime?
theorem erdos_1209.parts.iii.c :
∃ n : ℕ, {k | (n + 2 ^ (2 ^ k)).Prime}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1209.lean, line 213.
Erdos1209.erdos_1209.parts.iii.d
Open: stated without proof.
Are there \(n\) such that \(n+2^{2^k}\) is infinitely often squarefree?
theorem erdos_1209.parts.iii.d :
∃ n : ℕ, {k | Squarefree (n + 2 ^ (2 ^ k))}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1209.lean, line 221.
Sources
TheoremErdős Problem 1210#
References: - erdosproblems.com/1210 - [Er77c] Erdős, Paul, Problems and results on combinatorial number theory. III. Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976) (1977), 43-72. - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
Quoted from FormalConjectures/ErdosProblems/1210.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/1210.
The file states 2 research or textbook statements: 2 open.
Erdos1210.erdos_1210
Open: stated without proof.
Let \(A\subseteq [1,n)\) be a set of integers such that \((a,b)=1\) for all distinct \(a,b\in A\). Is it true that \(\sum_{a\in A}\frac{1}{n-a}\leq \sum_{p < n}\frac{1}{p}+O(1)\)?
theorem erdos_1210 :
∃ C : ℝ, ∀ n : ℕ, ∀ A : Finset ℕ,
(∀ a ∈ A, 1 ≤ a ∧ a < n) →
(∀ a ∈ A, ∀ b ∈ A, a ≠ b → a.Coprime b) →
∑ a ∈ A, (1 / ((n : ℝ) - a)) ≤ (∑ p ∈ (range n).filter Prime, (1 / (p : ℝ))) + C
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1210.lean, line 42.
Erdos1210.erdos_1210.variants.er80_correction
Open: stated without proof.
In [Er80] he claims he "did not state this quite correctly" in [Er77c]. The problem in [Er77c] which Erdős is presumably referring to states that if \(n < q_1 < \cdots < q_k\leq m\) is the set of primes in \((n,m]\) then \(\sum \frac{1}{q_i-n} < \sum_{p < m-n}\frac{1}{p}+O(1)\).
theorem erdos_1210.variants.er80_correction :
∃ C : ℝ, ∀ n m : ℕ, n < m →
∑ q ∈ (Ioc n m).filter Prime, (1 / ((q : ℝ) - n)) <
(∑ p ∈ (range (m - n)).filter Prime, (1 / (p : ℝ))) + C
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1210.lean, line 55.
Sources
TheoremErdős Problem 1211#
References: - erdosproblems.com/1211 - [CFP22] Conlon, David and Fox, Jacob and Pham, Huy Tuan, The upper logarithmic density of monochromatic subset sums. Mathematika 68 (2022), 1292--1301. arXiv:2105.15195 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. PDF
Quoted from FormalConjectures/ErdosProblems/1211.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/1211.
The file states 1 research or textbook statement: 1 solved. It also has 2 API statements, counted here but not shown.
Erdos1211.erdos_1211
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1211.lean#L401.
Let \(\mathbb{N}=A\cup B\) where \(A\) and \(B\) are disjoint. Let \(S(A)\) be those integers which are the sum of finitely many distinct elements of \(A\), and similarly for \(S(B)\).
If
\[ \overline{\delta}(X)=\limsup_{x\to \infty}\frac{1}{\log x} \sum_{\substack{n\in X\\ n\lt x}}\frac{1}{n} \]is the upper logarithmic density of \(X\) then how large must
\[\max(\overline{\delta}(S(A)),\overline{\delta}(S(B)))\]be?
A question of Erdős [Er80]. Conlon, Fox, and Pham [CFP22, Theorem 1] proved that the least possible value of \(\max(\overline{\delta}(S(A)),\overline{\delta}(S(B)))\) is \(\frac{2+\sqrt{3}}{4}\approx 0.93301\), and that it is attained.
theorem erdos_1211 :
(∀ A B : Set ℕ, IsNatPartition A B → erdos_1211.answer ≤ partitionValue A B) ∧
∃ A B : Set ℕ, IsNatPartition A B ∧ partitionValue A B = erdos_1211.answer
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1211.lean, line 97.
Sources
TheoremErdős Problem 1212#
References: - erdosproblems.com/1212 - [Er80] Erdős, P., Some notes on problems and results in number theory (1980), p. 114.
This file also records machine-checked cores of verified partial results (2026): a composite-anchor sufficient reduction and an impossibility theorem for periodic certificates; see the corresponding lemmas below.
Quoted from FormalConjectures/ErdosProblems/1212.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/1212.
The file states 1 research or textbook statement: 1 solved. It also has 1 test statement and 6 API statements, counted here but not shown.
Erdos1212.erdos_1212
Solved: stated here; a Lean proof is at https://github.com/crabsatellite/erdos-1212-visible-lattice-path/blob/400001f0847afe36a26c588d34445210dbdc116e/kernel/Erdos1212Kernel/AlgebraicCorridorKernelAudit.lean.
Let \(G\) be the graph with vertex set those pairs \((x,y)\in \mathbb{N}^2\) with \(\mathrm{gcd}(x,y)=1\), in which we join two vertices if the differ in only one coordinate, and there by \(\pm 1\).
Is there a path going to infinity on \(G\), say \(P\), such that for all \((x,y)\in P\) both \(\min(x,y)>1\) and at least one of \(x\) or \(y\) is composite?
The weaker version (only \(\min(x,y) > 1\)) was solved by C. Stewart via the prime-pair path \((p_k, p_{k+1}) \to (p_{k+1}, p_{k+2})\), as recounted in [Er80]; the compositeness condition forbids those anchors.
The strengthened problem was solved by Alex Chengyu Li; see Li's construction and the accompanying Lean formalization.
theorem erdos_1212 :
∃ f : ℕ → ℕ × ℕ, Function.Injective f ∧ (∀ n, Adj (f n) (f (n + 1))) ∧
(∀ n, Valid (f n)) ∧
Tendsto (fun n => (f n).1 + (f n).2) atTop atTop
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1212.lean, line 74.
Sources
TheoremErdős Problem 1213#
References: - erdosproblems.com/1213 - [He86] Hegyvári, N., On consecutive sums in sequences. Acta Math. Hungar. (1986), 193-200.
Quoted from FormalConjectures/ErdosProblems/1213.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/1213.
The file states 2 research or textbook statements: 2 solved.
Erdos1213.erdos_1213
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1213.lean#L495.
Let \(a,K\geq 1\). Does there exist \(f(a,K)\) such that if \(a=a_1\lt \cdots \lt a_s\) is a sequence of integers with \(a_s> f(a,K)\) and with bounded gaps \(a_{i+1}-a_i\leq K\) then there are two distinct intervals \(I\) and \(J\) such that
\[\sum_{i\in I}a_i=\sum_{j\in J}a_j?\]Hegyvári [He86] has proved the answer is yes, and gives an explicit bound of the shape \(f(a,K) \ll ae^{O(K)}\). Hegyvári believes that the exponential dependence on \(K\) here is not best possible.
theorem erdos_1213 : ∀ a K : ℕ, 1 ≤ a → 1 ≤ K → ∃ f : ℕ,
∀ (s : ℕ) (A : ℕ → ℕ), 0 < s → A 0 = a → StrictMonoOn A (Set.Iio s) →
(∀ i, i + 1 < s → A (i + 1) - A i ≤ K) → f < A (s - 1) → HasEqualIntervalSums A s
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1213.lean, line 53.
Erdos1213.erdos_1213.variants.hegyvari
Solved: stated here without proof.
Hegyvári [He86] proved that one can take \(f(a,K) \ll ae^{O(K)}\).
theorem erdos_1213.variants.hegyvari : ∃ C : ℝ, 0 < C ∧ ∀ a K : ℕ, 1 ≤ a → 1 ≤ K →
∀ (s : ℕ) (A : ℕ → ℕ), 0 < s → A 0 = a → StrictMonoOn A (Set.Iio s) →
(∀ i, i + 1 < s → A (i + 1) - A i ≤ K) → C * a * Real.exp (C * K) < A (s - 1) →
HasEqualIntervalSums A s
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1213.lean, line 62.
Sources
TheoremErdős Problem 1214#
References: - erdosproblems.com/1214 - [CoSc97] Corrales-Rodrigáñez, Capi and Schoof, René, The support problem and its elliptic analogue. J. Number Theory (1997) [Volume 64, Issue 2], 276--290.
Quoted from FormalConjectures/ErdosProblems/1214.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/1214.
The file states 1 research or textbook statement: 1 solved.
Erdos1214.erdos_1214
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1214.lean#L948.
Let \(x,y\geq 1\) be integers such that, for all \(n\geq 1\), the set of primes dividing \(x^{n}-1\) is equal to the set of primes dividing \(y^n-1\). Must \(x=y\)?
Erdős asked this at a 1988 number theory conference in Banff.
A positive answer was given by Corrales-Rodrigáñez and Schoof [CoSc97].
theorem erdos_1214 :
∀ x y : ℕ, x ≥ 1 → y ≥ 1 →
(∀ n : ℕ, n ≥ 1 → { p : ℕ | p.Prime ∧ p ∣ x ^ n - 1 } = { p : ℕ | p.Prime ∧ p ∣ y ^ n - 1 }) →
x = y
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1214.lean, line 44.
Sources
TheoremErdős Problem 1217#
References: - erdosproblems.com/1217 - [ABLLPSTT26] B. Alexeev, K. Barreto, Y. Li, J. D. Lichtman, L. Price, J. I. Shah, Q. Tang, and T. Tao, Primitive sets and von Mangoldt chains: Erdős Problem #1196 and beyond. arXiv:2605.00301 (2026). - [DaEr51] Davenport, H. and Erdős, P., On sequences of positive integers. J. Indian Math. Soc. (N.S.) (1951), 19--24. PDF - [ESS66] Erdős, P. and Sárközi, A. and Szemerédi, E., On divisibility properties of sequences of integers. Studia Sci. Math. Hungar. (1966), 431--435. PDF
Quoted from FormalConjectures/ErdosProblems/1217.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/1217.
The file states 5 research or textbook statements: 5 solved.
Erdos1217.erdos_1217
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1217.lean#L86.
Let \(A=\{a_1\lt a_2\lt \cdots\}\) be an infinite sequence of positive integers with positive lower logarithmic density.
Must there exist a sequence \(n_1\lt \cdots\) such that
\[a_{n_i}\mid a_{n_{i+1}}\]for all \(i\geq 1\) and
\[\limsup_{x\to \infty}\frac{1}{\log\log x}\sum_{a_{n_i}\lt x}1 \geq \limsup_{x\to \infty} \frac{1}{\log\log x}\sum_{a_n\lt x}\frac{1}{a_n\log a_n}?\]A problem of Erdős, Sárközi, and Szemerédi [ESS66, p. 432, (5)]. The answer is yes, proved by Alexeev, Barreto, Li, Lichtman, Price, Shah, Tang, and Tao [ABLLPSTT26, Theorem 1.6]. Sequences are indexed from \(0\) here.
theorem erdos_1217 :
∀ a : ℕ → ℕ, StrictMono a → (∀ i, 0 < a i) → 0 < lowerLogDensity (Set.range a) →
∃ n : ℕ → ℕ, StrictMono n ∧ (∀ i, a (n i) ∣ a (n (i + 1))) ∧
weightedRate (Set.range a) ≤ chainRate (a ∘ n)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1217.lean, line 97.
Erdos1217.erdos_1217.variants.without_density
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1217.lean#L66.
The answer to
erdos_1217is yes even without the assumption that \(A\) has positive lower logarithmic density [ABLLPSTT26]: it suffices that the doubly harmonic rate on the right-hand side is positive, which holds whenever the lower logarithmic density is positive.
theorem erdos_1217.variants.without_density :
∀ a : ℕ → ℕ, StrictMono a → 0 < weightedRate (Set.range a) →
∃ n : ℕ → ℕ, StrictMono n ∧ (∀ i, a (n i) ∣ a (n (i + 1))) ∧
weightedRate (Set.range a) ≤ chainRate (a ∘ n)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1217.lean, line 111.
Erdos1217.erdos_1217.variants.abllpstt
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1217/Resolution.lean#L451.
The set form of [ABLLPSTT26, Theorem 1.6]: if \(A \subseteq \mathbb{N}\) has positive upper doubly logarithmic density
\[\Delta=\limsup_{x\to\infty}\frac{1}{\log\log x}\sum_{n\in A,\ n\lt x}\frac{1}{n\log n},\]then \(A\) contains a strictly increasing infinite divisibility chain \(d_0\mid d_1\mid\cdots\) with
\[\limsup_{x\to\infty}\frac{1}{\log\log x}\sum_{d_i\lt x}1\geq\Delta.\]
theorem erdos_1217.variants.abllpstt (A : Set ℕ) (hA : 0 < weightedRate A) :
∃ d : ℕ → ℕ, StrictMono d ∧ (∀ i, d i ∈ A) ∧ (∀ i, d i ∣ d (i + 1)) ∧
weightedRate A ≤ chainRate d
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1217.lean, line 127.
Erdos1217.erdos_1217.variants.davenport_erdos
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1217.lean#L86.
Davenport and Erdős [DaEr51] proved that (assuming \(A\) has positive lower logarithmic density) there exists a sequence \(n_1\lt \cdots\) such that \(a_{n_i}\mid a_{n_{i+1}}\) for all \(i\geq 1\) (as stated in [ESS66, p. 431]). This also follows from
erdos_1217.
theorem erdos_1217.variants.davenport_erdos :
∀ a : ℕ → ℕ, StrictMono a → (∀ i, 0 < a i) → 0 < lowerLogDensity (Set.range a) →
∃ n : ℕ → ℕ, StrictMono n ∧ ∀ i, a (n i) ∣ a (n (i + 1))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1217.lean, line 140.
Erdos1217.erdos_1217.variants.erdos_sarkozi_szemeredi
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1217.lean#L66.
Erdős, Sárközi, and Szemerédi [ESS66, Theorem 2] proved that if
\[\limsup_{x\to \infty}\frac{1}{\log\log x}\sum_{a_n\lt x}\frac{1}{a_n\log a_n}=c>0,\]then there exists such a sequence with
\[\limsup_{x\to \infty}\frac{1}{\log\log x}\sum_{a_{n_i}\lt x}1\gg_c 1.\]Here \(\gg_c 1\) means a lower bound \(\kappa>0\) depending only on \(c\).
theorem erdos_1217.variants.erdos_sarkozi_szemeredi :
∀ c : ℝ, 0 < c → ∃ κ : ℝ, 0 < κ ∧ ∀ a : ℕ → ℕ, StrictMono a →
weightedRate (Set.range a) = ENNReal.ofReal c →
∃ n : ℕ → ℕ, StrictMono n ∧ (∀ i, a (n i) ∣ a (n (i + 1))) ∧
ENNReal.ofReal κ ≤ chainRate (a ∘ n)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1217.lean, line 155.
Sources
TheoremErdős Problem 1219#
References: - erdosproblems.com/1219 - [ErHa71] Erdős, Paul and Hajnal, András, Unsolved problems in set theory. Axiomatic Set Theory, Proc. Sympos. Pure Math. XIII Part I (1971), 17-48. - [Ko25b] Komjáth, Péter, The Erdős–Hajnal problem list. Bull. Symb. Log. (2025), 418-461. - [Sh75] Shelah, Saharon, Notes on partition calculus. Infinite and finite sets (Colloq., Keszthely, 1973), Colloq. Math. Soc. János Bolyai 10, North-Holland (1975), 1257-1276.
Quoted from FormalConjectures/ErdosProblems/1219.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/1219.
The file states 1 research or textbook statement: 1 solved. It also has 1 test statement, counted here but not shown.
Erdos1219.erdos_1219
Solved: stated here; a Lean proof is at https://github.com/jbaelaw/erdos1219-lean/blob/00e696a9cd2bbd8cad33d2cdc90ad385058c1466/Solution.lean#L22.
Let \((n_k)\) be an increasing sequence of integers such that \(2^{\aleph_{n_k}}\) is strictly increasing, and \(2^{\aleph_{n_0}} > \aleph_\omega\). Is it true that
\[\sum_k 2^{\aleph_{n_k}} \to (\aleph_\omega)^2?\]Here \(\sum_k 2^{\aleph_{n_k}}\) is the cardinal sum, and the partition relation is the classical one with two colours: every \(2\)-colouring of the pairs of a set of that cardinality has a monochromatic set of cardinality \(\aleph_\omega\).
A problem of Erdős, Hajnal, and Rado [ErHa71], proved by Shelah [Sh75].
theorem erdos_1219 :
∀ n : ℕ → ℕ, StrictMono n →
StrictMono (fun k => (2 : Cardinal.{u}) ^ ℵ_ (n k)) →
ℵ_ ω < (2 : Cardinal.{u}) ^ ℵ_ (n 0) →
cardinalPartitionRel (sum fun k => (2 : Cardinal.{u}) ^ ℵ_ (n k)) 2 2 (fun _ => ℵ_ ω)
Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1219.lean, line 54.
Sources
TheoremErdős Problem 1221#
References: - erdosproblems.com/1221 - [dBEr49] de Bruijn, N. G. and Erdős, P., Sequences of points on a circle. Nederl. Akad. Wetensch., Proc. (1949), 14-17 = Indagationes Math. 11 (1949), 46-49. PDF
Quoted from FormalConjectures/ErdosProblems/1221.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/1221.
The file states 7 research or textbook statements: 3 open and 4 solved.
Erdos1221.erdos_1221.parts.i
Open: stated without proof.
Let \(a=(a_1,\ldots,a_n)\) be points, ordered consecutively, around the circle (normalised to have circumference \(1\)). Let
\[M_r(a)=\max_r \lvert a_{i+r}-a_i\rvert\]and
\[m_r(a)=\min_r \lvert a_{i+r}-a_i\rvert,\]where the indices are interpreted in a cyclic fashion and the distance is around the circle (in other words, the maximum and minimum distance between \(r\)-consecutive points).
Let
\[\Lambda_r=\inf_a \limsup_n n M_r(a_1,\ldots,a_n),\]\[\lambda_r = \sup_a \liminf_n nm_r(a_1,\ldots,a_n),\]and
\[\mu_r=\inf_a \limsup_n \frac{M_r(a)}{m_r(a)},\]where the outer \(\inf/\sup\) is over all infinite sequences \(a=(a_1,\ldots)\).
Is it true that \(r(\Lambda_r-1)\), \(r(1-\lambda_r)\), and \(r(\mu_r-1)\) tend to infinity as \(r\to \infty\)?
This is the first part, conjectured by de Bruijn and Erdős [dBEr49, §6]. We read \(\Lambda_r\) and \(\lambda_r\) as in
bigLambdaandsmallLambda, that is, as printed. The sequences are required to have pairwise distinct points modulo \(1\) (seebigLambda). Then \(nM_r\geq r\) [dBEr49, §1], so \(r(\Lambda_r-1)\to\infty\) would hold trivially. Also \(m_r\geq r\,m_1\), so the sequence \(a_k=\log_2(2k-1)\) of [dBEr49, §2] gives \(\lambda_r\geq r/\log 4\), which exceeds \(1\) for \(r\geq2\), so \(r(1-\lambda_r)\) would be negative for \(r\geq2\). The intended conjectures are about the quantities normalised by \(r\), so \(r(\Lambda_r/r-1)=\Lambda_r-r\), and the first part asks whether \(\Lambda_r-r\to\infty\).
theorem erdos_1221.parts.i :
∀ K : ℝ, ∀ᶠ r : ℕ in atTop, ENNReal.ofReal ((r : ℝ) + K) < bigLambda r
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1221.lean, line 119.
Erdos1221.erdos_1221.parts.ii
Open: stated without proof.
Let \(a=(a_1,\ldots,a_n)\) be points, ordered consecutively, around the circle (normalised to have circumference \(1\)). Let
\[M_r(a)=\max_r \lvert a_{i+r}-a_i\rvert\]and
\[m_r(a)=\min_r \lvert a_{i+r}-a_i\rvert,\]where the indices are interpreted in a cyclic fashion and the distance is around the circle (in other words, the maximum and minimum distance between \(r\)-consecutive points).
Let
\[\Lambda_r=\inf_a \limsup_n n M_r(a_1,\ldots,a_n),\]\[\lambda_r = \sup_a \liminf_n nm_r(a_1,\ldots,a_n),\]and
\[\mu_r=\inf_a \limsup_n \frac{M_r(a)}{m_r(a)},\]where the outer \(\inf/\sup\) is over all infinite sequences \(a=(a_1,\ldots)\).
Is it true that \(r(\Lambda_r-1)\), \(r(1-\lambda_r)\), and \(r(\mu_r-1)\) tend to infinity as \(r\to \infty\)?
This is the second part. As in the first part, we normalise \(\lambda_r\) by \(r\), so \(r(1-\lambda_r/r)=r-\lambda_r\), and the second part asks whether \(r-\lambda_r\to\infty\).
theorem erdos_1221.parts.ii :
∀ K : ℝ, ∀ᶠ r : ℕ in atTop, smallLambda r < ENNReal.ofReal ((r : ℝ) - K)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1221.lean, line 146.
Erdos1221.erdos_1221.parts.iii
Open: stated without proof.
Let \(a=(a_1,\ldots,a_n)\) be points, ordered consecutively, around the circle (normalised to have circumference \(1\)). Let
\[M_r(a)=\max_r \lvert a_{i+r}-a_i\rvert\]and
\[m_r(a)=\min_r \lvert a_{i+r}-a_i\rvert,\]where the indices are interpreted in a cyclic fashion and the distance is around the circle (in other words, the maximum and minimum distance between \(r\)-consecutive points).
Let
\[\Lambda_r=\inf_a \limsup_n n M_r(a_1,\ldots,a_n),\]\[\lambda_r = \sup_a \liminf_n nm_r(a_1,\ldots,a_n),\]and
\[\mu_r=\inf_a \limsup_n \frac{M_r(a)}{m_r(a)},\]where the outer \(\inf/\sup\) is over all infinite sequences \(a=(a_1,\ldots)\).
Is it true that \(r(\Lambda_r-1)\), \(r(1-\lambda_r)\), and \(r(\mu_r-1)\) tend to infinity as \(r\to \infty\)?
This is the third part. The quantity \(\mu_r\) needs no normalisation, and the third part asks whether \(r(\mu_r-1)\to\infty\), that is, whether \(\mu_r>1+K/r\) for every \(K\) and all large \(r\).
theorem erdos_1221.parts.iii :
∀ K : ℝ, ∀ᶠ r : ℕ in atTop, ENNReal.ofReal (1 + K / (r : ℝ)) < mu r
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1221.lean, line 173.
Erdos1221.erdos_1221.variants.r_one
Solved: stated here without proof.
De Bruijn and Erdős [dBEr49, §§2-5] proved that \(\Lambda_1=\frac{1}{\log 2}\), \(\lambda_1=\frac{1}{\log 4}\), and \(\mu_1=2\). A sequence which witnesses this is \(a_k=\log_2(2k-1)\). For \(r=1\) the normalisation by \(r\) plays no role.
theorem erdos_1221.variants.r_one :
bigLambda 1 = ENNReal.ofReal (1 / Real.log 2) ∧
smallLambda 1 = ENNReal.ofReal (1 / Real.log 4) ∧ mu 1 = 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1221.lean, line 183.
Erdos1221.erdos_1221.variants.bigLambda_ge
Solved: stated here without proof.
De Bruijn and Erdős [dBEr49, (3.3)] proved that, for any \(r\geq 1\),
\[\Lambda_r \geq \frac{1}{\log(1+1/r)}.\]Here \(\Lambda_r\) is as in
bigLambda, with no normalisation by \(r\).
theorem erdos_1221.variants.bigLambda_ge {r : ℕ} (hr : 1 ≤ r) :
ENNReal.ofReal (1 / Real.log (1 + 1 / (r : ℝ))) ≤ bigLambda r
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1221.lean, line 194.
Erdos1221.erdos_1221.variants.smallLambda_le
Solved: stated here without proof.
De Bruijn and Erdős [dBEr49, (4.3)] proved that, for any \(r\geq 1\),
\[\lambda_r \leq \frac{r}{r+1}\frac{1}{\log(1+1/r)}.\]Here \(\lambda_r\) is as in
smallLambda, with no normalisation by \(r\).
theorem erdos_1221.variants.smallLambda_le {r : ℕ} (hr : 1 ≤ r) :
smallLambda r ≤
ENNReal.ofReal ((r : ℝ) / ((r : ℝ) + 1) * (1 / Real.log (1 + 1 / (r : ℝ))))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1221.lean, line 204.
Erdos1221.erdos_1221.variants.mu_ge
Solved: stated here without proof.
De Bruijn and Erdős [dBEr49, §1 and (5.7)] proved that, for any \(r\geq 1\),
\[\mu_r \geq 1+\frac{1}{r}.\]
theorem erdos_1221.variants.mu_ge {r : ℕ} (hr : 1 ≤ r) :
ENNReal.ofReal (1 + 1 / (r : ℝ)) ≤ mu r
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1221.lean, line 214.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.