{"id":"palomar/PALOMAR-2026-10-15-000009","url":"https://github.com/jtraverso/beck-fiala/tree/52f1a12a140b0589ac39619dfd07807d98fdbaf5","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-15-000009-v1.json","repo":"https://github.com/jtraverso/beck-fiala","tags":["math.CO","msc:05D40","msc:11K38","discrepancy-theory","integer-rounding","formal-verification"],"score":0,"title":"The Beck–Fiala integer-making theorem","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-15","reactions":{},"formalized":true,"formalizes":[{"title":"“Integer-making” theorems","identifier":"doi:10.1016/0166-218X(81)90022-6","relationship":"formalizes"}]}