Erdő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).

theorem Erdos897.erdos_897.parts.i : False ↔ ∀ (f : ℕ → ℝ), (∀ a > 0, ∀ b > 0, a.Coprime b → f (a * b) = f a + f b) → Filter.limsup (fun (x : ℕ × ℕ) => match x with | (p, k) => ↑(f (p ^ k)) / ↑(Real.log (↑p ^ k))) (Filter.atTop ⊓ Filter.principal {(p, k) : ℕ × ℕ | Nat.Prime p}) = ⊤ → Filter.limsup (fun (n : ℕ) => (↑(f (n + 1)) - ↑(f n)) / ↑(Real.log ↑n)) Filter.atTop = ⊤

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 Erdos897.erdos_897.parts.ii : False ↔ ∀ (f : ℕ → ℝ), (∀ a > 0, ∀ b > 0, a.Coprime b → f (a * b) = f a + f b) → Filter.limsup (fun (x : ℕ × ℕ) => match x with | (p, k) => ↑(f (p ^ k)) / ↑(Real.log (↑p ^ k))) (Filter.atTop ⊓ Filter.principal {(p, k) : ℕ × ℕ | Nat.Prime p}) = ⊤ → Filter.limsup (fun (n : ℕ) => ↑(f (n + 1)) / ↑(f n)) Filter.atTop = ⊤

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 Erdos897.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

Wirsing [Wi70] proved that if $|f(n+1)−f(n)| ≤ C$ then $f(n) = c \log n + O(1)$ for some constant $c$.

theorem Erdos897.erdos_897.variants.parts.i : True ↔ ∀ (f : ℕ → ℝ), (∀ a > 0, ∀ b > 0, a.Coprime b → f (a * b) = f a + f b) → Filter.limsup (fun (x : ℕ × ℕ) => match x with | (p, k) => ↑(f (p ^ k)) / ↑(Real.log (↑p ^ k))) (Filter.atTop ⊓ Filter.principal {(p, k) : ℕ × ℕ | Nat.Prime p}) = ⊤ → ((∀ (k p : ℕ), Nat.Prime p → f (p ^ k) = f p) ∨ ∀ (k p : ℕ), Nat.Prime p → f (p ^ k) = ↑k * f p) → Filter.limsup (fun (n : ℕ) => (↑(f (n + 1)) - ↑(f n)) / ↑(Real.log ↑n)) Filter.atTop = ⊤

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 Erdos897.erdos_897.variants.parts.ii : True ↔ ∀ (f : ℕ → ℝ), (∀ a > 0, ∀ b > 0, a.Coprime b → f (a * b) = f a + f b) → Filter.limsup (fun (x : ℕ × ℕ) => match x with | (p, k) => ↑(f (p ^ k)) / ↑(Real.log (↑p ^ k))) (Filter.atTop ⊓ Filter.principal {(p, k) : ℕ × ℕ | Nat.Prime p}) = ⊤ → ((∀ (k p : ℕ), Nat.Prime p → f (p ^ k) = f p) ∨ ∀ (k p : ℕ), Nat.Prime p → f (p ^ k) = ↑k * f p) → Filter.limsup (fun (n : ℕ) => ↑(f (n + 1)) / ↑(f n)) Filter.atTop = ⊤

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.