The Erdos-Turan set is Sidon, for $p$ prime

Proved

SidonSqrtN.et_sidon

by aarontcao · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricscombinatoricsnumber-theory

All pairwise sums of $\{2pk + (k^2 \bmod p) : 0 \le k < p\}$ are distinct when $p$ is prime.

Write the four elements as $2pk_i + r_i$ with $r_i = k_i^2 \bmod p$ . Each $r_i$ is below $p$ , so $r_1 + r_2 < 2p$ and $r_3 + r_4 < 2p$ . Uniqueness of quotient and remainder modulo $2p$ splits the single equation $a_1 + a_2 = a_3 + a_4$ into $k_1 + k_2 = k_3 + k_4$ and $r_1 + r_2 = r_3 + r_4$ . The second reads $k_1^2 + k_2^2 \equiv k_3^2 + k_4^2 \pmod p$ . So the two pairs have equal sum and equal sum of squares, hence equal sum and equal product, hence they are the roots of the same quadratic over the field $\mathbb{F}_p$ .

Primality is exactly what makes $\mathbb{Z}/p\mathbb{Z}$ a field, and the construction genuinely fails at $p = 4, 6, 8, 9, 10$ .

Preamble

import Mathlib

Formal statement

namespace SidonSqrtN

theorem et_sidon (p : ℕ) (hp : p.Prime) :
    ∀ a ∈ (Finset.range p).image (fun k => 2 * p * k + k ^ 2 % p),
    ∀ b ∈ (Finset.range p).image (fun k => 2 * p * k + k ^ 2 % p),
    ∀ c ∈ (Finset.range p).image (fun k => 2 * p * k + k ^ 2 % p),
    ∀ d ∈ (Finset.range p).image (fun k => 2 * p * k + k ^ 2 % p),
      a + b = c + d → (a = c ∧ b = d) ∨ (a = d ∧ b = c) := by sorry

end SidonSqrtN

Source

Paul Erdos and Pal Turan, "On a problem of Sidon in additive number theory, and on some related problems", J. London Math. Soc. 16 (1941) 212-215

Read-back

What the Lean code literally says, in plain math · claude-opus-5

READ-BACK

Fix a natural number p and assume p is prime. Form the finite set S of natural numbers obtained as the image of {0, 1, ..., p-1} under k -> 2pk + (k^2 mod p). The parse is (2pk) + (k^2 mod p): the remainder is taken of k^2 alone, not of the whole expression, and the shift 2pk is not inside the modulus. The remainder is natural-number remainder, lying in [0, p-1], while the shifts 2pk step by 2p, so distinct k give distinct values and S has exactly p elements, one in each interval [2pk, 2pk + p). The claim is that for any four elements a, b, c, d of S, the equation a + b = c + d forces either (a = c and b = d) or (a = d and b = c): the unordered pair is recovered from its sum. The four elements are not required to be distinct, so the case a = b is included and the assertion also forbids c + d = 2a with c not equal to d. This is the strong B_2 (Sidon) condition on S, not the weaker version restricted to pairs of distinct elements. Quantification runs over elements of S, not over indices k. The declaration has no proof body.

QUANTIFIER ORDER p : N, universal, scope is everything after it. hp : p is prime, scope is everything after it. a in S, universal, bounded. b in S, universal, bounded, inside a. c in S, universal, bounded, inside b. d in S, universal, bounded, inside c. Then the implication a + b = c + d -> conclusion. No existentials anywhere.

HYPOTHESES hp (p prime): rules out p = 0, p = 1, and all composite p. It forces p >= 2, so the index range is nonempty and the modulus is nonzero (no natural-number mod-by-zero fallback). It is the only hypothesis. No typeclass constraints appear; p is a bare natural and all arithmetic is on N. No hypothesis constrains a, b, c, d beyond membership in S; in particular no distinctness and no ordering.

DEGENERATE CASES S is never empty here: k = 0 gives 0 in S for every p, so the quantified family is nonempty and the statement is not vacuous. p = 2 gives S = {0, 5}; p = 3 gives S = {0, 7, 13}. Were p = 0 allowed, the index range would be empty, S empty, and the statement vacuously true; primality excludes that. Likewise p = 1 would give S = {0}, where the claim is immediate. The hypothesis a + b = c + d is always satisfiable (take a = c, b = d), so the implication has non-trivial instances.

UNREADABLE Nothing.

Human review

Endorsed by Shuze Chen · Sep 17, 2026
Endorsed by aarontcao · Sep 17, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The Erdos-Turan set is Sidon, for ppp prime

The Erdos-Turan set is Sidon, for $p$ prime