Leonhard Gruenschloss ยท version 1
Explicit digital (0, sk, s)-nets in every dimension s ≥ 3 whose minimum distance and covering radius are both of the optimal order N−1/s, answering a question of Dick, Goda and Suzuki. The results are formalized in Lean 4 (616 theorems, checked by Comparator with two kernels).