No-three-in-line at n=75
- Slug:
three-in-line - Solver: Codex
gpt-5.6-solMax (2026-08-16 search; 2026-08-23 replay and campaign). Grok watched only. - Status: residue — remains open; audited rct4 SAT returned no 150-set
- Area: Discrete geometry
- Sources: Green 100 #72; Dudeney 1900 / Guy–Kelly 1968; Prellberg, arXiv:2602.07751; Heule 2026 (Flammenkamp database); MathWorld
- Started: 2026-08-16
- Campaign: find and independently replay a 150-point certificate on the grid
In general
Place as many points as possible on the grid so that no three are collinear (any slope, not just axis-aligned). Pigeonhole on rows gives . The no-three-in-line problem asks whether for every , or only for small . Green #72 records both the finite question and the asymptotic one (Guy–Kelly suggested , so would eventually fail; Hall-type constructions still give almost for infinitely many ).
The finite record moved fast in 2026. Prellberg (arXiv:2602.07751) used symmetry-reduced CP-SAT to get for all . Flammenkamp's dated database then recorded Prellberg configurations at and Heule configurations at . On 17 August 2026 Heule found an rct4 configuration at , followed by on 19 August. Thus is now known for every and for ; the first current hole is .
The previous campaign recovered Heule's database code, decoded it to
142 coordinates, and checked it with two exact implementations. The present
campaign is scoped to the first remaining hole, . Odd order cannot use
clean (rot4) orbits—the rotation centre is a lattice point—so the
first search uses Flammenkamp's rct4, with four-orbits off the diagonal
and half-turn pairs on it.
Precise statement
A set is no-three-in-line if no three distinct points of are collinear in : equivalently, for all distinct ,
Finite target. A checked set with would meet the row bound and prove . No such certificate is currently known in the database cut of 19 August 2026. An incomplete or symmetry-restricted SAT run is residue, not evidence that .
A SAT/CP encoding has one Boolean per cell (or per rct4 orbit); for every line that meets the grid in points, at most two of those points are selected. Cardinality is exactly 150 points. In canonical rct4 this means one selected diagonal half-turn pair and 37 selected four-orbits, with the anti-diagonal fixed empty.
What a solution looks like
- Found and replayed. A plain
compute/n75-150.txtstores onex ypair per line. Two independent exact verifiers must check 150 distinct in-grid points, exactly two in every row and column, and no collinear triple. - Not found. The CNF or CP model under
compute/, the symmetry reduction, solver + version, wall-clock / timeout, and whether the result was timeout, unsat (on the restricted symmetry), or inconclusive. Unsat on rct4 is an incomplete search, not a proof that . - Do not claim without a checked point list. Do not claim without a complete (not symmetry-restricted) unsat proof. Do not start an asymptotic campaign from this folder.
Related
- Ben Green, 100 Open Problems, Problem 72
- Guy–Kelly, The no-three-in-line problem, Canad. Math. Bull. 1968
- Prellberg, Constraint Satisfaction Programming for the No-three-in-line Problem, arXiv:2602.07751
- Flammenkamp, no-three-in-line database (Heule 2026 entries)
- MathWorld, No-Three-in-a-Line Problem
- formal-conjectures #1692, Green #72
Campaigns so far
- The 16 August rct4 CP-SAT and SAT runs ended
UNKNOWN; their generated CNF was not preserved in this checkout. - On 23 August the current database certificate decoded and passed both exact verifiers, proving .
- On 23 August the live database notes and both unrestricted and rct4 lookups
were refreshed. They contain no configuration at the 19 August cut;
the search then left an audited rct4 formula and three full-search
UNKNOWNruns. No 150-point certificate was found.
Figures
