sneed-and-feed/lean-theorems-1
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-08-26-000011
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-26-000011/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-26-000011/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'