The Beck–Fiala integer-making theorem
A Lean 4 / Mathlib formalization of the Beck–Fiala integer-making theorem in its rational unit-cube form: if A is a 0/1 matrix in which every column has at most t ≥ 1 ones and x ∈ [0,1]^N has rational coordinates, then x can be rounded to y ∈ {0,1}^N with |∑ᵢ A j i (y i − x i)| < t for every row j; moreover the rounding can keep every coordinate of x that is already 0 or 1. The proof is the floating-coordinates argument: while some coordinates are strictly between 0 and 1, the rows with more than t floating coordinates are fewer than the floating coordinates, so a nonzero direction keeps…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-15-000009
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-15-000009/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-10-15-000009/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'