Erdős Problem 893 to Erdős Problem 899
TheoremErdős Problem 893#
References: - erdosproblems.com/893 - [KoLu25] V. Kovač and F. Luca, On the number of divisors of Mersenne numbers. arXiv:2506.04883 (2025).
Quoted from FormalConjectures/ErdosProblems/893.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/893.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos893.erdos_893
Open: stated without proof.
Does the limit \(\lim_{n\to\infty} \frac{f(2n)}{f(n)}\) tend to infinity?
(Other finite limits have been ruled out by [KoLu25], see below)
theorem erdos_893 :
Tendsto (fun n : ℕ => (f (2 * n) : ℝ) / (f n : ℝ)) atTop atTop
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/893.lean, line 47.
Erdos893.erdos_893.variants.unbounded
Solved: stated here without proof.
Kovač and Luca [KoLu25] (building on a heuristic independently found by Cambie (personal communication)) have shown that there is no finite limit, in that \(\lim_{n\to\infty} \frac{f(2n)}{f(n)}\) is unbounded.
theorem erdos_893.variants.unbounded :
¬ BddAbove (Set.range fun n : ℕ => (f (2 * n) : ℝ) / f n)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/893.lean, line 58.
Sources
TheoremErdős Problem 894#
References: - erdosproblems.com/894 - [Ka01] Katznelson, Y., Chromatic numbers of Cayley graphs on \(\mathbb{Z}\) and recurrence. Combinatorica (2001), 211--219. - [PeSc10] Peres, Yuval and Schlag, Wilhelm, Two Erdős problems on lacunary sequences: chromatic number and Diophantine approximation. Bull. Lond. Math. Soc. (2010), 295--300.
Quoted from FormalConjectures/ErdosProblems/894.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/894.
The file states 1 research or textbook statement: 1 solved.
Erdos894.erdos_894
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos894.lean#L310.
Let \(A=\{n_1\lt n_2\lt \cdots\}\subset \mathbb{N}\) be a lacunary sequence (so there exists some \(\epsilon>0\) with \(n_{k+1}\geq (1+\epsilon)n_k\) for all \(k\)). Is it true that there must exist a finite colouring of \(\mathbb{N}\) with no monochromatic solutions to \(a-b\in A\)?
Asked by Erdős in 1987, according to Katznelson [Ka01]. In other words, does the Cayley graph defined on \(\mathbb{Z}\) by a lacunary sequence have a finite chromatic number?
Katznelson observed that a positive solution to the problem follows from the answer to 464, which yields an irrational \(\theta\) and \(\delta>0\) such that \(\inf_k \| \theta n_k\|>\delta\). In particular, the solution to 464 implies the answer to this question is yes, with the best known quantitative bound, due to Peres and Schlag [PeSc10], being that there is a colouring with no solutions using at most \(\ll \epsilon^{-1}\log(1/\epsilon)\) colours.
theorem erdos_894 :
∀ n : ℕ → ℕ, StrictMono n → (∀ k, 0 < n k) → IsLacunary n →
∃ (r : ℕ) (c : ℕ → Fin r), ∀ b k, c (b + n k) ≠ c b
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/894.lean, line 58.
Sources
TheoremErdős Problem 895#
References: - erdosproblems.com/895 - [Er95d] Erdős, Paul, On some problems in combinatorial set theory. Publ. Inst. Math. (Beograd) (N.S.) (1995), 61-65.
Quoted from FormalConjectures/ErdosProblems/895.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/895.
The file states 3 research or textbook statements: 1 open and 2 solved.
Erdos895.erdos_895
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos895.lean#L268.
Is it true that, for all sufficiently large \(n\), if \(G\) is a triangle-free graph on \(\{1,\ldots,n\}\) then there must exist three independent points \(a,b,a+b\)?
A problem of Erdős and Hajnal [Er95d]. The stated problem has been resolved by Barber (personal communication) who verified using a SAT solver that this is true for all \(n\geq 18\).
theorem erdos_895 :
∀ᶠ n in atTop, ∀ G : SimpleGraph (Set.Icc 1 n), G.CliqueFree 3 →
∃ a b c : Set.Icc 1 n, a ≠ b ∧ (a : ℕ) + (b : ℕ) = c ∧ G.IsIndepSet {a, b, c}
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/895.lean, line 45.
Erdos895.erdos_895.variants.eighteen
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos895.lean#L243.
Barber's sharp form of erdős_895: every triangle-free graph on \(\{1,\ldots,n\}\) with \(n\geq 18\) contains three independent points \(a,b,a+b\).
theorem erdos_895.variants.eighteen (n : ℕ) (hn : 18 ≤ n) (G : SimpleGraph (Set.Icc 1 n))
(hG : G.CliqueFree 3) :
∃ a b c : Set.Icc 1 n, a ≠ b ∧ (a : ℕ) + (b : ℕ) = c ∧ G.IsIndepSet {a, b, c}
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/895.lean, line 57.
Erdos895.erdos_895.variants.hindman
Open: stated without proof.
Hajnal thought that there is in fact an independent set which is a Hindman set - that is, an independent set of the shape
\[\left\{ \sum_{i\in S}a_i : S\subseteq \{1,\ldots,k\}\right\}\]for some \(a_1,\ldots,a_k\) (provided \(n\) is sufficiently large depending on \(k\)).
The general question of an independent Hindman set remains open. Here the \(a_i\) are taken to be distinct positive integers and \(S\) ranges over the nonempty subsets of \(\{1,\ldots,k\}\).
theorem erdos_895.variants.hindman :
∀ k : ℕ, ∀ᶠ n in atTop, ∀ G : SimpleGraph (Set.Icc 1 n), G.CliqueFree 3 →
∃ a : Fin k → ℕ, StrictMono a ∧ ∃ I : Set (Set.Icc 1 n), G.IsIndepSet I ∧
Subtype.val '' I = {m | ∃ S : Finset (Fin k), S.Nonempty ∧ m = ∑ i ∈ S, a i}
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/895.lean, line 72.
Sources
TheoremErdős Problem 897#
References: - erdosproblems.com/897 - [Ar25] Archivara Math Research Agent, An Additive Counterexample: Erdős Problem 897 (2025) - [ArWu25] Aristotle, operated mostly by L. Wu, Lean formalisation of Erdős problem 897 (2025) - [Wi70] E. Wirsing, A characterization of \(\log n\) as an additive arithmetic function. Symposia Math. (1970), 45-57. - [Wi81] E. Wirsing, Additive and completely additive functions with restricted growth. Recent progress in analytic number theory, Vol. 2 (Durham, 1979), 231--280 (1981).
Quoted from FormalConjectures/ErdosProblems/897.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/897.
The file states 5 research or textbook statements: 2 open and 3 solved.
Erdos897.erdos_897.parts.i
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos897.lean.
Let \(f(n)\) be an additive function (so that \(f(ab)=f(a)+f(b)\) if \((a,b)=1\) such that \(\limsup_{p,k} f(p^k) / \log(p^k) = ∞\). Is it true that \(\limsup_n (f(n+1)−f(n))/ \log n = ∞\)?
The answer is no; this follows from a construction of Wirsing [Wi81], rediscovered by Archivara [Ar25] and formalised in Lean by Aristotle [ArWu25].
theorem erdos_897.parts.i : ¬ ∀ (f : ℕ → ℝ),
(∀ᵉ (a > 0) (b > 0), a.Coprime b → f (a * b) = f a + f b) →
((Filter.atTop ⊓ Filter.principal {(p, k) : ℕ × ℕ | p.Prime}).limsup
(fun (p, k) => (f (p^k) / (p^k : ℝ).log : EReal)) = ⊤) →
Filter.atTop.limsup (fun (n : ℕ) => ((f (n+1) - f n) / (n : ℝ).log : EReal)) = ⊤
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/897.lean, line 49.
Erdos897.erdos_897.parts.ii
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos897.lean.
Let \(f(n)\) be an additive function (so that \(f(ab)=f(a)+f(b)\) if \((a,b)=1\)) such that \(\limsup_{p,k} f(p^k) / \log(p^k) = ∞\). Is it true that \(\limsup_n f(n+1)/ f(n) = ∞\)?
The answer is no; the same counterexample is formalised in Lean by Aristotle [ArWu25].
theorem erdos_897.parts.ii : ¬ ∀ (f : ℕ → ℝ),
(∀ᵉ (a > 0) (b > 0), a.Coprime b → f (a * b) = f a + f b) →
((Filter.atTop ⊓ Filter.principal {(p, k) : ℕ × ℕ | p.Prime}).limsup
(fun (p, k) => (f (p^k) / (p^k : ℝ).log : EReal)) = ⊤) →
Filter.atTop.limsup (fun (n : ℕ) => (f (n+1) / f n : EReal)) = ⊤
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/897.lean, line 66.
Erdos897.erdos_897.variants.log_growth
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos491.lean#L34.
Wirsing [Wi70] proved that if \(|f(n+1)−f(n)| ≤ C\) then \(f(n) = c \log n + O(1)\) for some constant \(c\). This is Erdős Problem 491; see
erdos_491, whose linked formal proof gives this statement.
theorem erdos_897.variants.log_growth
(f : ℕ → ℝ)
(hf : ∀ᵉ (a > 0) (b > 0), a.Coprime b → f (a * b) = f a + f b)
(C : ℝ) (hf' : ∀ n, |f (n+1) - f n| ≤ C) :
∃ c, ∃ (O : ℕ → ℝ), O =O[Filter.atTop] (1 : ℕ → ℝ) ∧
∀ n, f n ≤ c*Real.log n + O n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/897.lean, line 80.
Erdos897.erdos_897.variants.parts.i
Open: stated without proof.
Let \(f(n)\) be an additive function (so that \(f(ab)=f(a)+f(b)\) if \((a,b)=1\)) such that \(\limsup_{p,k} f(p^k) / \log(p^k) = ∞\) and \(f(p^k) = f(p)\) or \(f(p^k) = kf(p)\). Is it true that \(\limsup_n (f(n+1)−f(n))/ \log n = ∞\)?
The known counterexample does not satisfy either of these extra hypotheses, so this variant remains open.
theorem erdos_897.variants.parts.i : ∀ (f : ℕ → ℝ),
(∀ᵉ (a > 0) (b > 0), a.Coprime b → f (a * b) = f a + f b) →
((Filter.atTop ⊓ Filter.principal {(p, k) : ℕ × ℕ | p.Prime}).limsup
(fun (p, k) => (f (p^k) / (p^k : ℝ).log : EReal)) = ⊤) →
(∀ k p, p.Prime → f (p^k) = f p) ∨ (∀ (k p : ℕ), p.Prime → f (p^k) = k*f p) →
Filter.atTop.limsup (fun (n : ℕ) => ((f (n+1) - f n) / (n : ℝ).log : EReal)) = ⊤
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/897.lean, line 99.
Erdos897.erdos_897.variants.parts.ii
Open: stated without proof.
Let \(f(n)\) be an additive function (so that \(f(ab)=f(a)+f(b)\) if \((a,b)=1\)) such that \(\limsup_{p,k} f(p^k) / \log(p^k) = ∞\) and \(f(p^k) = f(p)\) or \(f(p^k) = kf(p)\). Is it true that \(\limsup_n f(n+1)/f(n) = ∞\)?
The known counterexample does not satisfy either of these extra hypotheses, so this variant remains open.
theorem erdos_897.variants.parts.ii : ∀ (f : ℕ → ℝ),
(∀ᵉ (a > 0) (b > 0), a.Coprime b → f (a * b) = f a + f b) →
((Filter.atTop ⊓ Filter.principal {(p, k) : ℕ × ℕ | p.Prime}).limsup
(fun (p, k) => (f (p^k) / (p^k : ℝ).log : EReal)) = ⊤) →
(∀ k p, p.Prime → f (p^k) = f p) ∨ (∀ (k p : ℕ), p.Prime → f (p^k) = k*f p) →
Filter.atTop.limsup (fun (n : ℕ) => (f (n+1) / f n : EReal)) = ⊤
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/897.lean, line 117.
Sources
TheoremErdős Problem 898#
References: - erdosproblems.com/898 - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79. - Wikipedia
Quoted from FormalConjectures/ErdosProblems/898.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/898.
The file states 1 research or textbook statement: 1 solved.
Erdos898.erdos_898
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos898.lean.
If \(A,B,C\in \mathbb{R}^2\) form a triangle and \(P\) is a point in the interior then, if \(N\) is where the perpendicular from \(P\) to \(AB\) meets the triangle, and similarly for \(M\) and \(L\),
\[ \overline{PA}+\overline{PB}+\overline{PC}\geq 2(\overline{PM}+\overline{PN}+\overline{PL}). \]Conjectured by Erdős in 1932 (according to [Er82e]) and proved by Mordell soon afterwards, now known as the Erdős-Mordell inequality.
theorem erdos_898 (A B C P L M N : ℝ²) (hABC : AffineIndependent ℝ ![A, B, C])
(hP : P ∈ interior (convexHull ℝ ({A, B, C} : Set ℝ²)))
(hN : N ∈ line[ℝ, A, B]) (hPN : line[ℝ, P, N].direction ⟂ line[ℝ, A, B].direction)
(hM : M ∈ line[ℝ, B, C]) (hPM : line[ℝ, P, M].direction ⟂ line[ℝ, B, C].direction)
(hL : L ∈ line[ℝ, C, A]) (hPL : line[ℝ, P, L].direction ⟂ line[ℝ, C, A].direction) :
dist P A + dist P B + dist P C ≥ 2 * (dist P M + dist P N + dist P L)
Category research solved; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/898.lean, line 48.
Sources
TheoremErdős Problem 899#
Reference: erdosproblems.com/899
Quoted from FormalConjectures/ErdosProblems/899.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/899.
The file states 1 research or textbook statement: 1 solved.
Erdos899.erdos_899
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/dfe2d78128b493c572cf525b1b8edf4897fb7664/src/latest/ErdosProblems/Erdos899.lean#L793.
Let \(A\subseteq\mathbb{N}\) be an infinite set such that \(|A\cap \{1, ..., N\}| = o(N)\). Is it true that
\[ \limsup_{N\to\infty}\frac{|(A - A)\cap \{1, ..., N\}|}{|A \cap \{1, ..., N\}|} = \infty? \]The answer is yes, proved by Ruzsa [Ru78].
[Ru78] Ruzsa, I. Z., On the cardinality of {\(A+A\)}\ and {\(A-A\)}. (1978), 933--938.
theorem erdos_899 : ∀ (A : Set ℕ), A.Infinite →
Tendsto (fun N => (A ∩ Icc 1 N |>.ncard : ℝ) / N) atTop (𝓝 0) →
atTop.limsup (fun N => ((A - A : Set ℕ) ∩ Icc 1 N |>.ncard : EReal) /
(A ∩ Icc 1 N).ncard) = ⊤
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/899.lean, line 50.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.