sneed-and-feed/lean-theorems-1
A complete, machine-checked Lean 4 formalization of Radon's Lemma (Johann Radon, 1921) and Helly's Theorem on intersecting families of convex sets (Eduard Helly, 1923; Freek Wiedijk #99) from first principles. Proves that any d + 2 points in ℝ^d admit a Radon partition into two disjoint subsets whose convex hulls intersect, and uses Radon's lemma by induction on the family size to prove Helly's theorem for finite families of convex sets under the general <= d + 1 subfamily intersection hypothesis (covering small families |ι| <= d + 1 as well as large families). To the maintainers' knowledge,…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-08-29-000007
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-29-000007/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-29-000007/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'