Formalization of Amicable Numbers Theory

Zhipeng Chen, Haolun Tang, Jingyi Zhan

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 pro…