The Bondy–Simonovits even cycle theorem
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.
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-22-000043
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000043/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000043/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'