ks24

This repository contains reproducible starting artifacts for a 24-ray Kochen--Specker search in the original ray-counting convention.

It does not contain a proof that n=24 is impossible, and it does not contain exact coordinates for a 24-ray KS set. As of 2026-04-28, public primary sources still give the global 3D status as:

• lower bound: at least 24 rays;
• smallest public construction: Conway--Kochen, 31 rays;
• unresolved gap: 24 through 30 rays.

Relevant sources:

• Li, Bright, Ganesh, IJCAI 2024 / arXiv:2306.13319: https://arxiv.org/abs/2306.13319
• Kirchweger, Peitl, Szeider, IJCAI 2023: https://www.ijcai.org/proceedings/2023/0216.pdf
• Li, Bright, Trandafir, Cabello, Ganesh, arXiv:2604.19947: https://arxiv.org/abs/2604.19947

Files

• ks24_cnf_schema.py: streaming DIMACS schema generator.
• ks24_manifest.json: n=24 counts, include flags, and variable ranges.
• ks24_checker.py: dependency-free graph validator, 4-colour checker, 010-colouring checker, and lazy non-010 blocking-clause emitter.
• test_ks24_tools.py: smoke tests for the generator and checker.

Useful Commands

Print core n=24 counts:

python3 ks24_cnf_schema.py --n 24

Generate structural CNF plus safe pruning, without the full non-010 expansion:

python3 ks24_cnf_schema.py \
  --n 24 \
  --include-four-color \
  --include-critical \
  --include-triangle-unique \
  --out structural_pruned.cnf

The generator refuses to write the full all-colourings non-010 expansion for n >= 20 unless --force-full-non010 is passed. For n=24, that expansion is 16,777,216 clauses and 5,402,263,552 literal occurrences.

Validate a candidate graph JSON:

python3 ks24_checker.py \
  --graph-json candidate.json \
  --n 24 \
  --check-four-color \
  --find-010

Run smoke tests:

python3 -m unittest -v