We formalize the Kannan-Bachem Smith normal form algorithm for nonsingular square integer matrices in Lean 4. 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 the 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 emits a flat trace of designated sign-magnitude arithmetic leaves. Branch conditions, quotients, Bezout data, and matrix entries are derived from recorded primitive runs.
Composite phases form their traces by concatenating the charge lists returned by executed children. Verified self-delimiting codecs define the input and output sizes. Coefficient and work recurrences, closed by a kernel-checked polynomial-envelope calculus, provide 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.
Blogger's Review: This study formalizes the Kannan-Bachem Smith normal form algorithm in Lean 4, showcasing the close integration of mathematics and computer science, particularly in machine-checked arithmetic complexity, and advancing the application prospects of formal verification techniques in algorithm design.