The seventh ternary density Hales–Jewett number

Let $c_{n,3}$ be the largest size of a subset of $\{0,1,2\}^n$ containing no combinatorial line, a triple obtained by varying a nonempty set of coordinates through the same letter while fixing the rest. We give a computer-assisted proof that $c_{7,3}=1302$, confirming Polymath1's tentative conjecture and closing its bounds $1302\leq c_{7,3}\leq1348$, recorded by Tao in 2009 and O'Bryant in 2015. The witness realizes Polymath1's known lower bound. Three auxiliary SAT bounds, slicing and global alphabet symmetry give sixteen main slice obligations. Refutations of all nineteen formulas were accepted by FRAT-rs, and in a separate earlier production campaign by drat-trim's lrat-check. Formal verification applies to certificate checking: cake_lpr, verified in HOL4 and compiled with CakeML, accepted refutations of all nineteen formulas across two regeneration campaigns. The SAT encodings, cap induction, symmetry reduction, case cover and counting interpretation are justified by the written proof and separate executable checks; they are outside that formal verification.

Computer-assisted; not yet reviewed by experts. Produced by AI models under the author's direction.