{"id":"palomar/PALOMAR-2026-08-26-000003","url":"https://github.com/JaTaSn/lattice-line-covers/tree/68f90ff9d90cb71af2c76eb1291a6ddf564cf4fb/lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-26-000003-v2.json","repo":"https://github.com/JaTaSn/lattice-line-covers","tags":["math.CO","math.NT","msc:05B40","msc:11H31","msc:52C15","msc:11B25","msc:11B57","combinatorics","number-theory","lean"],"score":0,"title":"JaTaSn/lattice-line-covers","trust":"high","domain":"math.CO","source":"palomar","authors":["Jan Snellman"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 formalization of Theorem 1 of arXiv:2608.22550: there is a family of lattice lines covering the integer plane whose set of realized directions is dense. Concretely, a family F of subsets of Z^2 is exhibited such that (i) every member is a genuine lattice line, the nonempty solution set of Px + Qy = c with P, Q coprime; (ii) the members cover Z^2; (iii) two members of different direction are disjoint, so no lattice point is covered twice in different directions; and (iv) the directions that occur are dense in the space RP^1 of line directions, that is, every angle in [0, pi) is…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-01","reactions":{},"formalized":true,"formalizes":[{"title":"On the directions occurring in lattice-line coverings of the integer plane","identifier":"arXiv:2608.22550","relationship":"formalizes"}]}