AI summaryⓘ
The authors formalize a method called the Kannan-Bachem Smith normal form algorithm in a programming language called Lean 4, which works with square integer matrices that can be inverted. Their program not only computes certain matrices and their inverses but also proves important mathematical properties about these matrices and their relationships. They ensure the algorithm finishes by showing each step simplifies the problem, and they record detailed information about the computation at each step. Additionally, the authors provide guarantees on how much work the program does and how large the outputs are by using verified calculations. The work focuses specifically on the arithmetic parts, excluding other operations and the runtime environment.
Smith normal formKannan-Bachem algorithmLean 4integer matricesmatrix inversesrecursive algorithmbinary sizearithmetic verificationpolynomial boundsself-delimiting codecs
Abstract
We formalize in Lean 4 the Kannan-Bachem Smith normal form algorithm for nonsingular square integer matrices. The program returns $S,U,U^{-1},V,V^{-1}$ and proves $UAV=S$, $U^{-1}SV^{-1}=A$, four inverse identities, the Smith divisibility conditions, and equality of $S$ with a canonical reference matrix. Stabilization terminates because each recursive pass strictly decreases the binary size of the active pivot; the outer algorithm recurses on the lower-right block. The computation also emits a flat trace of designated sign-magnitude arithmetic leaves. Branch conditions, quotients, Bezout data, and matrix entries are taken from the recorded primitive runs. Composite phases form their traces by concatenating the charge lists returned by the executed children. Verified self-delimiting codecs define the input and output sizes. Coefficient and work recurrences, closed by a kernel-checked polynomial-envelope calculus, give fixed polynomial bounds for both trace cost and the encoded length of the five output matrices. The theorem concerns these arithmetic primitives; structural operations and compiled Lean runtime are outside the model.