---

Wirsing, Das asymptotische Verhalten von Summen über multiplikative Funktionen. II, Acta Math. Acad. Sci. Hungar. 18 (1967), no. 3–4, 411–467, proves that for every multiplicative $f:\mathbb{N}\to\{-1,1\}$ the mean value

$$\lim_{N\to\infty}\frac{1}{N}\sum_{n\le N}f(n)$$

exists, which is the question of Problem 239 answered yes. The limit is zero unless the series $\sum_p(1-f(p))/p$ converges, and in that case it equals the Euler product value $\prod_p(1-1/p)\sum_{k\ge0}f(p^k)p^{-k}$. The theorem is stated in this form in Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter III.4 (Mean values of multiplicative functions), and Elliott, Probabilistic Number Theory I, Chapter 6 (Theorems of Delange, Wirsing, and Halász). Erdős had conjectured the existence of the mean value, as the site records through the Erdős references on the problem page. The page's date is the journal issue's month, September 1967, as Crossref records it; the issue gives no day, so the first of the month stands in for it.

Depends on. Nothing in this wiki; the result rests on the refereed paper linked above.

Formalization. The repository plby/lean-proofs holds src/latest/ErdosProblems/Erdos239.lean (1,642 lines at the pinned commit linked above, the file's last change of 2026-09-04), whose header declares it a Lean formalization of a solution to the problem with Eduard Wirsing as informal author, the Formal Conjectures authors as statement authors and Codex and GPT-5.6 Sol as formal authors, its copyright line naming Boris Alexeev and OpenAI Codex. Its module docstring says that every real multiplicative function with values $\pm1$ has a Cesàro mean, the conjecture proved by Wirsing and generalized by Halász, and that the statement agrees with the one in formal-conjectures, multiplicativity being required only for coprime arguments. Its theorem erdos_239 states: for every $f:\mathbb{N}\to\mathbb{R}$ with $f(n)\in\{1,-1\}$ for $n\ge1$, $f(mn)=f(m)f(n)$ for coprime $m,n$ and $f(1)=1$, there is an $L$ with $N^{-1}\sum_{n\le N}f(n)\to L$. The file imports two modules of the same repository's problem 67 and problem 69 developments (Erdos67.MRRealPrefixCompleteStability, Erdos69.HalaszMean); the file contains no sorry, no axiom and no #print axioms line. Jayyhk/erdos-lean holds a flattened copy with the import closure concatenated and Mathlib as the only import (the second formalization link). The statement file of formal-conjectures carries no formal_proof attribute for this problem at its pinned commit (see the problem page). The file declares itself a formalization of Wirsing's result, so it is recorded here and gets no page of its own; nothing was built, kernel-checked or audited in this repository.

Acceptance. Refereed: the paper appeared in Acta Mathematica Academiae Scientiarum Hungaricae, volume 18, issue 3–4 (1967). Reviewed: the site's curator, Thomas F. Bloom, credits the affirmative answer to Wirsing in the problem's commentary, and Halász's refereed theorem of 1968 (Halász 1968) generalizes it to complex-valued multiplicative functions of modulus at most one. The site's label is PROVED (LEAN) and the community database records a Lean formal status dated 2026-08-23; the Lean development linked above was not built or audited in this repository, so no formalized evidence is listed. The paper is not carded in the library; the statement follows the site's commentary and the textbook accounts cited above.