sneed-and-feed/lean-theorems-1
A complete, machine-checked Lean 4 formalization of Bárány's Colorful Carathéodory Theorem (1982), Bárány's First Selection Lemma (1982), the 1D Centerpoint Theorem, and geometric deductions from first principles. Proves that for any d + 1 sets of points S_0, ..., S_d in R^d whose convex hulls all contain a common target point p, there exists a colorful transversal f (selecting f(i) in S_i for each color class i) whose convex hull conv({f(0), ..., f(d)}) contains p. Formulated over arbitrary dimension d, with specializations to the origin and low dimensions (d = 0, 1, 2), a formal deduction…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-08-29-000012
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-29-000012/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-000012/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'