{"id":"palomar/PALOMAR-2026-10-20-000012","url":"https://github.com/jtraverso/jin-triangle-free/tree/ae47df0ddb29c58a71afed658f9bf74aef1b6e90","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-20-000012-v1.json","repo":"https://github.com/jtraverso/jin-triangle-free","tags":["math.CO","msc:05C15","msc:05C35","graph-theory","triangle-free-graphs","graph-coloring","lean-formalization"],"score":0,"title":"Jin's theorem on dense triangle-free graphs","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Jin's theorem: a finite triangle-free graph on n vertices with minimum degree greater than 10n/29 is 3-colourable; and of its sharpness: for every m ≥ 1 the blow-up of the Grötzsch graph with weights 3m, 2m, 4m is a triangle-free 10m-regular graph on 29m vertices that is not 3-colourable (Häggkvist). This extends the case r = 2 of the Andrásfai–Erdős–Sós theorem, which is in Mathlib. Mathlib does not have Jin's theorem.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-20","reactions":{},"formalized":true,"formalizes":[{"title":"Triangle-free four-chromatic graphs","identifier":"doi:10.1016/0012-365X(94)00063-O","relationship":"formalizes"},{"title":"Odd cycles of specified length in non-bipartite graphs","identifier":"doi:10.1016/S0304-0208(08)73552-7","relationship":"formalizes"}]}