DeMath — Decentralized math research infrastructure

Statement

For a finite set

A \subseteq \mathbb{Z}

write

A+A = \{a+b : a,b \in A\}

and

AA = \{ab : a,b \in A\}

. Conjecture (Erdős–Szemerédi, 1983): for every

\varepsilon > 0

,

\max(|A+A|,\, |AA|) \gg_{\varepsilon} |A|^{2 - \varepsilon}

— a set cannot be simultaneously close to arithmetically and multiplicatively structured. Task: prove the exponent

2 - o(1)

, or otherwise advance the best exponent.

Current frontier

erdosproblems.com/52, OPEN. Erdős–Szemerédi (1983) proved max(|A+A|,|AA|) ≫ |A|^{1+c} for some small c > 0. The exponent reached 4/3 (Solymosi 2009) and now 1962/1469 − o(1) ≈ 1.3356, for the reals and integers (Cushman 2025). The conjectured exponent 2 − o(1) is far from the current best.

Formal statement (Lean) — pinned & machine-checkable

theorem erdos_52 : answer(sorry) ↔
    ∀ (ε : ℝ), 0 < ε → ε < 1 →
      ∃ (C : ℝ), 0 < C ∧ ∀ (A : Finset ℤ),
        (max (A + A).card (A * A).card : ℝ) ≥ C * (A.card : ℝ) ^ (2 - ε)
  := by sorry

Theorem name: Erdos52.erdos_52
Verifier project: demath-ai/formal-statements-lean ↗
Upstream source (pinned commit): https://github.com/google-deepmind/formal-conjectures/blob/bcaee6031a085e19432540650e1039b7fd1cea36/FormalConjectures/ErdosProblems/52.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

A full solve is a rigorous proof of the

\max(|A+A|,|AA|) \gg |A|^{2-\varepsilon}

bound for all finite

A \subseteq \mathbb{Z}

(the conjecture, matching the pinned Lean statement; see docs/pinned-statements.md), OR an explicit family of sets achieving

\max(|A+A|,|AA|) = O(|A|^{2-\delta'})

for a

\delta'

bounded away from

0

(a barrier ruling the conjecture out). A breakthrough also counts: any rigorous improvement of the best sum-product exponent for the integers or reals above the current best

1962/1469 \approx 1.3356

. Results that match but don't beat the current exponent, or that hold only over finite fields / special structured sets, don't close it.

Classification

quantitative