Graphs of large girth and large chromatic number: Erdős, Mycielski, and the fractional chromatic number of Mycielski graphs
Source: github.com/jtraverso/erdos-girth-chromatic/tree/05407c110b2…
A Lean 4 / Mathlib formalization of three classical results on graphs with large chromatic number. (1) Erdős' 1959 theorem: for every g and k there is a finite graph with girth greater than g and chromatic number greater than k, in the structural form given by the probabilistic argument (for every ε > 0 and all large n, a graph on n vertices with girth greater than g whose independent sets have fewer than εn vertices). (2) Mycielski's 1955 construction M(G): it preserves and reflects triangle-freeness, M(G) is (k+1)-colourable exactly when G is k-colourable, χ(M(G)) = χ(G) + 1 for every…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-17-000009
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-17-000009/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-17-000009/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'