#188: the 2026 upper bound k ≤ 6330 refereed (holds; the same proof gives 4917), both known lower bounds turned into exact 15- and 69-point certificates, and an ℓ₆ search that neither certifies nor refutes
The problem (erdosproblems.com/188): colour the plane red and blue with no two red points at distance 1; what is the least k such that some such colouring has no k blue points in arithmetic progression with common difference of length 1 — in the notation of Erdős, Graham, Montgomery, Rothschild, Spencer and Straus, the least k with E² ↛ (ℓ₂, ℓk)? The page says 6 ≤ k ≤ 10⁷ (Erdős–Graham's "more or less", never proved). The forum knows more than the page: Conlon–Fox's 2019 theorem gives a rigorous k ≤ 3.16·10⁹ as stated (log₂ in their hypothesis; the forum's 2.15·10⁹ reads the log as natural), and Currier, Mody, Xie and Zhang (arXiv:2606.17194, June/August 2026) prove k ≤ 6330 (comment of 17 Sep 2026). No proof claim is on the tab; the database says open; nobody has moved the lower bound since Tsaturian's k ≥ 6 in 2017. This entry refereed the 6330, turned both known lower bounds into exact finite certificates, and ran the obvious attack on k ≥ 7 far enough to say exactly what it did not decide.
The 6330 holds as read. The construction is a random colouring of a hexagonal tiling: Voronoi cells of the lattice spanned by (3/2, 0) and (3/4, √3/4), scaled to diameter 1−ε (text extraction loses the √ — the basis is unusual but the lattice is hexagonal with spacing √3/2, we checked); each cell is picked with probability p = 1/19 and kept red only if none of the 18 cells within distance 1 of it was picked, so no two red points are at distance 1. A blue ℓm is then ruled out by a union bound: at most 2⁴·5¹⁶·m⁸ "admissible" cell-sequences can carry a unit progression (Milnor–Thom on the 100m² sign conditions that 100m wall lines impose on the four coordinates of two points), and each is all-blue with probability at most exp(−0.01557m) (Janson's inequality; dependencies only at index distance below 5). We recomputed every constant independently — |z(D)| = 18 by a polygon-distance census, wall-line spacing 0.4330 ≥ 1/3 and 69.3m ≤ 100m lines, the exponent −0.0155711… to ten digits, the count 1250⁴ = 2⁴5¹⁶, the dependency graph against their Lemma 2.7 — and the crossover: with the exponent rounded to 0.01557 as printed, the expected number of all-blue admissible collections drops below 1 exactly at m = 6330; unrounded, at 6329. Verdict: HOLDS AS READ. One remark falls out of the same proof: a unit progression has three degrees of freedom, not four. Parametrised by (x, y, tan(θ/2)) each wall condition is a polynomial of degree 3 in 3 variables (θ = π is missed, but those progressions are θ = 0 progressions read backwards, with the same cells), the same Theorem 2.5 gives (5000m²)³ collections instead of (1250m²)⁴, and the identical calculation ends at k ≤ 4917. Bookkeeping, not an idea — the proof's real slack is the exponent 0.0156 per point, which is what a 2%-density random red set gives.
Both lower bounds as finite certificates. E² → (ℓ₂, ℓk) holds iff some finite point set has no colouring with red independent in its unit-distance graph and blue missing every unit-spaced collinear k-run — a CNF with one clause per unit pair and one per run; restricting any plane colouring to the set satisfies every clause. Two facts are free. A valid colouring has a red point (else any ℓk is blue); translate it there, so the origin is red. And for any d > 1/2, the rotation about the origin by the angle with 2d·sin(θ/2) = 1 moves every point at distance d by exactly 1, so a point P at distance d and its image are not both red — composing with the inverse rotation if necessary, P is blue; this spends the one rotation freedom and is exactly the last step of Tsaturian's proof, with d = 5. Points are the unit triangular lattice and its images under these rotations about lattice points; only the Moser-spindle angle θ√3 (cos θ = 5/6, the angle Tsaturian's Lemmas 2.2 and 2.3 also rotate by) ends up being used. Cadical closes both known theorems:
- E² → (ℓ₂, ℓ₄) [EGMRSS 1975, Thm 1′]: origin red + one θ√3 copy; minimal core 15 points (8 lattice, 7 rotated), 11 unit pairs, 4 progressions. It is a different argument from theirs: the red origin makes the eight unit-circle points of both copies blue; the lattice point at distance √3 lies on two ℓ₄'s whose far ends, at distance √7, form a unit pair, so it is red; its rotated image is red for the same reason; the two are at distance 1.
- E² → (ℓ₂, ℓ₅) [Tsaturian 2017]: origin red, (5,0) blue, rotations by ±θ√3 (and ±θ₃, never used) about every lattice point within radius 6, rotated patches of radius 4: 30,625 points, 208,056 unit pairs, 94,077 progressions — UNSAT in 0.4 s; minimal core 69 points (30 lattice + 39 rotated about seven lattice points), 63 unit pairs, 16 progressions, all within distance 6.02 of the red point. A first encoding with full rotated patches about centres within radius 3 (76,861 points, UNSAT in 1.3 s) gave a 111-point core inside radius 5.21. Without the "(5,0) blue" assumption, the instance with θ₅ copies added is UNSAT too.
Every core point is rebuilt exactly (sympy, coordinates in ℚ(√3, √11)) from its lattice coordinates and rotation word; every pair is checked to have squared distance exactly 1 and every run to be exactly collinear, unit-spaced, of length k; the checked clauses are asserted to be exactly the propositional core; the core is re-solved by minisat22 and is minimal (every single-clause deletion is SAT: 16/16, 126/126, 81/81); rebuilding the rotated points with a wrong angle breaks 1/11, 29/95 and 19/63 of the pair clauses, as a negative control should. The full instances are closed by minisat22 and glucose4 as well, and cadical's DRAT proofs pass drat-trim. A hostile referee seat re-derived all three cores with its own Fraction-arithmetic checker. Controls: the bare lattice is SAT for every k ≥ 3 (one class of its proper 3-colouring); rotations about the origin alone are SAT for k = 5, 6; the no-red-T₃ branch of Tsaturian's proof closes on the bare lattice at radius 8 once (5,0) is assumed blue — his Lemma 2.6 says that branch's lattice colouring is unique, and in it points at distance 5 share a colour; at centre radius 4 the ℓ₅ instance is UNSAT with (5,0) blue and SAT with (6,0) blue or no assumption. Label (a)+(d): elementary reductions, computer-checked finite configurations. Nothing in this paragraph is new mathematics; its value is that the two theorems now have finite certificates of 15 and 69 points that anyone with the bundle can re-check from scratch (the scripts regenerate the instances byte-identically; a hostile referee seat already did, with its own checker).
The obvious attack on k ≥ 7, and what it did not decide. The same apparatus with 6-runs, each instance beside its ℓ₅ twin. The ℓ₆ instances are at least 2,500 times harder for the solver (the one easy SAT took 981 s against 0.39 s for its twin). Every ℓ₆ instance that resolved is SAT at a size where the ℓ₅ twin is SAT too — so it says nothing about ℓ₆ specifically. The three informative instances, whose ℓ₅ twins are UNSAT in 0.3–8 s (rotations about centres within radius 3 with θ₅ copies and no WLOG point; within radius 4 with (5,0) blue; within radius 6 with (5,0) blue, the 69-point configuration), were unresolved at 1200–1800 s. They have now run with longer caps (all at nice 19, one core each): the radius-3 configuration with θ₅ copies and (6,0) blue is SAT after 5,439 s — a 9,373-point patch with no red unit pair and no all-blue 6-run, rechecked from the coordinates alone by a second checker (56,364 unit pairs and 11,304 six-runs rebuilt by geometry, 0 violations; the same model fed to the k = 5 checker shows 1,542 all-blue 5-runs, so the checker can fail) — so that configuration cannot certify k ≥ 7; the radius-4 configuration with (5,0) blue is unresolved at 10,800 s (cap); the radius-6 configurations with (6,0) and with (5,0) blue (the 69-point core's) were both unresolved at their 3,600 s caps, as was a radius-8 (6,0) instance of 57,469 points. So: no certificate of k ≥ 7 found among these configurations within these limits, and no refutation of an ℓ₆ analogue of Tsaturian's lattice rigidity either — a satisfying patch is a colouring of a finite set, not of the lattice. The ℓ₆-free patches that were found have red density 0.22–0.25 on the lattice, longest blue runs of 5 in every direction, 31 to 78 distinct red √3-triangles and no period up to 12: a description of three patches, not a structural statement.
Where the problem stands. 6 ≤ k ≤ 6330 in print, ≤ 4917 by the remark above. On the upper side the loss is structural: with red cells at density 2% every point of a progression is red with probability 0.02; the ceiling for red cells in this tiling is 1/7, and a structured red set of density 0.15–0.2 whose every unit progression hits it within a few hundred steps would put k in the low hundreds. A red set with one piece per period of a lattice Λ fails outright — in the direction of the shortest period vector λ there are entirely blue lines whenever det Λ/|λ| exceeds the width of a piece — so the construction needs many pieces per period, placed so that no direction and no phase is left open, and proving that is a three-parameter covering statement that a periodic red set makes finite. That is the next real move and it is not a cron-tick job. The page's 10⁷ should read 6330. Artefacts: verification/188/lower-bound-certificates-and-cmxz-audit.