The 33-vector, 14-basis Cabello set is a Kochen–Specker set (admits no {0,1} coloring) — refuting the ≥16-basis conjecture (Cabello, PRL 135, 190203, 2025)

Enuntiatio — the claim

The 33-vector, 14-basis Cabello set is a Kochen–Specker set (admits no {0,1} coloring) — refuting the ≥16-basis conjecture (Cabello, PRL 135, 190203, 2025)

Refuted by a {0,1}-assignment f of the 33 rays with f(u)+f(v) ≤ 1 for orthogonal u,v and exactly one 1 per orthonormal basis (a valid KS coloring)

Expressio — the formal statement

set_option maxHeartbeats 0
set_option maxRecDepth 4000000

abbrev Eis := Int × Int
def emul (p q : Eis) : Eis := (p.1 * q.1 - p.2 * q.2, p.1 * q.2 + p.2 * q.1 - p.2 * q.2)
def econj (p : Eis) : Eis := (p.1 - p.2, - p.2)
def eadd (p q : Eis) : Eis := (p.1 + q.1, p.2 + q.2)
def herm (u v : List Eis) : Eis := (List.zipWith (fun a b => emul (econj a) b) u v).foldl eadd (0, 0)
def orth (u v : List Eis) : Bool := herm u v == (0, 0)
def ray (rays : List (List Eis)) (i : Nat) : List Eis := rays.getD i []
def orthI (rays : List (List Eis)) (i j : Nat) : Bool := orth (ray rays i) (ray rays j)
def pickable (rays : List (List Eis)) (ones zeros : List Nat) (v : Nat) : Bool :=
  !(zeros.contains v) && !(ones.any (fun o => orthI rays o v))
def solve (rays : List (List Eis)) (bs : List (Nat × Nat × Nat)) (ones zeros : List Nat) (fuel : Nat) : Bool :=
  match fuel with
  | 0 => false
  | Nat.succ fuel => match bs with
    | [] => true
    | (a, b, c) :: rest =>
      let cnt := (if ones.contains a then 1 else 0) + (if ones.contains b then 1 else 0) + (if ones.contains c then 1 else 0)
      if cnt > 1 then false
      else if cnt == 1 then solve rays rest ones (([a,b,c].filter (fun v => !ones.contains v)) ++ zeros) fuel
      else [a,b,c].any (fun v => pickable rays ones zeros v &&
             solve rays rest (v :: ones) (([a,b,c].filter (fun w => w != v)) ++ zeros) fuel)
def rays : List (List Eis) := [[(0, 0), (0, 0), (1, 0)], [(0, 0), (1, 0), (0, 0)], [(1, 0), (0, 0), (0, 0)], [(1, 0), (0, 1), (-1, -1)], [(1, 0), (1, 0), (1, 0)], [(-1, -1), (0, 1), (1, 0)], [(1, 0), (0, 1), (1, 1)], [(1, 0), (1, 0), (-1, 0)], [(-1, -1), (0, 1), (-1, 0)], [(1, 0), (0, -1), (-1, -1)], [(1, 0), (-1, 0), (1, 0)], [(-1, -1), (0, -1), (1, 0)], [(-1, 0), (0, 1), (-1, -1)], [(-1, 0), (1, 0), (1, 0)], [(1, 1), (0, 1), (1, 0)], [(1, 0), (1, 0), (0, 0)], [(1, 0), (-1, 0), (0, 0)], [(1, 0), (0, 1), (0, 0)], [(1, 0), (0, -1), (0, 0)], [(0, 1), (1, 0), (0, 0)], [(0, 1), (-1, 0), (0, 0)], [(1, 0), (0, 0), (1, 0)], [(1, 0), (0, 0), (-1, 0)], [(1, 0), (0, 0), (0, 1)], [(1, 0), (0, 0), (0, -1)], [(0, 1), (0, 0), (1, 0)], [(0, 1), (0, 0), (-1, 0)], [(0, 0), (1, 0), (1, 0)], [(0, 0), (1, 0), (-1, 0)], [(0, 0), (1, 0), (0, 1)], [(0, 0), (1, 0), (0, -1)], [(0, 0), (0, 1), (1, 0)], [(0, 0), (0, 1), (-1, 0)]]
def bases : List (Nat × Nat × Nat) := [(0, 1, 2), (3, 4, 5), (6, 7, 8), (9, 10, 11), (12, 13, 14), (0, 15, 16), (0, 17, 18), (0, 19, 20), (1, 21, 22), (1, 23, 24), (1, 25, 26), (2, 27, 28), (2, 29, 30), (2, 31, 32)]

theorem cabello_uncolorable : solve rays bases [] [] 30 = false

Figura — drawn from the certified data

Demonstratio — the kernel-checked proof

by decide