{"id":"palomar/PALOMAR-2026-08-26-000001","url":"https://github.com/sneed-and-feed/lean-theorems-1/tree/fc4a68b1a7ec3ab87aa40ab64fbfd168fda862d2","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-26-000001-v1.json","repo":"https://github.com/sneed-and-feed/lean-theorems-1","tags":["math.CO","msc:05C50","msc:05C70","msc:15A03","graph-theory","combinatorics","lean","formal-verification"],"score":0,"title":"sneed-and-feed/lean-theorems-1","trust":"high","domain":"math.CO","source":"palomar","authors":["Sneed & Feed Formalization Team"],"reviews":0,"subject":"math.CO","summary":"A complete, machine-checked Lean 4 formalization of the Graham–Pollak theorem (1971) and its tightness on complete bipartite partitions of complete graphs. Proves that any partition of the edges of the complete graph K_n into m complete bipartite subgraphs requires at least n - 1 bipartite graphs (m >= n - 1), adapting Helge Tverberg's 1982 linear-algebraic quadratic form argument. Also formalizes the canonical star partition proving tightness. To the maintainers' knowledge, Graham–Pollak was not previously formalized in Mathlib (checked against Mathlib v4.34.0-rc1).","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-26","reactions":{},"formalized":true,"formalizes":[{"title":"On embedding graphs in squashed cubes","identifier":"","relationship":"formalizes"},{"title":"On the decomposition of K_n into complete bipartite graphs","identifier":"","relationship":"adapts"}]}