{"id":"palomar/PALOMAR-2026-10-22-000009","url":"https://github.com/miinadietrich/crown_graphs_maximise/tree/368a515d22ec74a9f4c2b9b9798f27b49df377e2/lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000009-v1.json","repo":"https://github.com/miinadietrich/crown_graphs_maximise","tags":["math.CO","graph-theory","bipartite-graphs","extremal-combinatorics","lean"],"score":0,"title":"A formal proof that crown graphs maximise the representation number of bipartite graphs","trust":"high","domain":"math.CO","source":"palomar","authors":["Matthew J. Colbrook","Catherine Drysdale"],"reviews":0,"subject":"math.CO","summary":"Lean proofs of the sharp bipartite representation bound, crown extremality, and the supporting finite and structural results.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"Crown graphs maximise the representation number of bipartite graphs","identifier":"","relationship":"formalizes"},{"title":"Crown graph computational certificates","identifier":"validation/SOURCES.json","relationship":"formalizes"},{"title":"On the representation number of a crown graph","identifier":"doi:10.1016/j.dam.2018.03.013","relationship":"formalizes"},{"title":"Solving computational problems in the theory of word-representable graphs","identifier":"https://cs.uwaterloo.ca/journals/JIS/VOL22/Kitaev/kitaev11.html","relationship":"formalizes"},{"title":"On the conjecture of the representation number of bipartite graphs","identifier":"arXiv:2506.01057v1","relationship":"adapts"}]}