Perfect Numbers in ACL2
Logic in Computer Science
2015-09-22 v1 Number Theory
Abstract
A perfect number is a positive integer n such that n equals the sum of all positive integer divisors of n that are less than n. That is, although n is a divisor of n, n is excluded from this sum. Thus 6 = 1 + 2 + 3 is perfect, but 12 < 1 + 2 + 3 + 4 + 6 is not perfect. An ACL2 theory of perfect numbers is developed and used to prove, in ACL2(r), this bit of mathematical folklore: Even if there are infinitely many perfect numbers the series of the reciprocals of all perfect numbers converges.
Cite
@article{arxiv.1509.06081,
title = {Perfect Numbers in ACL2},
author = {John Cowles and Ruben Gamboa},
journal= {arXiv preprint arXiv:1509.06081},
year = {2015}
}
Comments
In Proceedings ACL2 2015, arXiv:1509.05526