### Abstract

This is a formalisation of Amicable Numbers, involving some relevant material including Euler's sigma function, some relevant definitions, results and examples as well as rules such as Thābit ibn Qurra's Rule, Euler's Rule, te Riele's Rule and Borho's Rule with breeders.

### License

BSD License

### Topics

- Mathematics/Number theory

### Session Amicable_Numbers

- Amicable_Numbers

### Depends on

- Polynomial Factorization
- Pratt’s Primality Certificates

## Cite

×

Amicable_Numbers-AFP

    @article{Amicable_Numbers-AFP,
      author  = {Angeliki Koutsoukou-Argyraki},
      title   = {Amicable Numbers},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Amicable_Numbers.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Aug 15, 2020 : Isabelle2020