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

For a graph H, the three-color Ramsey number R(H,H,H) is the least N such that every coloring of the edges of the complete graph KN with three colors contains a monochromatic copy of H. Faudree and Schelp (J. Combin. Theory Ser. B 19, 1975) conjectured that R(Pn,Pn,Pn) = 2n − 2 + (n mod 2) for the path Pn on n vertices. Gyárfás, Ruszinkó, Sárközy and Szemerédi proved this for all sufficiently large n, and Dybizbański, Dzido and Radziszowski determined R(P8,P8,P8) = 14 and R(P9,P9,P9) = 17, completing the cases n ≤ 9 and leaving n = 10 as the first open case. We prove R(P10,P10,P10) = 18: every 3-coloring of the edges of K18 contains a monochromatic path on 10 vertices. The proof is a SAT computation: symmetry breaking anchored on a monochromatic P9, whose existence is re-derived by the same method for the smaller cases, path constraints generated during the search, and a cube-and-conquer split into 15,956 subproblems, each with an unsatisfiability certificate. The argument is formalized in Lean 4; every certificate is checked by Lean's verified LRAT checker, run by native evaluation. Computer-assisted, with a Lean proof; not yet reviewed by experts. Produced by AI models under the author's direction.