Skip to content

Erdős problem 897

Start work

Let f(n)f(n) be an additive function (so that f(ab)=f(a)+f(b)f(ab)=f(a)+f(b) if (a,b)=1(a,b)=1 such that lim sup⁡p,kf(pk)/log⁡(pk)=∞\limsup_{p,k} f(p^k) / \log(p^k) = ∞. Is it true that lim sup⁡n(f(n+1)−f(n))/log⁡n=∞\limsup_n (f(n+1)−f(n))/ \log n = ∞?

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

897.lean

Retained formal statement2 of 5

Let f(n)f(n) be an additive function (so that f(ab)=f(a)+f(b)f(ab)=f(a)+f(b) if (a,b)=1(a,b)=1) such that lim sup⁡p,kf(pk)/log⁡(pk)=∞\limsup_{p,k} f(p^k) / \log(p^k) = ∞. Is it true that lim sup⁡nf(n+1)/f(n)=∞\limsup_n f(n+1)/ f(n) = ∞?

The answer is no; the same counterexample is formalised in Lean by Aristotle [ArWu25].

FormalConjectures/ErdosProblems/897.leanErdos897.erdos_897.parts.ii10 linesExact file
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 = ⊤
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.