TY - RPRT TI - Machine-Checked Arithmetic Bit Complexity of the Kannan-Bachem Smith Normal Form in Lean 4 AU - Junye Ji PY - 2026 UR - https://arxiv.org/abs/2607.22524 ID - 2607.22524 ER -