---

Wirsing [Wi70] proves that if $f:\mathbb{N}\to\mathbb{R}$ is additive and there is a constant $c$ with $\lvert f(n+1)-f(n)\rvert<c$ for every $n$, then there is a constant $c'$ with $f(n)=c'\log n+O(1)$, which answers the question yes. The paper, A characterization of $\log n$ as an additive arithmetic function, appeared in Symposia Mathematica IV (INDAM, Rome, 1968/69), Academic Press, London (1970), 45–57; no online posting of it is known to this corpus, and no earlier circulation date is recorded, so the page is dated by the publication year. Erdős [Er46] had proved the exact conclusion $f(n)=c\log n$ under the stronger hypotheses that $f(n+1)-f(n)\to0$ or that $f$ is nondecreasing (accepted partial claim), and Theorem V of that paper supplies the criterion that pushes an additive function whose values cluster on a positive-density set toward a multiple of the logarithm (card); Wirsing's theorem completes that line for bounded differences.

Acceptance. Reviewed: the site's curator, Thomas F. Bloom, records the problem as proved by Wirsing (problem page last edited 2026-04-01). The venue is a published proceedings volume rather than a journal, so the evidence listed is the curator's acceptance alone. Formalization: a Lean 4 proof in the lean-proofs repository, linked above at its pinned commit, proves erdos_491, that bounded consecutive differences of an additive function give a logarithmic main term with a bounded residual; its modules present themselves as Wirsing's resolution of the problem. The file names no author (the repository's commits are by Boris Alexeev) and no AI system, and the formal-conjectures statement file ErdosProblems/491.lean records it as the problem's formal proof. This corpus has neither built that proof nor audited its statement, so it is not listed as evidence.

Depends on. No page of this wiki: the result rests on the cited paper alone.