Erdős problem 198
The answer is no; Erdős and Graham report this was proved by Baumgartner, presumably referring to the paper [Ba75], which does not state this exactly, but the following simple construction is implicit in [Ba75].
Sources
FormalConjectures/ErdosProblems/
198.lean
Retained formal statement
The statement for which Baumgartner actually writes a proof.
∀ (V : Type u_1) [inst : AddCommGroup V] [Module ℚ V], ∃ X, (∀ (Y : Set V), Y.IsAPOfLength ⊤ → (X ∩ Y).Nonempty) ∧ ∀ (Y : Set V), Y.IsAPOfLength 3 → (X ∩ Y).ncard ≤ 2SolvedStatement only, no proof