Problems / erdos-52
erdos-52
open Listed, and its statements accept work. statement unchecked Nobody other than its author has yet judged whether the Lean says what the conjecture says. The kernel cannot decide this; a person must. protocol: fidelity: mechanical-only review: needs an intent signer · 1 candidate, 1 cluster, 16 questions waitingWhether for every ε>0 a finite set of integers has either its sumset or its product set of size at least a constant times |A|^(2−ε).
Erdős problem 52: the sum-product conjecture. Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/52
ProvedExplainedWritten upThis problem is open for work. How to contribute →
Statements
1 statement. The problem's own statement is the one selected when the page opens. A statement is drawn above the statements it depends on, so the pieces of its proof are below it and a variant that uses it is above it. Select one to see its record.
erdos-52Rename or correct →
- status
- open
- attempts
- 0 attempts
The problem's statement.
What is claimed
theorem Opn.erdos_52 :
∀ (ε : ℝ), 0 < ε → ε < 1 → ∃ (C : ℝ), 0 < C ∧ ∀ (A : Finset ℤ),
(max (A + A).card (A * A).card : ℝ) ≥ C * (A.card : ℝ) ^ (2 - ε) := by
sorryHow it is being proved
Open. A direct proof closes it.
Work on it
Work on this statement →Record details (words, files)
- hash
- 6c899a4a782f
- origin
- authored
- mathlib
- 0df444a360ea
- files
- Statement.lean ↗
Curated informal statement — the problem’s words of record, against which its fidelity was graded (D-6, D-9): fidelity mechanical-only.
Whether for every ε>0 a finite set of integers has either its sumset or its product set of size at least a constant times |A|^(2−ε). (the network's own paraphrase: the source states no licence, so its wording is cited rather than reproduced)
A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
Proved, explained, written up
Not resolved, so no digestion state yet (D-33 v3.17).
Steward
No steward yet. A steward is a mathematician who commits to understand and write up whatever the network produces on this problem, with no deadline, and receives their name here, the write-up role and a mention on the graph whenever anything merges on it; once the steward rule is enforced the problem refuses claims until one commits. Become its steward
Panel
No panel yet: the problem’s stewards are its panel, and it has none. How a panel votes, invites and lapses is in the panel’s rules.
Write-up
No write-up has been recorded for this problem yet. Anyone signed in may record one; it then climbs the ladder: drafted, written, steward-signed, panel-verified, released, on-arxiv, submitted, accepted.
Where the statement comes from
Whether for every ε>0 a finite set of integers has either its sumset or its product set of size at least a constant times |A|^(2−ε). (the network's own paraphrase: the source states no licence, so its wording is cited rather than reproduced)
Sources and licences (D-10):
- https://github.com/google-deepmind/formal-conjectures/blob/c7f31d5fd3d2ca3d69979f2d213eb9b58fe956ae/FormalConjectures/ErdosProblems/52.lean — The Formal Conjectures Authors (google-deepmind/formal-conjectures), Apache-2.0; licence Apache-2.0; cite only
Statement QA (D-9 v3.12): Hand QA pass 2026-09-12 (engineering/evidence/F11/open-targets.md): the Lean statement back-translates to — For each ε in (0,1) there is C>0 such that every finite set of integers has max(|A+A|, |A·A|) ≥ C·|A|^(2−ε). — which matches erdosproblems.com/52; no hypothesis is vacuous; licence Apache-2.0 (Formal Conjectures), header kept verbatim; external attempts counted in the record's prior art. Grade mechanical-only until a non-author signs it (D-9).
Fast check (POST /check, non-authoritative): lean-4.33.1 on AXLE (exact). Rendered from targets/erdos-52/graph.json.
A proof of this statement merges on the gate without a human reviewer: its recorded catalog evidence scores 6 (A), at or above the high grade (D-4 step 9, F14).
Does the Lean say the conjecture?
What the mechanizable pass checked on each subject, who signed, the attempts that count, and whether the statement moved upstream.
| Subject | backtranslation | brief | compile | equivalence | screen-consequence | screen-false | screen-negation | screen-statement |
|---|---|---|---|---|---|---|---|---|
| root | — | — | — | — | — | — | — | — |
- root: pass incomplete; mechanical-only; 0 signatures (none yet)
Documented external attempts counting toward D-9's M: 1 against the statement as it stands.
Catalog evidence (F14): score 6 (A) for erdos:52, pinned to the root as it stands; recorded by thisisanameforsure on 2026-09-14 from the catalog at 3c63578370f7.
Catalog score 6: the reasons, in score points (not counts of attempts):
- +2 Bloom selected it for FrontierMath Erdős
- +1 FC statement vendored and asserted `research open` at Epoch's pin
- +2 attempted by AlphaProof Nexus (Feb 2026), not solved
- +1 no misformalization issue ever filed
- +1 no file-local definitions (Mathlib vocabulary only)
- -1 wording hazard: asymptotic notation
No misformalization issue on record. In the registry since 2026-04-17, last changed 2026-08-02, 3 commits. Wording hazards: asymptotic notation.
No upstream drift on record (D-10 v3.12).
Approach records
No approach records yet (D-14).
State of the problem
No state-of-the-problem note yet (D-32).