Erdős Problem 1144: Random Completely Multiplicative Function Summation

### What is the conjecture

Let $f$ be a random completely multiplicative function on the positive integers, where for each prime $p$, we independently choose $f(p) \in \{-1, 1\}$ with equal probability. A function $f$ is completely multiplicative if $f(mn) = f(m)f(n)$ for all positive integers $m, n$. The conjecture asks whether with probability 1, $$\limsup_{N\to \infty}\frac{\sum_{m\leq N}f(m)}{\sqrt{N}}=\infty$$

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://www.erdosproblems.com/1144

### Prerequisites needed

**Formalizability Rating:** 2/5 (0 is best) (as of 2026-02-01)

Building blocks (1-3; from search results):
- Basic arithmetic and summation notation in Mathlib
- Probability theory foundations (probability spaces, independent random variables)
- Real analysis and limsup/liminf concepts

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition and theory of multiplicative and completely multiplicative arithmetic functions
- Probabilistic framework for independent Bernoulli-valued random functions on the set of primes with extension to all positive integers

Rating justification (1-2 sentences): The statement itself can be formulated using existing Mathlib concepts (summation, probability, limsup), but formalizing it requires building the theory of multiplicative functions as a random construction over primes. This is moderate foundational work in analytic number theory and probability theory that doesn't exist in Mathlib.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-11
* ams-60

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)