Rudin's Conjecture on Squares in Arithmetic Progressions

[franzhusch]

What is the conjecture

Let $Q(N; q, a)$ denote the number of perfect squares in the arithmetic progression ${qn + a : n = 0, 1, \ldots, N-1}$, where $q, a \geq 1$ and $\gcd(q, a) = 1$ with $(q, a) \neq (1, 1)$. Let $Q(N) = \max {Q(N; q, a)}$ over all such non-trivial arithmetic progressions.

Rudin's Conjecture claims that $Q(N) = O(\sqrt{N})$. A stronger form of the conjecture states that for $N \geq 6$, the arithmetic progression $24n + 1$ attains the maximum and is the unique such progression (up to equivalence).

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

Sources:

• https://en.wikipedia.org/wiki/Rudin%27s_conjecture, https://www.cambridge.org/core/journals/lms-journal-of-computation-and-mathematics/article/on-a-conjecture-of-rudin-on-squares-in-arithmetic-progressions/CCC59F8F8B8FB126A3ED6C8ADF6E8393, https://arxiv.org/abs/1301.5122, https://mat.uab.cat/~xarles/rudin.pdf

Prerequisites needed

Formalizability Rating: 1/5 (0 is best) (as of 2026-02-13)

Building blocks (1-3; from search results):

• Set.IsAPOfLengthWith from FormalConjecturesForMathlib/Combinatorics/AP/Basic.lean for arithmetic progression definitions
• Nat.sqrt and Finset.card from Mathlib for counting and big-O notation
• Standard Mathlib definitions for perfect squares and finite sets

Missing pieces (exactly 2; unclear/absent from search results):

• A helper function to count perfect squares in a specific arithmetic progression parameterized by (q, a)
• A formalization of the big-O asymptotic bound in the context of arithmetic combinatorics

Rating justification (1-2 sentences): The core mathematical objects (arithmetic progressions, cardinality, perfect squares) are available in Mathlib and FormalConjecturesForMathlib. Only minor helper definitions are needed to state the conjecture precisely, making it straightforward to formalize.

AMS categories

• ams-11
• ams-05

Choose either option

• I plan on adding this conjecture to the repository
• 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

Feedback on mistakes/hallucinations: link

[Rafiaminhaj]

Hello @franzhusch,

I would like to work on this issue as part of my OSCG 2026 open source contributions.

I have gone through the conjecture description and the listed prerequisites, including arithmetic progression definitions, perfect squares, and finset cardinality in Mathlib. I am particularly interested in contributing by formalizing Rudin's Conjecture and implementing the required helper functions, such as counting perfect squares in arithmetic progressions and expressing the asymptotic big-O bound.

I will begin by studying the relevant modules in Mathlib and FormalConjecturesForMathlib to ensure the implementation follows the repository's conventions.

Please let me know if you have any suggestions, preferred approach, or references I should review before starting.

Thank you!

[franzhusch]

Hi Rafia,

Sounds good :)