pith. sign in

arxiv: 2605.03274 · v2 · submitted 2026-05-05 · 🧮 math.CO

Formalizing Singer Sidon Constructions and Sidon Set Infrastructure in Lean 4

David B. Hulak , Arthur F. Ramos , Ruy J. G. B. de Queiroz This is my paper

Pith reviewed 2026-05-13 07:48 UTC · model grok-4.3

classification 🧮 math.CO
keywords Sidon setsSinger constructionLean 4formal verificationadditive combinatoricsfinite fieldsErdős problem 30
0
0 comments X

The pith

For every prime power q there exists a Sidon set of size q plus one modulo q squared plus q plus one.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper supplies a complete Lean 4 formalization of Singer's classical construction of large Sidon sets. It proves that for any prime power q the cyclic group of order q squared plus q plus one contains a Sidon set with exactly q plus one elements. The argument first builds the base field with q elements and its cubic extension, extracts the trace kernel as a two-dimensional subspace, uses intersection properties to obtain the multiplicative Sidon property in the quotient, and finally transfers that property to distinct pairwise sums under ordinary modular addition. The work also assembles a reusable library containing definitions of interval and modular Sidon sets, the extremal function h of N, several explicit upper and lower bounds, and a conditional route from prime-gap hypotheses to the full asymptotic form of Erdős Problem 30. A sympathetic reader cares because the formalization forces every step of the classical argument to be stated without gaps and produces machine-checkable building blocks for additive combinatorics.

Core claim

For every prime power q equals p to the k the Singer construction produces a Sidon set of cardinality q plus one inside the integers modulo q squared plus q plus one. The proof proceeds by constructing the finite field of order q and its degree-three extension, identifying the trace kernel as a two-dimensional vector space over the base field, applying a geometric intersection argument to establish the multiplicative Sidon property inside the quotient group, and transferring the distinct-products condition to the distinct-sums condition under integer addition modulo the order.

What carries the argument

The transfer map that converts the multiplicative Sidon property of the trace-kernel quotient into an additive Sidon property under integer addition modulo q squared plus q plus one.

If this is right

  • The prime-field case serves as the explicit base from which the general prime-power result follows by field extension.
  • The library supplies unconditional two-sided bounds establishing h of N equals theta of square root of N together with exact floor-rounded statements that hold for every N at least 5.
  • A conditional reduction shows that subpolynomial prime gaps combined with a subpolynomial error term for the upper bound on h of N imply the full Erdős estimate h of N equals square root of N plus O sub epsilon of N to the epsilon for every epsilon greater than zero.
  • The entire Singer construction and supporting library are verified in 7,541 lines of Lean 4 code containing no active sorry statements.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The explicit treatment of the transfer step from multiplication in the quotient to addition in the integers may allow analogous formalizations for Sidon sets inside other algebraic groups.
  • The reusable library could support machine-checked exploration of variants that impose extra constraints such as sum-freeness or restricted difference sets.
  • The zero-sorry verification indicates that the classical finite-field arguments become fully amenable to formal methods once the passage from geometry to modular arithmetic is written out in full detail.

Load-bearing premise

The algebraic construction in the finite-field extension, once transferred via the quotient map, yields a set whose pairwise sums are distinct under ordinary integer addition modulo q squared plus q plus one.

What would settle it

Any prime power q together with four distinct elements a, b, c, d from the constructed set satisfying a plus b congruent to c plus d modulo q squared plus q plus one with the unordered pairs distinct would falsify the central claim.

read the original abstract

Erd\H{o}s Problem 30 asks for sharp asymptotics of the Sidon extremal function $h(N)$, and Singer's construction is the classical source of lower-bound examples matching the main term. We present a Lean 4 formalization of Singer's Sidon set construction, together with reusable Sidon-set infrastructure for additive combinatorics. For every prime power $q=p^k$, we prove the existence of a Sidon set modulo $q^2+q+1$ of cardinality $q+1$; the prime-field case $q=p$ is the base presentation. The proof proceeds through a non-trivial algebraic chain: construction of the base field and its degree-three extension, analysis of the trace kernel as a 2-dimensional subspace over the base field, a geometric argument via subspace intersections establishing the multiplicative Sidon property in the quotient group, and a transfer from quotient multiplication to modular integer addition. Around this central result, we develop a reusable Sidon set library. It comprises interval and modular Sidon sets, the extremal function $h(N)$, Lindstr\"om's cross-difference inequality, a Johnson-route shift-incidence upper bound of the form $h(N)\leq\sqrt{N}+N^{1/4}+O(1)$, representation-function identities, and unconditional two-sided $h(N)=\Theta(\sqrt{N})$ bounds with exact floor-rounded finite statements for $N\geq 5$. We further formalize a conditional reduction: subpolynomial prime gaps together with a full subpolynomial upper-error hypothesis for $h(N)$ imply the Erd\H{o}s Problem 30 estimate $h(N)=\sqrt{N}+O_\epsilon(N^\epsilon)$ for every $\epsilon>0$. The Singer/Sidon modules and transfer lemmas comprise 7,541 lines of Lean 4 with zero active uses of sorry. We describe the mathematical lessons learned, focusing on how formalization clarifies the precise scope of classical arguments and forces explicit treatment of the passage from the field-theoretic construction to integer Sidon predicates.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper presents a Lean 4 formalization of Singer's classical construction of Sidon sets together with supporting infrastructure for additive combinatorics. For every prime power q it proves the existence of a Sidon set of cardinality q+1 modulo q²+q+1 by constructing a degree-3 field extension, analyzing the trace kernel as a 2-dimensional subspace, establishing a multiplicative Sidon property in the quotient via subspace intersections, and transferring the property to ordinary modular addition. The development comprises 7541 lines with zero active 'sorry' statements and includes reusable modules for interval/modular Sidon sets, the extremal function h(N), Lindström's inequality, a Johnson-type upper bound, representation-function identities, unconditional two-sided bounds h(N)=Θ(√N), and a conditional reduction from subpolynomial prime gaps plus an upper-error hypothesis on h(N) to the Erdős Problem 30 estimate h(N)=√N + O_ε(N^ε).

