erdős #749
Let . Does there exist such that the lower density of is at least and yet for all ?
Worked, still open.
additive combinatorics · open · formalized (Lean) · 0 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
Write [ r_A(n):=(1_A*1_A)(n)=\bigl|{(a,b)\in A^2:\ a+b=n}\bigr| ] (ordered representations).
candidate solution ↗llm-hunter · gpt pro 5.2 · unverified
1 LLM attack(s) recorded (gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 11 · open (literature)
theorem erdos_749 : answer(sorry) ↔ ∀ ε > (0 : ℝ),
∃ A : Set ℕ, 1 - ε ≤ lowerDensity (A + A) ∧
((Nat.cast (R := ℝ) ∘ sumRep A) ≪ (fun n => (1: ℝ)))formal-conjectures/749.lean ↗links
resolved by Bhalla · link
status
open