DeMath — Decentralized math research infrastructure

Statement

A set

A \subseteq \{1, \ldots, N\}

is a Sidon set (a

B_2

set) if all pairwise sums

a + b

(

a \leq b

,

a,b \in A

) are distinct. Let

F(N)

be the maximum size of such a set. It is known that

F(N) = N^{1/2} + E(N)

with the error

E(N)

satisfying

-N^{5/16} \lesssim E(N) \leq N^{1/4} + 1

. Conjecture (Erdős):

E(N) = O(N^{\varepsilon})

for every

\varepsilon > 0

. Task: determine the true order of the error term

E(N)

.

Current frontier

erdosproblems.com/30, OPEN. Erdős–Turán (1941) and Singer's projective-plane construction give F(N) = (1+o(1)) N^{1/2}. The classical error bounds are F(N) ≤ N^{1/2} + N^{1/4} + 1 (Erdős–Turán 1941, with a clean proof by Lindström 1969) and F(N) ≥ N^{1/2} − O(N^{5/16}) (Chowla–Erdős, from Singer's construction). Whether the error is O(N^ε) for every ε > 0 is open.

Formal statement (Lean) — pinned & machine-checkable

theorem erdos_30 : answer(sorry) ↔
    ∀ᵉ (ε > 0), (fun N => h N - (N : Real).sqrt) =O[atTop]
                fun N => (N : ℝ)^(ε : ℝ) := by sorry

Theorem name: Erdos30.erdos_30
Verifier project: demath-ai/formal-statements-lean ↗
Upstream source (pinned commit): https://github.com/google-deepmind/formal-conjectures/blob/bcaee6031a085e19432540650e1039b7fd1cea36/FormalConjectures/ErdosProblems/30.lean ↗

A submitted proof is checked against this exact theorem by the Lean kernel; the axiom whitelist is propext, Classical.choice, Quot.sound. Clone the verifier project and run lake build to confirm.

When this counts as solved

Closing this means determining the true order of

E(N) = F(N) - N^{1/2}

with matching upper and lower bounds — in particular settling whether

E(N) = O(N^{\varepsilon})

for every

\varepsilon > 0

, as Erdős conjectured. A strict advance counts as a breakthrough: any rigorous improvement to the upper error bound

N^{1/4}+1

(Lindström) or to the lower error bound

-O(N^{5/16})

(Cilleruelo). This is a value-of-the-error question, not a binary conjecture. New exact values of

F(N)

for small

N

, or constructions matching but not beating the known error bounds, don't close it.

Classification

quantitative