Formalization of Amicable Numbers Theory
Zhipeng Chen, Haolun Tang, Jingyi Zhan
TL;DR
This work presents a comprehensive formalization of amicable number theory in Lean 4, introducing the proper divisor sum $s(n)$ via $s(n)=\sigma(n)-n$ and defining amicable pairs and numbers. It achieves complete machine-verified proofs of three classical generation methods— Thābit ibn Qurra's formula, Euler's generalized rule, and the Borho–Hoffmann breeding method—while leveraging automation (zify and ring) to handle intricate polynomial identities. The formalization extends to sociable numbers, betrothed numbers, parity constraints, and computational search bounds, and it includes verified instances of historic pairs as well as Poulet's five-cycle, all organized across 2076 lines with 139 theorems. Computational verification complements universal proofs, illustrating how concrete checks and rigorous theory can cohere in a single formal framework. The work significantly advances mechanized number theory by providing a complete, extensible Lean 4 library for divisor-sum multiplicativity, coprimality reasoning, and amicable-genesis procedures.
Abstract
This paper presents a formalization of the theory of amicable numbers in the Lean~4 proof assistant. Two positive integers $m$ and $n$ are called an amicable pair if the sum of proper divisors of $m$ equals $n$ and the sum of proper divisors of $n$ equals $m$. Our formalization introduces the proper divisor sum function $\propersum(n) = σ(n) - n$, defines the concepts of amicable pairs and amicable numbers, and computationally verifies historically famous amicable pairs. Furthermore, we formalize basic structural theorems, including symmetry, non-triviality, and connections to abundant/deficient numbers. A key contribution is the complete formal proof of the classical Thābit formula (9th century), using index-shifting and the \texttt{zify} tactic. Additionally, we provide complete formal proofs of both Thābit's rule and Euler's generalized rule (1747), two fundamental theorems for generating amicable pairs. A major achievement is the first complete formalization of the Borho-Hoffmann breeding method (1986), comprising 540 lines with 33 theorems and leveraging automated algebra tactics (\texttt{zify} and \texttt{ring}) to verify complex polynomial identities. We also formalize extensions including sociable numbers (aliquot cycles), betrothed numbers (quasi-amicable pairs), parity constraint theorems, and computational search bounds for coprime pairs ($>10^{65}$). We verify the smallest sociable cycle of length 5 (Poulet's cycle) and computationally verify specific instances. The formalization comprises 2076 lines of Lean code organized into Mathlib-candidate and paper-specific modules, with 139 theorems and all necessary infrastructure for divisor sum multiplicativity and coprimality reasoning.