Erdős problem 897 · problems.science

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 = ∞$ ?

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

897.lean

Retained formal statement2 of 5

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

FormalConjectures/ErdosProblems/897.leanErdos897.erdos_897.parts.ii10 linesExact file

1False ↔2  ∀ (f : ℕ → ℝ),3    (∀ a > 0, ∀ b > 0, a.Coprime b → f (a * b) = f a + f b) →4      Filter.limsup5            (fun x =>6              match x with7              | (p, k) => ↑(f (p ^ k)) / ↑(Real.log (↑p ^ k)))8            (Filter.atTop ⊓ Filter.principal {(p, k) | Nat.Prime p}) =9          ⊤ →10        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.

Sources

Search problems.science