Problem 491

../

claims/: The 2 claim pages of Problem 491, one per claimant's result; the problem's standing derives from them.

---

Statement. Let $f:\mathbb{N}\to \mathbb{R}$ be an additive function (i.e. $f(ab)=f(a)+f(b)$ whenever $(a,b)=1$). If there is a constant $c$ such that $\lvert f(n+1)-f(n)\rvert <c$ for all $n$ then must there exist some $c'$ such that

$$f(n)=c'\log n+O(1)?$$

Status. Proved. The site labels the problem PROVED (page last edited 2026-04-01) and credits Wirsing [Wi70], whose theorem answers the question yes; the accepted full claim is on the claim page.

Source. erdosproblems.com/491, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #491, https://www.erdosproblems.com/491.

References.

• [Er46] Erdős, P., On the distribution function of additive functions. Annals of Math. (1946), 1-20.
• [Wi70] E. Wirsing, A characterization of $\log n$ as an additive arithmetic function. Symposia Math. (1970), 45-57.

Formalization. Statement in formal-conjectures (pinned at the commit of 2026-09-18), which records as the problem's formal proof a Lean 4 development in the lean-proofs repository (pinned commit), which this corpus has neither built nor audited.

Current assessment

The question is answered yes. Erdős [Er46] proved the exact conclusion $f(n)=c\log n$ under either of two stronger hypotheses, that $f(n+1)-f(n)\to0$ or that $f$ is nondecreasing, an accepted partial claim on its claim page. Wirsing [Wi70] proved the full statement: bounded consecutive differences force $f(n)=c'\log n+O(1)$ for some constant $c'$. The site's curator records the problem as proved by Wirsing, which is the acceptance evidence on the claim page; the paper appeared in a proceedings volume, so no refereed evidence is listed. A Lean 4 development in Boris Alexeev's lean-proofs repository proves the statement and is recorded by the formal-conjectures catalog as the problem's formal proof; it is a formalization link on the claim page, and this corpus has neither built nor audited it, so it is not evidence.

Known Results

• [Er46]: if $f(n+1)-f(n)=o(1)$, or if $f(n+1)\ge f(n)$ for every $n$, then $f(n)=c\log n$ for a constant $c$ (card); the accepted partial claim on Erdős 1946.
• [Wi70]: if $\lvert f(n+1)-f(n)\rvert<c$ for every $n$, then $f(n)=c'\log n+O(1)$ for a constant $c'$; the accepted claim on Wirsing 1970.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

• erdos_1946_distribution_function_additive_functions
• erdos_1946_distribution_function_additive_functions / conjecture_p3
• erdos_1946_distribution_function_additive_functions / theorem_11
• erdos_1946_distribution_function_additive_functions / theorem_13
• erdos_1946_distribution_function_additive_functions / theorem_5