The three-color Ramsey number of the 10-vertex path

We prove $R(P_{10},P_{10},P_{10})=18$: every three-coloring of the edges of $K_{18}$ contains a monochromatic path on ten vertices, and some three-coloring of $K_{17}$ contains none. Faudree and Schelp suggested a formula for three-color path Ramsey numbers. Gyárfás, Ruszinkó, Sárközy and Szemerédi proved that the three-color Ramsey number of the path on $n$ vertices is $2n-2+(n\bmod2)$ for all sufficiently large $n$. Dybizbański, Dzido and Radziszowski established the eight- and nine-vertex cases, completing the cases through nine vertices recorded by Radziszowski's survey. The lower-bound coloring is the even-case $K_4$ blow-up given by Gyárfás, Ruszinkó, Sárközy and Szemerédi and by Dybizbański, Dzido and Radziszowski. The new upper bound follows from Boolean satisfiability refutations after fixing a monochromatic nine-vertex path and imposing simultaneous symmetry constraints. A separate refutation proves that the cases considered cover every coloring. The reduction and the certificate checks are formalized in Lean. This work has not yet been reviewed by experts. The proofs, the Lean formalization, the search code, the certificate checkers and the text were produced by AI models (from OpenAI and Anthropic), working under the author's direction.

Proved in Lean, with compiled checking; not yet reviewed by experts. Produced by AI models under the author's direction.