qedbot

Erdős·erdos:1

Erdős Problem 1

problem formal record: solved source: disproved (Lean)$500 F2 declared

No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.

Fidelity F2: The correspondence is declared through an alignment table and written divergences.

number theory, additive combinatorics·Source

AI activity

How grades work

No AI contribution recorded against this statement.

Claimed on erdosproblems.com

2

Proof claims posted on erdosproblems.com, which says that listing a claim “is no guarantee of proof correctness”. The register records who claims what, with which systems, and links to each claim there. Nobody has examined them, and none counts in the register's totals.

Fidelity

How fidelity is graded

F2 declared. The correspondence is declared through an alignment table and written divergences.

declares divergences from its source

Declared by the projects

1

As each project's formalization.yaml states it.

Erdős problem #1: disprooftadamcz/erdos1 · joined by anchor · no independent check

Read formalization.yaml

method
autonomous — GPT-6 Astra (pre-release version, OpenAI)
review
other — mechanically verified (comparator: lean kernel replay, standard axioms only) in the benchmark harness and again in this repository's ci; preliminary informal reading of the argument by thomas f. bloom; no independent refereeing (Thomas F. Bloom)
sorry
0 unproved goals declared
sources
Disproof of Erdős problem #1: A sum-distinct set A ⊆ {1,…,N} of size n does not force N ≫ 2^n. — other; Erdős problem #1 (erdosproblems.com) — background; Some of my new and almost new problems and results in combinatorial number theory — background; Problems and results in additive number theory — background
related
google-deepmind/formal-conjectures/blob/488aade228ec37880b8fec178c173c07d279bb53/FormalConjectures/ErdosProblems/1.lean — builds-on; epoch-research/LeanOpenProblems/blob/77882c437ca1dfefab3b27fa00f1d29788100311/apn/data/erdos/Isolated/Erdos1.erdos_1.lean — builds-on
divergences
None known between the compared theorem and the conjecture as stated on erdosproblems.com. The formal conjecture `Erdos1.erdos_1` (Formal Conjectures) reads: there is `C > 0` such that `C · 2^|A| < N` for every `N ≠ 0` and every sum-distinct `A ⊆ {1, …, N}`; the compared theorem is exactly its negation. The hypothesis `N ≠ 0` only excludes the degenerate empty interval. The disproof is ineffective (no explicit `n(ε)`).
checked by
nobody independent of its authors yet

Follow and discuss

All discussion

Discussion and bounties for this problem load here.

Something wrong or missing here? Request a correction or add a claim, with its sources.

Formal material

Formal statements · 1
Cited proofs · 2
Also known as · 3
  • https://www.erdosproblems.com/1
  • https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1.lean
  • FormalConjectures/ErdosProblems/1.lean

Cite this record

qed.bot, “Erdős Problem 1”, https://qed.bot/s/erdos-1, as of 30 Sep 2026.

This record as plain text, with each claim, its grades and its sources.