Formalization of Amicable Numbers Theory

TL;DR

This paper formalizes the theory of amicable numbers in Lean 4, proving classical theorems, verifying famous pairs, and formalizing advanced concepts like sociable and betrothed numbers with extensive automated proof techniques.

Contribution

It provides the first complete formal proof of Th ext={a}bit's formula, Euler's rule, and the Borho-Hoffmann breeding method in Lean 4, advancing formal number theory verification.

Findings

Formal proof of Th ext={a}bit's formula and rule

Verification of famous amicable pairs and cycles

Complete formalization of breeding method and extensions

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) = \sigma(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\={a}bit formula (9th century), using index-shifting and the \texttt{zify} tactic. Additionally, we provide complete formal proofs of both Th\={a}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.