{
  "annotation_id": "53e2fabe-f496-4ee1-8dc8-e82a4473631b",
  "date_created": "2026-02-17T05:53:12.365000Z",
  "date_modified": "2026-02-17T05:53:12.365000Z",
  "file_hash": "59976b46a439d2a6eec600b1137c0fa9d8f0fd876e429a0c9899ddfa6dd68cca",
  "private": false,
  "record": {
    "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\u0027s rule and Euler\u0027s 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 ($\u003e10^{65}$). We verify the smallest sociable cycle of length 5 (Poulet\u0027s 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.",
    "arxiv_id": "2601.07444",
    "authors": [
      "Zhipeng Chen",
      "Haolun Tang",
      "Jingyi Zhan"
    ],
    "categories": [
      "cs.LO"
    ],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "title": "Formalization of Amicable Numbers Theory",
    "url": "https://arxiv.org/abs/2601.07444",
    "version": "v1"
  },
  "schema_id": "dorsal/arxiv",
  "source": {
    "execution_id": "271a0608-1b80-4876-a6df-2a923412f0c1",
    "id": "arXiv Dataset",
    "type": "Model",
    "variant": "snapshot-2026-01-17",
    "version": "0.1.0"
  },
  "user_id": 1000002
}