This is the second installment of an exposition of an ACL2 formalization of finite group theory. The first, which was presented at the 2022 ACL2 workshop, covered groups and subgroups, cosets, normal subgroups, and quotient groups, culminating in a proof of Cauchy's Theorem: If the order of a group G is divisible by a prime p, then G has an element of order p. This sequel addresses homomorphisms, direct products, and the Fundamental Theorem of Finite Abelian Groups: Every finite abelian group is isomorphic to the direct product of a list of cyclic p-groups, the orders of which are unique up to permutation. This theorem is a suitable application of ACL2 because of its extensive reliance on recursion and induction as well as the constructive nature of the factorization. The proof of uniqueness is especially challenging, requiring the formalization of vague intuition that is commonly taken as self-evident.

翻译：本文是ACL2形式化有限群理论系列论文的第二篇。第一篇在2022年ACL2研讨会上发表，涵盖了群与子群、陪集、正规子群和商群，并以柯西定理的证明收尾：若群G的阶能被素数p整除，则G包含一个阶为p的元素。本续篇将讨论同态、直积以及有限阿贝尔群基本定理：每个有限阿贝尔群同构于一系列循环p-群的直积，且这些群的阶在置换意义下唯一。由于该定理高度依赖递归与归纳，且其分解过程具有构造性特征，因此是ACL2的理想应用场景。其中唯一性证明尤为困难，需要对通常被视为不言自明的模糊直觉进行形式化处理。