Significance. If the formalization is correct, the work supplies the first machine-checked proof of Singer's construction, removing any doubt about the algebraic transfer steps and providing a verified library that can be reused for further formalizations in additive combinatorics. The explicit treatment of the passage from field-theoretic predicates to integer Sidon predicates and the conditional link to Erdős Problem 30 are concrete advances that strengthen the reliability of the classical lower-bound examples.

minor comments (2)
  1. [§3.2] §3.2: the notation for the quotient map φ is introduced without an explicit type declaration in the Lean code snippet; adding a one-line type annotation would improve readability for readers unfamiliar with the formalization.
  2. [Table 1] Table 1: the column headers for the finite-field cases use 'q=p^k' without clarifying that k is allowed to be 1; a parenthetical remark would prevent minor confusion.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript and for recommending acceptance. The referee's summary accurately captures the formalization of Singer's construction, the supporting library, and the conditional link to Erdős Problem 30.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper supplies a complete, self-contained Lean 4 formalization (7541 lines, zero sorries) of Singer's construction. The existence of a Sidon set of size q+1 modulo q²+q+1 is derived directly from the encoded axioms of finite fields, vector spaces, trace maps, subspace intersections, and the quotient transfer lemma; every predicate is machine-checked against the stated definitions without any fitted parameters, self-referential definitions, or load-bearing self-citations. The reusable library components (h(N), Lindström inequality, Johnson bound, etc.) are developed in parallel but do not enter the central existence proof as premises. The conditional reduction to Erdős Problem 30 is explicitly stated as depending on external hypotheses and is not used to establish the main theorem.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The proof rests on the standard axioms of finite fields and finite-dimensional vector spaces already present in Lean's mathlib; no new free parameters are introduced and no new entities are postulated.

axioms (2)
  • standard math Finite fields of prime-power order exist and are unique up to isomorphism
    Invoked when constructing the base field F_q and its cubic extension.
  • standard math Trace map from cubic extension to base field is F_q-linear and surjective
    Used to define the 2-dimensional kernel subspace.

pith-pipeline@v0.9.0 · 5691 in / 1432 out tokens · 38447 ms · 2026-05-13T07:48:29.537718+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

