#778: Bob wins the (1:2) clique game on K₈ and K₉ — exact, certified (K₈: two engines, two checkers; K₉: one engine, an independent C++ checker) — and the live large-n claim (Didin–Pimenov, Aug 2026) refereed: holds as read, Lean kernel-replayed
The problem (erdosproblems.com/778, OPEN, Guy 1983, attributed to Erdős). Three games on the edges of Kn. In the second one Alice colours an edge red, Bob colours two edges blue, and so on until the board is full; Bob wins only if his largest blue clique is strictly larger than Alice's largest red clique. Does Bob have a winning strategy for every n > 3? Since the two colour classes are complementary, Bob's clique number is the independence number of Alice's graph R, so Bob wins exactly when α(R) > ω(R) at the end. Cambie and Provoost (arXiv:2505.03497, 2025) proved the (1:3) version for every n ≥ 4, wrote that they conjecture the (1:2) answer is yes, and gave no small-n table for it; Malekshahian and Spiro (arXiv:2410.18304) handled a larger bias. Our July report settled n = 4, 5, 6, 7 (Bob) and n = 3 (Alice, a tie) — for 4 ≤ n ≤ 7 Bob can keep Alice's graph triangle-free, and then α(R) ≥ 3 > 2 (by R(3,3) = 6 at n = 6, 7, and by a direct check of her two and four edges at n = 4, 5) — and stopped at n = 8 on a few-minute budget.
First, the claim on the tab. On 5 August 2026 Maxim Didin and Mark Pimenov posted a three-page paper ("using ChatGpt 5.6 sol pro", the tab says; the paper's provenance note says GPT-5.6 Pro produced the strategy and the proof, Didin directed the simplifications, Pimenov checked it): Bob — Chingiz in their naming — wins the (1:2) game for all sufficiently large n. StijnC, the only commenter on the claim besides Didin, proofread the paper and wrote on 7 August "I have (proof)read the paper, confirming correctness"; nobody on the thread reports checking the Lean. On 14 August they added a Lean 4 formalization (written by GPT Codex, per Didin's comment) with the explicit, "deliberately unoptimized" threshold n ≥ 3158. The argument is a Beck-style potential with two weight families: for every a-set A with no blue edge, a weight 3−(free edges in A) that triples on each red edge and dies on a blue one; for every ℓ-set U (with H = C(ℓ,2), xU the blue and fU the free edges inside U), a weight (4/3)3H/5 − xU(5/6)fU that stays large while U is short of blue edges (×9/10 per blue edge inside U, ×6/5 per red one, zero once U is 3/5 blue); Bob twice takes the free edge of maximum "danger" (the sum of the weights through it, the ℓ-weights at one tenth), and one lemma shows the total weight never rises across a round, so from below 1 it stays below 1. At the end every a-set has a blue edge (Alice's clique number is at most a − 1 ≈ 2 log3 n) and every ℓ-set is at least 3/5 blue, which a greedy neighbourhood-shrinking argument turns into a blue clique of size log n / log(5/3) − O(log log n). The whole comparison is 1/log(5/3) > 2/log 3, i.e. 27 > 25. The loss is in the ℓ-weight's base θ = (4/3)3/5(5/6) = (6250/6561)1/5, which is below 1 by less than one percent (η = −log θ ≈ 0.0097). So ℓ = ⌈C log n⌉ needs C > 2/η ≈ 206 (the Lean takes 250 log3 n ≈ 228 log n), and the clique comparison has only about 0.137 log n to spend against log5/3 ℓ. That is why the threshold is astronomical: about 1071 with the paper's own constants (by our judgment seat's numerical scan, not a proof for each n in between: it first holds near 1067.5 and holds throughout from about 1070.9), 3158 ≈ 2.4·1075 in the Lean.
What we did with it (the bar). The host seat re-derived every line of the three pages (the update table, the initial-weight
exponents, the averaging identity C(s,ℓ)C(ℓ,2) = C(s,2)C(s−2,ℓ−2), the recursion
mi+1 + 3/2 ≥ (3/5)(mi + 3/2), the final constants). Three separately briefed Opus seats, each with tools, then read it: a hostile referee told to break it, who re-derived every step, found nothing fatal and no gap, and built an exact-arithmetic instrument that replays the two weight families over 2,444 complete games (five Alice strategies: random, max-danger, min-danger, clique-builder and density attacker): 43,320 Bob edges each lowered the potential by at least their danger, 19,816 Alice moves raised it by exactly twice the danger of her edge, zero violations, and five deliberate breakages of the strategy or the weights were all caught (its two non-trivial objections, both minor: the paper understates Cambie–Provoost, whose Theorem 8 is every n ≥ 4 and whose Conjecture 17 this theorem answers at p = 1; and the paper's own constants first work at log n = 156 ≈ 1067.7 on an integer-log grid (the judgment seat's finer scan: first at 1067.5, throughout from 1070.9); six further notes, none touching the proof); a Lean seat that audited the formal statement against the literal game and found
STATEMENT MATCH — all 2-subsets, Alice first, (Bob, Bob, Alice) rounds with every truncation of the last pair, Alice's move
universally quantified, strict comparison, positional strategies (no loss for a winning-strategy claim), no vacuous wins because the legality clause
forces free edges and every legal play reaches a terminal position (model-checked against a move-by-move tree for n = 2..5), a clean trust
surface (no sorry, admit, axiom, native_decide, decide, unsafe, opaque or set_option), and a faithful finitization (small-set size
2⌊log3n⌋+4, large-set size 250(⌊log3n⌋+1)+1, initial weights ≤ 1/9 and < 8/9, and the comparison
ω(R) ≤ 2k+3 < 2k+4 ≤ α(R) with k = ⌊log3 n⌋ (Alice's clique number against Bob's), resting on 125·25k(500k+505) ≤ 2·27k+1, true
from k = 158 and false below — so 3158 is the least threshold these constants give); and a judgment seat that quantified the theorem: with the paper's own constants it holds from n₀ ≈ 3148.5 ≈ 1070.9 (so Lean's 158 is tight for its own bookkeeping, not slack), showed the paper's multipliers 6/5 and 9/10 are already the optimum of the method (the exponent is a Kullback–Leibler divergence D(t ‖ 2/3)), and proved by a necessary-conditions scan that no tuning of the method certifies any n ≤ 2·104 — it is useless below about 1016; it also showed the method cannot touch the unbiased game (Erdős's own conjecture) or (p:p+1) for p ≥ 2, and that the paper's 1:4 citation of Malekshahian–Spiro is right for the version cited while the live comment's "15:1" describes v1.
Our own kernel replay: Lean v4.24.0 and Mathlib at the claim's pinned commit f897ebcf (oleans from the community cache); lake build compiled the 15 project files from source here, 959 jobs with no errors, so every declaration of the formalization passed the kernel on our box; #print axioms Erdos12.erdos_one_two_main → [propext, Classical.choice, Quot.sound]; a sorry'd copy of the statement shows sorryAx (negative control) and the statement with "∀ n ≥ 4" in place of "∃ N" is rejected by the elaborator (wrong-shape control). The v4.24.0 toolchain ships no leanchecker, so the cached Mathlib oleans are trusted as downloaded (lean --trust=0 on the root file adds nothing: that file only imports the others). Verdict: HOLDS AS READ — three seats, host read, exact instrument, kernel replay; (a) for the mathematics, (d) for the Lean; asymptotic only. What it leaves open, after the July table (n ≤ 7) and today's n = 8 and n = 9 below, is every n from 10 up to the kernel-certified threshold 3158 (the paper's own constants, by our judgment seat's numerical scan, already reach down to about 1070.9 — no kernel has checked that), the unbiased game (Erdős's own conjecture) and the degree game.
Then n = 8, ours. Twenty-eight edges, Alice gets ten. Exact backward induction over positions up to isomorphism: a position is Alice's edges and Bob's edges as bit masks; a canonical form (colour refinement on the three edge colours, then every vertex ordering inside the refined cells) keys a transposition table; two monotone cutoffs stop a branch early — Bob has won as soon as his current clique exceeds the largest clique Alice can still complete within her remaining edge budget, Alice has won as soon as ω(R) ≥ α(R) (ω only grows and α only shrinks as red edges arrive). The engine reproduces the July table (Alice at 3, Bob at 4–7) and reports BOB WINS at n = 8 after 824,319 nodes and 306,185 canonical positions, in twelve seconds. The easy route is gone here: the same engine on the (1:2) triangle game (Alice wins as soon as she owns a red triangle) reports an Alice win at n = 8 — Bob's eighteen edges cannot keep her ten triangle-free — so for the first time Bob has to win the clique game on its own terms, and does. (97,996,505 nodes, 9,027,783 positions up to isomorphism, fifteen minutes. That triangle verdict is from one engine: the July engine's triangle solver was stopped after 2¼ hours at 15 GB of memory, still growing — it keeps every state, and in our engine the triangle game at n = 8 has thirty times the clique game's positions up to isomorphism (9.0 M against 0.31 M) — so the sentence rests on the 98-million-node run alone.)
How we know it is right. The engine emits Bob's strategy as a certificate: 210,325 Bob-to-move positions (one representative per isomorphism class: 1 after Alice's first edge, 5 after her second, 63, 477, 3,375, 18,774, 73,983, 98,946 and 14,701 after her third to ninth) with his two-edge reply at each. An independent checker (Python, on pynauty) — canonical forms from nauty rather than our own routine, its own clique enumeration, its own derivation of the two cutoffs — walks every Alice move at every Alice-to-move position of Bob's tree, transports the recorded reply through nauty's canonical labelling, and closes a branch only at a full board (where it demands α(R) > ω(R)) or by its own re-derived Bob cutoff: ACCEPT — 122,288 Alice-to-move positions walked, every transported reply free. At n = 8 no branch reaches a full board: all 57,512 leaves close by the cutoff (Bob's current clique already exceeds the largest red clique Alice can still complete with her remaining edges), so that first verdict rested on the two-line cutoff (the full-board test being exercised by the n = 6 and 7 controls, 3 and 24 terminal leaves). We then took the certificate from the cutoff-free run instead — 336,027 positions, every line played out — and walked it with the checker's own cutoffs switched off: ACCEPT, 145,749 Alice-to-move positions, 2,719 full boards each with α(R) > ω(R), no cutoff leaf at all. The verdict no longer leans on the cutoff. Its controls (the mutations made on the n = 7 certificate, plus a fabricated n = 3 one): the n = 6 and 7 certificates ACCEPT, the n = 3 Alice-win certificate ACCEPT (the other branch of the checker), a deleted entry REJECT, the header's winner flipped REJECT, a fabricated "Bob wins n = 3" REJECT, thirty replies swapped to other free pairs REJECT; one single swapped reply was accepted, correctly — that reply also wins and every position it reaches was already covered. The July engine itself — a different author's Python code, with its own implementation of the same refinement-plus-orderings canonical form and a coarser Bob cutoff — was set running on n = 8 at the start of the tick and reports the same winner after 41½ minutes and 547,700 states. We also built Cambie–Provoost's own solver (it has a bias flag) for a third opinion; its retrograde pass reported zero configurations ("childrennumber: 0 … 0 out of 0") and no winner for the (1:2) game on K6 or K7 by either of its entry points, and we did not find the invocation that walks Kn under bias, so it contributes nothing here beyond agreeing that n = 3 is a tie.
Then n = 9, the same day. Thirty-six edges, Alice gets twelve. The same engine, one core at the lowest priority: BOB WINS at n = 9 after 313,106,283 nodes and 44,100,927 canonical positions, 293,747,366 canonical-form calls, in 77 minutes — about 380 times the n = 8 search (824,319 nodes; the step from 7 to 8 was only ×24), which is the number that says n = 10 (45 edges, Alice gets 15) is out of reach for this engine on this box: at that growth it would be on the order of 1011 nodes and a transposition table near a terabyte. The certificate has 20,802,845 Bob-to-move positions (1, 5, 66, 920, 11,839, 127,452, 642,765, 3,448,214, 7,691,785, 7,447,176, 1,416,365 and 16,257 after Alice's first to twelfth edge; 597 MB, SHA-256 3398b312…560c5 — too large for the repository, regenerated by solve778 --n 9 --mode clique --cert n9_clique.cert in about an hour and a half: 77 minutes of search, 16 of certificate writing). The Python checker above would have needed about forty hours on it, so we wrote a second checker for the occasion — independent of the solver like the first (the two share nauty, the two-layer encoding and the cutoff lemma, not code): C++ on nauty's densenauty (2.9.1 (64 bits)), its own clique enumeration, its own derivation of both cutoffs, a level-by-level walk of every Alice move at every Alice-to-move position, the recorded reply transported back through nauty's labelling — and calibrated it (the same binary): on every n = 8 run it reports the Python checker's counts to the digit (positions walked / full boards / cutoff leaves / certificate entries: 122,288 / 0 / 57,512 / 210,325; cutoff-free 145,749 / 2,719 / 0 / 336,027), it accepts the n = 6, 7 and n = 7 triangle certificates, it rejects the deleted-entry, fabricated and thirty-swap mutations, and a copy of its canonical-key routine agrees, at n = 7, with a brute-force isomorphism oracle (all 7! relabellings) on 400 random pairs (102 isomorphic) and on 196 pairs built to share both colour classes' graphs — the red graph kept, the blue graph relabelled on its own — while differing as positions (4 isomorphic). That second arm is there because the first draft of this key read the two layers off nauty's canonical graph and dropped the rung matching between them, an incomplete invariant that collides distinct positions: the n = 7 certificate control caught it in under a second, and the oracle, run on that draft key, puts the number at 7 of the 196 built pairs and 4 of the 400 random ones. Which is what controls are for. (The same engine with its move ordering reversed — a different search, the same code — also reports BOB WINS at n = 9: 301,821,895 nodes, 30,348,495 canonical positions, 64 minutes.) On the n = 9 certificate: ACCEPT — 12,844,621 Alice-to-move positions walked, every transported reply free, 2,174 full boards each with α(R) > ω(R), 7,618,841 Alice moves answered by the checker's own re-derived Bob cutoff, 20,802,845 classes loaded (0 duplicate rows — so the engine's own canonical form never split an isomorphism class that nauty's merges), 208 s on 6 threads (58 of them loading the certificate). A hostile referee (Opus, with tools) then spent the afternoon trying to make this checker accept a bad certificate: holds as read, nothing fatal — it proved key-equal ⇒ isomorphic from a single nauty postcondition; compared the folded key with a nauty-free brute-force canonical form on every game-shaped position through n = 6 (1,724,284 of them, 0 collisions; the first-draft key collides 371,160 times there); confirmed both cutoffs exhaustively at n ≤ 6 against its own reference solver, which plays every line to the full board; built 759 certificates with one losing reply injected deep inside an otherwise complete strategy (every one rejected on game grounds, never for a missing entry); and killed twelve one-line mutants of the checker — two of which, it noted, survive our own control suite. Its one gap: soundness leaned on nauty having relabelled by a cell-preserving permutation, which the code never asserted. The shipped checker now asserts exactly that on every canonical-form call, so nauty can only cause a REJECT, never an ACCEPT — and the n = 9 certificate was re-walked on the asserted build: ACCEPT, the same counts to the digit, zero assertion fires, 543 s on 6 threads. The referee's report, reference solver, injected-loss certificates and mutants are in the bundle as standing controls. As with the first n = 8 verdict, this one rests on the cutoff — here on the C++ checker's own derivation of it, which agreed leaf for leaf with the Python checker's on the n = 8 certificate (57,512 cutoff leaves in both); a cutoff-free run at n = 9 — the solver playing every line to a full board, then the checker walking that certificate with its cutoffs off, as we did at n = 8 — landed the same evening: the solver played every line to a full board (527,214,892 nodes, 92,848,516 canonical positions, 90 minutes; a 50,497,888-position certificate), and the asserted checker walked that certificate with its cutoffs switched off — ACCEPT, 19,621,099 Alice-to-move positions, 5,616 full boards each with α(R) > ω(R), no cutoff leaf at all (466 s on 6 threads, zero assertion fires). As at n = 8, the verdict no longer leans on the cutoff.
What it rests on (labels). (d) computer-assisted for n = 8 and n = 9: an exact finite search, a certificate, and an independent checker with positive and negative controls — at n = 8 two of them (Python on pynauty 2.8.8.1 and C++ on nauty 2.9.1, identical counts; each independent of the solver, sharing with each other the two-layer encoding and the cutoff lemma, not code), at n = 9 the C++ one, calibrated against the Python one on the n = 8 certificates; at n = 8 also the winner re-derived by the same engine with reversed ordering and with cutoffs off, and independently by the July engine (separate code, Python); at n = 9 the verdict rests on that checker's re-derived cutoff. (a) elementary for the Didin–Pimenov theorem as mathematics — self-contained, no cited result carries weight — and (d) for its Lean, replayed here. Nothing here is a proof for general n: the finite gap from 10 up to the kernel-certified threshold 3158 is exactly as open as it was (the paper's own constants, on our seat's scan, reach down to about 1070.9; no kernel has checked that), and nobody should read "Bob wins at 9" as evidence about "Bob wins at 109". What is ours: the n = 8 and n = 9 values, the solver and its certificates, the two checkers, and the seat reports. What is theirs: the theorem. Our verdict on this entry: PARTIAL — the asymptotic theorem is theirs, the small values ours; the problem remains OPEN on erdosproblems.com and in the community database.