{"id":"palomar/PALOMAR-2026-08-26-000011","url":"https://github.com/sneed-and-feed/lean-theorems-1/tree/f60794e58faf3eb7032a78f7e756538cb6513da5","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-26-000011-v1.json","repo":"https://github.com/sneed-and-feed/lean-theorems-1","tags":["math.CO","msc:05C50","msc:05C75","msc:05E30","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 Friendship Theorem (P. Erdős, A. Rényi, and V. T. Sós, 1966; H. S. Wilf, 1971). Proves that any finite simple graph on at least three vertices (|V| ≥ 3) in which every pair of distinct vertices shares exactly one common neighbor must contain a universal vertex (the 'politician'), structuring the graph as a collection of triangles sharing a central vertex (a windmill graph). To the maintainers' knowledge, the theorem was not found in an exact declaration name, docstring, and type signature search of the pinned Mathlib revision (Mathlib…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-26","reactions":{},"formalized":true,"formalizes":[{"title":"On a problem of graph theory","identifier":"","relationship":"formalizes"},{"title":"The friendship theorem","identifier":"","relationship":"adapts"}]}