/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilRudin's conjecture on squares in arithmetic progressions
References:
[Ru60] Rudin, W., Trigonometric series with gaps, J. Math. Mech. 9 (1960), 203–227.
González-Jiménez, E. and Xarles, X., On a conjecture of Rudin on squares in arithmetic progressions, LMS J. Comput. Math. 17 (2014), 58–76.
open Filter Asymptotics Realnamespace RudinsConjecture$Q(N; q, a)$ is the number of perfect squares among the first $N$ terms of the arithmetic progression ${q n + a : 0 \le n < N}$.
noncomputable abbrev Q (N q a : ℕ) : ℕ := {n : ℕ | n < N ∧ IsSquare (q * n + a)}.ncardA pair $(q, a)$ describes a non-trivial arithmetic progression if $q, a \ge 1$, $\gcd(q, a) = 1$, and $(q, a) \neq (1, 1)$.
def IsNontrivial (q a : ℕ) : Prop :=
1 ≤ q ∧ 1 ≤ a ∧ Nat.Coprime q a ∧ (q, a) ≠ (1, 1)$Q(N) = \max Q(N; q, a)$, the largest number of perfect squares occurring among the first $N$ terms of any non-trivial arithmetic progression. The supremum is over a set of naturals that is bounded above by $N$ (each progression has only $N$ terms), so it is attained.
noncomputable def Qmax (N : ℕ) : ℕ :=
sSup {m : ℕ | ∃ q a : ℕ, IsNontrivial q a ∧ Q N q a = m}Sanity check: the progression $24 n + 1$ is non-trivial.
@[category test, AMS 11]
theorem isNontrivial_24_1 : IsNontrivial 24 1 := ⊢ IsNontrivial 24 1
refine ⟨⊢ 1 ≤ 24 All goals completed! 🐙, ⊢ 1 ≤ 1 All goals completed! 🐙, ⊢ Nat.Coprime 24 1 All goals completed! 🐙, ⊢ (24, 1) ≠ (1, 1) All goals completed! 🐙⟩
Sanity check: there are no squares among the first 0 terms of any progression.
@[category test, AMS 11]
theorem Q_zero (q a : ℕ) : Q 0 q a = 0 := q:ℕa:ℕ⊢ Q 0 q a = 0
All goals completed! 🐙
Sanity check pinning Q to a concrete value: among the first 6 terms of 24 n + 1, namely
1, 25, 49, 73, 97, 121, exactly four are perfect squares (1, 25, 49, 121), so
Q 6 24 1 = 4. This validates the definition of Q and matches the claim that 24 n + 1 is the
extremal progression.
hset:{n | n < 6 ∧ IsSquare (24 * n + 1)} = {0, 1, 2, 5}hcoe:{0, 1, 2, 5} = ↑{0, 1, 2, 5}⊢ {0, 1, 2, 5}.card = 4
All goals completed! 🐙Rudin's conjecture. The maximal number of squares among the first $N$ terms of a non-trivial arithmetic progression grows at most like $\sqrt{N}$: $$Q(N) = O(\sqrt{N}).$$
@[category research open, AMS 11]
theorem rudins_conjecture :
(fun N : ℕ => (Qmax N : ℝ)) =O[atTop] fun N : ℕ => Real.sqrt N := ⊢ (fun N ↦ ↑(Qmax N)) =O[atTop] fun N ↦ √↑N
All goals completed! 🐙A stronger form of Rudin's conjecture: for every $N \ge 6$, the arithmetic progression $24 n + 1$ attains the maximum $Q(N)$.
@[category research open, AMS 11]
theorem rudins_conjecture_strong (N : ℕ) (hN : 6 ≤ N) : Q N 24 1 = Qmax N := N:ℕhN:6 ≤ N⊢ Q N 24 1 = Qmax N
All goals completed! 🐙The strongest form of Rudin's conjecture also asserts uniqueness: for $N \ge 6$, any non-trivial arithmetic progression attaining the maximum $Q(N)$ has common difference $24$. (Its initial term is then forced by $\gcd(24, a) = 1$; the progression $24n + 1$ is the canonical representative.)
@[category research open, AMS 11]
theorem rudins_conjecture_unique (N : ℕ) (hN : 6 ≤ N) (q a : ℕ)
(hqa : IsNontrivial q a) (hmax : Q N q a = Qmax N) : q = 24 := N:ℕhN:6 ≤ Nq:ℕa:ℕhqa:IsNontrivial q ahmax:Q N q a = Qmax N⊢ q = 24
All goals completed! 🐙end RudinsConjecture