{"id":"palomar/PALOMAR-2026-10-14-000006","url":"https://github.com/AItoBit/erdos-627-palomar/tree/4a98648f631e1be44b8fcd61f3f7bb48e7388e99","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-14-000006-v1.json","repo":"https://github.com/AItoBit/erdos-627-palomar","tags":["math.CO","msc:05C15","graph-theory","chromatic-number","lean"],"score":0,"title":"Triangle-free graphs with prescribed chromatic number","trust":"high","domain":"math.CO","source":"palomar","authors":["alexander"],"reviews":0,"subject":"math.CO","summary":"A Lean formalization of the classical existence of finite triangle-free graphs with arbitrarily large chromatic number. For each integer k at least two, it constructs a finite simple graph whose clique number is exactly two and whose chromatic number is exactly k. The proof iterates the Mycielski construction from the complete graph on two vertices. This is the Tutte–Zykov variant recorded with Erdős problem 627, not a solution of that problem's open asymptotic limit question.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-14","reactions":{},"formalized":true,"formalizes":[{"title":"Sur le coloriage des graphs","identifier":"doi:10.4064/cm-3-2-161-162","relationship":"formalizes"}]}