{"id":"palomar/PALOMAR-2026-10-22-000020","url":"https://github.com/gdahia/ShelahHalesJewett/tree/8a91fc0e8a9617f8ade16ccb3b56e543990c9f45","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000020-v1.json","repo":"https://github.com/gdahia/ShelahHalesJewett","tags":["math.CO","math.LO","msc:05D10","msc:03D20","ramsey-theory","hales-jewett","combinatorics","lean"],"score":0,"title":"Shelah's bound for the Hales–Jewett numbers","trust":"high","domain":"math.CO","source":"palomar","authors":["Gabriel Dahia"],"reviews":0,"subject":"math.CO","summary":"Lean 4 formalization of Shelah's proof of the Hales–Jewett theorem. For k ≥ 1 letters and r colors, every coloring with r colors of the words of length n over k letters has a monochromatic combinatorial line when n is at least the Ackermann function at level 5 and argument 2k + r.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"Primitive recursive bounds for van der Waerden numbers","identifier":"https://doi.org/10.1090/S0894-0347-1988-0929498-X","relationship":"formalizes"}]}