Newmans Conjecture

### What is the conjecture

The partition function $p(n)$ counts the number of ways to express a nonnegative integer $n$ as a sum of positive integers without regard to order. Newman's conjecture asserts that for every integer $m \geq 1$ and every residue class $r$ with $0 \leq r < m$, there are infinitely many nonnegative integers $n$ such that the partition function satisfies the congruence:
$$p(n) \equiv r \pmod{m}$$
In other words, every residue class modulo any positive integer $m$ appears infinitely often in the sequence of partition function values.

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

**Sources:**
- https://en.wikipedia.org/wiki/Newman%27s_conjecture
https://mathworld.wolfram.com/NewmansConjecture.html
https://arxiv.org/abs/2005.05142
https://arxiv.org/abs/1310.3477

### Prerequisites needed

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

The partition function $p(n)$ has some basic formalization in Mathlib (e.g., in Nat.Partition), but the conjecture requires:
1. A formal definition of the partition function and its congruences modulo integers
2. Formalization of the notion of "infinitely many" in a modular arithmetic context
3. Lemmas relating congruences and residue classes in modular arithmetic

While modular arithmetic and congruences are well-established in Mathlib, the specific setup for stating this conjecture about partition function congruences requires moderate infrastructure development to connect partition combinatorics with modular number-theoretic concepts appropriately.

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

* ams-11
* ams-05

### 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)

Start by reading the existing Nat.Partition formalization and the cited sources to determine the precise statement of Newman's conjecture. Define the required modular and infinitude infrastructure, then formalize the conjecture and verify that the resulting Lean statements compile.

Written by the indexing model from the issue text.