PROVED (LEAN), the site's label. The answer is yes: Wirsing proved in 1967 that every multiplicative $f:\mathbb{N}\to\{-1,1\}$ has a mean value, and Halász generalized the theorem in 1968 (both refereed; the accepted claim pages are Wirsing 1967 and Halász 1968). The label's Lean marker refers to a community Lean formalization of Wirsing's theorem, linked from his claim page; none was built or audited here.