{"id":"palomar/PALOMAR-2026-08-31-000020","url":"https://github.com/sneed-and-feed/lean-theorems-1/tree/aafce9c36667271ab1113c71a86d97201756c49f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-31-000020-v1.json","repo":"https://github.com/sneed-and-feed/lean-theorems-1","tags":["math.CO","msc:05C75","msc:05C50","msc:05C07","graph-theory","combinatorics","lean-formalization"],"score":0,"title":"The Friendship Windmill Structure Theorem (Erdős–Rényi–Sós 1966)","trust":"high","domain":"math.CO","source":"palomar","authors":["Noah Cohen"],"reviews":0,"subject":"math.CO","summary":"A complete, machine-checked Lean 4 formalization of the Friendship Windmill Structure Theorem (Erdős, Rényi, and Sós, 1966). Proves that any finite graph in which every pair of distinct vertices shares exactly one common neighbor possesses a universal vertex w, has an odd number of vertices |V| = 2k + 1, induces a 1-regular perfect matching on V \\ {w}, and is isomorphic to the Dutch windmill graph Wd(k, 2) 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 v4.34.0-rc1).","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-31","reactions":{},"formalized":true,"formalizes":[{"title":"On a problem of graph theory","identifier":"","relationship":"formalizes"}]}