The Friendship Windmill Structure Theorem (Erdős–Rényi–Sós 1966)
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).
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-08-31-000020
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-31-000020/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-08-31-000020/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'