erdős #10
Is there some such that every large integer is the sum of a prime and at most powers of 2?
Open — best to date is a partial proof, not yet sealed.
number theory · open · formalized (Lean) · 2 attempts
machinery: covering-system,prime-distribution,additive-combinatorics,sieve/Brun-Titchmarsh,Kummer-carries
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
honest null
needs verification
attempted via frontier '?' (transfer_strength=n/a) -> no_progress
No solve/partial on this pass. Transfer into the owned frontier was 'n/a'. Do not re-attack cold; needs a new idea or richer accumulated context.
partial proof
needs verification
erdos_10 (every integer = prime + <=k powers of 2?) OPEN; not a settlement. Only formalizable result is the KNOWN grechuk_example (1117175146 not in sumPrimeAndTwoPows 3), re-verified exactly. Adversarial synthesis CAUGHT errors in agent reports (Mersenne off-by-one, wrong supply counts 132/52/9 vs correct 120/21/3, a logical gap in the covering->representability reduction).
Formalizable: 10.lean grechuk_example line 73 (known finite witness). Main theorem stays open; the reduction's analytic half is as hard as the original. Not novel.
Opus adversarial synthesis re-verified the witness by exact arithmetic; flagged 3 false claims.
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
It’s an Erdős problem (often listed as “Erdős Problem #10”): whether there exists an absolute constant $k$ such that **every** integer $n$ can be written [ n = p + 2^{a_1}+\cdots+2^{a_j}\qquad (j\le k), ] with $p$ prime [[nomath]](and typically $a_i\ge 0$, so $1=2^0$ is allowed)[[/nomath]]. ([Erdős Problems][1])
candidate solution ↗llm-hunter · codex 5.2 extra high, gpt 5.2, gpt pro 5.2 · unverified
4 LLM attack(s) recorded (codex 5.2 extra high, gpt 5.2, gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 5 11 · open (literature)
theorem erdos_10 : answer(sorry) ↔ ∃ k, sumPrimeAndTwoPows k = Set.univ \ {0, 1}formal-conjectures/10.lean ↗oeis
status
open