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.

翻译：本文在Lean~4证明助手中提出了亲和数理论的形式化。若两个正整数$m$和$n$满足$m$的真因子之和等于$n$，且$n$的真因子之和等于$m$，则称它们构成一个亲和对。我们的形式化引入了真因子和函数$\propersum(n) = σ(n) - n$，定义了亲和对与亲和数的概念，并通过计算验证了历史上著名的亲和对。此外，我们形式化了基本的结构定理，包括对称性、非平凡性以及与过剩数/亏数之间的联系。一个关键贡献是使用指标平移和\texttt{zify}策略，完成了经典萨比特公式（9世纪）的完整形式化证明。我们还提供了萨比特法则和欧拉广义法则（1747）这两个生成亲和对的基本定理的完整形式化证明。一项重要成果是首次完整形式化了Borho-Hoffmann繁殖方法（1986），该部分包含540行代码和33个定理，并利用自动化代数策略（\texttt{zify}和\texttt{ring}）验证了复杂的多项式恒等式。我们还形式化了扩展内容，包括社交数（相亲数链）、订婚数（拟亲和对）、奇偶性约束定理，以及互质对的计算搜索边界（$>10^{65}$）。我们验证了长度为5的最小社交数循环（普莱循环），并通过计算验证了具体实例。该形式化包含2076行Lean代码，组织为Mathlib候选模块和论文专用模块，包含139个定理以及所有必要的真因子和乘性与互质性推理基础结构。