If $A \subset N$ is a Sidon set then must the complement of $A$ contain an infinite arithmetic progression?

Worked, still open.

additive combinatorics · solved · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

formal

AMS 5 · solved (literature)

lemma baumgartner_strong (V : Type*) [AddCommGroup V] [Module ℚ V] (k : ℕ) :
    ∃ X : Set V,
      (∀ Y, Y.IsAPOfLength ⊤ → (X ∩ Y).Nonempty) ∧
      (∀ Y, IsAPOfLength Y k → (X ∩ Y).ncard ≤ 2)

formal-conjectures/198.lean ↗

links

Vela Sidon frontier (A309370) · verified work

A B₂/Sidon problem — the same object family as Vela's verified Sidon records, where nine improved terms were accepted into OEIS A309370 (the campaign's first external adoption).

OEIS A309370 ↗ · verified-combinatorics (witnesses + verify.py) ↗ · the Erdős campaign

status

solved

formal

links

status

Search Vela