Open Research Index

The Graham–Pollak theorem

Juan Pablo Traverso Gianini

Palomar Registrypalomar/PALOMAR-2026-10-23-000006Oct 23, 2026math.COscore 0

A Lean 4 / Mathlib formalization of the Graham–Pollak theorem: the edge set of the complete graph K_n cannot be partitioned into fewer than n − 1 complete bipartite graphs, together with the matching construction by n − 1 stars. Biclique decompositions are encoded by families of pairs of disjoint vertex sets covering every pair of distinct vertices exactly once. Mathlib does not contain this theorem.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-10-23-000006
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-23-000006/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-23-000006/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'