{"id":"palomar/PALOMAR-2026-10-22-000043","url":"https://github.com/jtraverso/bondy-simonovits/tree/a4ca4b28a0d82735316fd73a5a11303231109fc7","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000043-v1.json","repo":"https://github.com/jtraverso/bondy-simonovits","tags":["math.CO","msc:05C35","msc:05C38","extremal-graph-theory","even-cycles","formalization"],"score":0,"title":"The Bondy–Simonovits even cycle theorem","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of the Bondy–Simonovits theorem: for every k ≥ 2 there is a constant C such that every finite simple graph on n vertices with no cycle of length exactly 2k has at most C·n^(1+1/k) edges, i.e. ex(n, C_2k) = O(n^(1+1/k)). The statement is existential in C (the proof gives C = 16k + 4); the sharper constants of later work and the full range of even cycle lengths in Bondy–Simonovits's paper are not stated. Mathlib has walks and cycles but not this theorem.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"Cycles of even length in graphs","identifier":"doi:10.1016/0095-8956(74)90052-5","relationship":"formalizes"}]}