19 extracted references · 19 canonical work pages · 1 internal anchor

  1. [1]

    Alexeev and D

    B. Alexeev and D. G. Mixon,Forbidden Sidon subsets of perfect dif- ference sets, featuring a human-assisted proof, arXiv:2510.19804v2 [math.CO] preprint, first posted 2025, revised 2026. DOI: 10.48550/arXiv.2510.19804

    work page doi:10.48550/arxiv.2510.19804 2025

  2. [2]

    Balogh, Z

    J. Balogh, Z. Füredi, and S. Roy, An upper bound on the size of Sidon sets,Amer. Math. Monthly130(2023), no. 5, 437–445. DOI: 10.1080/00029890.2023.2176667

    work page doi:10.1080/00029890.2023.2176667 2023

  3. [3]

    R. C. Baker, G. Harman, and J. Pintz, The difference between consec- utive primes, II,Proc. London Math. Soc.83(2001), no. 3, 532–562. DOI: 10.1112/plms/83.3.532

    work page doi:10.1112/plms/83.3.532 2001

  4. [4]

    Bertrand, Mémoire sur le nombre de valeurs que peut prendre une fonction quand on y permute les lettres qu’elle renferme,J

    J. Bertrand, Mémoire sur le nombre de valeurs que peut prendre une fonction quand on y permute les lettres qu’elle renferme,J. École Polytech.18(1845), 123–140. (The prime-number assertion now called Bertrand’s postulate is stated there; it is formalized in Mathlib as Nat.bertrand.)

    work page

  5. [5]

    A. Best, C. Birkbeck, R. Brasca, E. Rodriguez Boidi, R. van de Velde, and A. Yang, A complete formalization of Fermat’s Last Theorem for regular primes in Lean,Ann. Formalized Math.1(2025), article 14586. DOI: 10.46298/afm.14586

    work page doi:10.46298/afm.14586 2025

  6. [6]

    R. C. Bose and S. Chowla, Theorems in the additive theory of num- bers,Comment. Math. Helv.37(1962/63), no. 1, 141–147. DOI: 10.1007/BF02566968

    work page doi:10.1007/bf02566968 1962

  7. [7]

    Cramér, On the order of magnitude of the difference between consecu- tive prime numbers,Acta Arith.2(1936), no

    H. Cramér, On the order of magnitude of the difference between consecu- tive prime numbers,Acta Arith.2(1936), no. 1, 23–46. DOI: 10.4064/aa- 2-1-23-46

    work page doi:10.4064/aa- 1936

  8. [8]

    Carter, Z

    D. Carter, Z. Hunter, and K. O’Bryant, On the diameter of finite Sidon sets,Acta Math. Hungar.175(2025), no. 1, 108–126. DOI: 10.1007/s10474-024-01499-8

    work page doi:10.1007/s10474-024-01499-8 2025

  9. [9]

    Erdős, Some unsolved problems,Michigan Math

    P. Erdős, Some unsolved problems,Michigan Math. J.4(1957), no. 3, 291–300. DOI: 10.1307/mmj/1028997963

    work page doi:10.1307/mmj/1028997963 1957

  10. [10]

    Erd¨ os and P

    P. Erdős and P. Turán, On a problem of Sidon in additive number theory, and on some related problems,J. London Math. Soc.16(1941), no. 4, 212–215. DOI: 10.1112/jlms/s1-16.4.212

    work page doi:10.1112/jlms/s1-16.4.212 1941

  11. [11]

    W. T. Gowers, B. Green, F. Manners, and T. Tao, On a conjec- ture of Marton,Ann. of Math.201(2025), no. 2, 515–549. DOI: 24 10.4007/annals.2025.201.2.5. Formalization project:https://github. com/teorth/pfr(accessed 2026-05-03)

    work page doi:10.4007/annals.2025.201.2.5 2025

  12. [12]

    R. K. Guy,Unsolved Problems in Number Theory, 3rd ed., Springer, 2004. ISBN 978-0-387-20860-2; eISBN 978-0-387-26677-0. DOI: 10.1007/978- 0-387-26677-0

    work page doi:10.1007/978- 2004

  13. [13]

    B. S. Ho, Erdős’s diameter conjecture for separated distances fails in high dimensions, arXiv:2604.15305v1 [math.CO], 2026. DOI: 10.48550/arXiv.2604.15305. Formalization project: https://github. com/boonsuan/erdos670 (accessed 2026-05-03); the Singer-specific file and commit used for comparison are cited in the main text

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2604.15305 2026

  14. [14]

    S. M. Johnson, A new upper bound for error-correcting codes, IEEE Trans. Inform. Theory8(1962), no. 3, 203–207. DOI: 10.1109/TIT.1962.1057714

    work page doi:10.1109/tit.1962.1057714 1962

  15. [15]

    Lindström, An inequality forB2-sequences,J

    B. Lindström, An inequality forB2-sequences,J. Combin. Theory6 (1969), no. 2, 211–212. DOI: 10.1016/S0021-9800(69)80124-9

    work page doi:10.1016/s0021-9800(69)80124-9 1969

  16. [16]

    Loeffler and M

    D. Loeffler and M. Stoll, Formalizing zeta andL-functions in Lean,Ann. Formalized Math.1(2025), article 15328. DOI: 10.46298/afm.15328

    work page doi:10.46298/afm.15328 2025

  17. [17]

    Mercuri, Formalising the local compactness of the adele ring,Ann

    S. Mercuri, Formalising the local compactness of the adele ring,Ann. Formalized Math.1(2025), article 14840. DOI: 10.46298/afm.14840

    work page doi:10.46298/afm.14840 2025

  18. [18]

    O’Bryant, A complete annotated bibliography of work related to Sidon sequences,Electron

    K. O’Bryant, A complete annotated bibliography of work related to Sidon sequences,Electron. J. Combin.(2004), Dynamic Survey DS11, 39 pp. DOI: 10.37236/32

    work page doi:10.37236/32 2004

  19. [19]

    Singer, A theorem in finite projective geometry and some applications to number theory,Trans

    J. Singer, A theorem in finite projective geometry and some applications to number theory,Trans. Amer. Math. Soc.43(1938), no. 3, 377–385. DOI: 10.1090/S0002-9947-1938-1501951-4. 25

    work page doi:10.1090/s0002-9947-1938-1501951-4 1938