		Search-engine friendly clone of the ACL2 documentation.

Math

100-theorems

ACL2 versions of (some of) the Top 100 Theorems List

This page collects those theorems from the Formalizing 100 Theorems page that have been proved in ACL2.

Note that ACL2 has largely focused on proving theorems that are rather different from these (e.g., the correctness of large and complex hardware designs).

1. The Irrationality of the Square Root of 2

Theorem: irrational-sqrt-2

(defthm irrational-sqrt-2
  (implies (equal (* x x) 2)
           (and (real/rationalp x)
                (not (rationalp x)))))

By Ruben Gamboa, in books/nonstd/nsa/sqrt-2.lisp.

2. Fundamental Theorem of Algebra

Theorems fundamental-theorem-of-algebra and fundamental-theorem-of-algebra-sk.

By Ruben Gamboa and John Cowles, in books/workshops/2018/gamboa-cowles/complex-polynomials.lisp.

Note: These theorems require ACL2(r).

3. The Denumerability of the Rational Numbers

Theorem: q2z-bi-z2q

(defthm dm::q2z-bi-z2q
  (implies (integerp n)
           (and (rationalp (dm::z2q-bi n))
                (equal (dm::q2z-bi (dm::z2q-bi n)) n))))

Theorem: z2q-q2z-bi

(defthm dm::z2q-q2z-bi
  (implies (rationalp x)
           (and (integerp (dm::q2z-bi x))
                (equal (dm::z2q-bi (dm::q2z-bi x)) x))))

By David Russinoff, in books/projects/numbers/z2q.lisp.

6. Godel's Incompleteness Theorem

By Natarajan Shankar, using Nqthm, a predecessor to ACL2.

See this file. See also this book.

7. Law of Quadratic Reciprocity

Theorem: quadratic-reciprocity

(defthm dm::quadratic-reciprocity
  (implies (and (dm::primep p)
                (not (= p 2))
                (dm::primep q)
                (not (= q 2))
                (not (= p q)))
           (iff (equal (dm::residue q p)
                       (dm::residue p q))
                (evenp (* (/ (1- p) 2) (/ (1- q) 2))))))

By David Russinoff, in books/projects/numbers/eisenstein.lisp.

9. The Area of a Circle

Theorem circle-area.

By Jagadish Bapanapally, in books/nonstd/circles/area-of-a-circle/area-of-a-circle-2.lisp.

Note: This theorem requires ACL2(r).

10. Euler's Generalization of Fermat's Little Theorem

Theorem: euler-totient

(defthm dm::euler-totient
  (implies (and (posp n)
                (> n 1)
                (posp x)
                (< x n)
                (equal (dm::gcd x n) 1))
           (equal (mod (expt x (dm::totient n)) n)
                  1)))

By David Russinoff, in books/projects/groups/abelian.lisp.

11. The Infinitude of Primes

Theorem: infinitude-of-primes

(defthm dm::infinitude-of-primes
  (implies (integerp n)
           (and (dm::primep (dm::greater-prime n))
                (> (dm::greater-prime n) n)))
  :rule-classes nil)

By David Russinoff, in books/projects/numbers/euclid.lisp.

15. Fundamental Theorem of Integral Calculus

Theorem fundamental-theorem-of-calculus.

By Matt Kaufmann, in books/nonstd/workshops/1999/calculus/book/fundamental-theorem-of-calculus.lisp.

Note: This theorem requires ACL2(r).

17. De Moivre's Theorem

Theorem de-moivre-1.

By Ruben Gamboa, in books/workshops/2018/gamboa-cowles/de-moivre.lisp.

Note: This theorem requires ACL2(r).

19. Four Squares Theorem

Theorem: nat-sum-of-4-squares

(defthm dm::nat-sum-of-4-squares
  (implies (natp n)
           (and (dm::int4p (dm::int4-nat n))
                (equal (dm::sum-squares (dm::int4-nat n))
                       n))))

By David Russinoff, in books/projects/numbers/sum4squares.lisp.

20. All Primes (1 mod 4) Equal the Sum of Two Squares

Theorem: prime-sum-squares

(defthm dm::prime-sum-squares
  (implies (and (dm::primep p)
                (natp a)
                (natp b)
                (equal (+ (* a a) (* b b)) p))
           (or (equal p 2) (equal (mod p 4) 1)))
  :rule-classes nil)

Theorem: prime-sum-squares-converse

(defthm dm::prime-sum-squares-converse
  (implies (and (dm::primep p) (equal (mod p 4) 1))
           (let* ((pair (dm::square-pair p))
                  (a (car pair))
                  (b (cdr pair)))
             (and (natp a)
                  (natp b)
                  (equal (+ (* a a) (* b b)) p)))))

By David Russinoff, in books/projects/numbers/girard.lisp.

22. The Non-Denumerability of the Continuum

Theorem reals-are-not-countable.

By Ruben Gamboa and John Cowles, in books/nonstd/transcendentals/reals-are-uncountable-1.lisp.

Note: This theorem requires ACL2(r).

23. Formula for Pythagorean Triples

Theorem: pyth-trip-sufficiency

(defthm dm::pyth-trip-sufficiency
  (implies (and (posp m) (posp n) (> m n))
           (let ((a (- (* m m) (* n n)))
                 (b (* 2 m n))
                 (c (+ (* m m) (* n n))))
             (equal (+ (* a a) (* b b)) (* c c)))))

Theorem: pyth-trip-necessity

(defthm dm::pyth-trip-necessity
  (implies (and (posp a)
                (posp b)
                (posp c)
                (= (dm::gcd a b) 1)
                (= (+ (* a a) (* b b)) (* c c)))
           (if (oddp a)
               (mv-let (m n)
                       (dm::pyth-trip-generators a b c)
                 (and (posp m)
                      (posp n)
                      (equal a (- (* m m) (* n n)))
                      (equal b (* 2 m n))
                      (equal c (+ (* m m) (* n n)))))
             (mv-let (m n)
                     (dm::pyth-trip-generators b a c)
               (and (posp m)
                    (posp n)
                    (equal b (- (* m m) (* n n)))
                    (equal a (* 2 m n))
                    (equal c (+ (* m m) (* n n)))))))
  :rule-classes nil)

By David Russinoff, in books/projects/numbers/triples.lisp.

25. Schroeder-Bernstein Theorem

Theorem: injectivity-of-sb

(defthm sbt::injectivity-of-sb
  (implies (and (sbt::p sbt::x)
                (sbt::p sbt::y)
                (equal (sbt::sb sbt::x)
                       (sbt::sb sbt::y)))
           (equal sbt::x sbt::y))
  :rule-classes nil)

Theorem: surjectivity-of-sb

(defthm sbt::surjectivity-of-sb
  (implies (sbt::q sbt::x)
           (sbt::exists-sb-inverse sbt::x)))

By Grant Jurgensen, in books/projects/schroeder-bernstein/schroeder-bernstein.lisp.

Theorem: schroeder-bernstein

(defthm zf::schroeder-bernstein
  (implies (and (zf::injective-funp zf::f)
                (zf::injective-funp zf::g)
                (equal zf::s1 (zf::domain zf::f))
                (equal zf::s2 (zf::domain zf::g))
                (zf::subset (zf::image zf::f) zf::s2)
                (zf::subset (zf::image zf::g) zf::s1)
                (zf::force? (zf::sbt-prop))
                (zf::force? (zf::fun-bij$prop)))
           (zf::exists-bijection zf::s1 zf::s2)))

An alternate formulation in pure set theory by Matt Kaufmann, derived from Grant Jurgensen's proof and statement, in books/projects/set-theory/schroeder-bernstein.lisp.

30. The Ballot Problem

Theorem: ballot-theorem

(defthm dm::ballot-theorem
  (let ((a (dm::a-count p e))
        (b (dm::b-count p e)))
    (implies (and (dm::dlistp p) (> a b))
             (equal (dm::prob p e)
                    (/ (- a b) (+ a b))))))

By David Russinoff, in books/projects/numbers/ballot.lisp.

31. Ramsey's Theorem

By Matt Kaufmann, using PC-Nqthm, a predecessor to ACL2.

Note: Only the exponent-2 Ramsey Theorem for two partitions.

34. Divergence of the Harmonic Series

Theorem: harmonic-series-diverges

(defthm harmonic-series-diverges
  (implies (and (natp m)
                (natp n)
                (>= n (expt 2 (* m 2))))
           (> (harmonic-sum n) m)))

By David Russinoff, in books/projects/numbers/harmonic.lisp.

35. Taylor's Theorem

By Ruben Gamboa and Brittany Middleton.

38. Arithmetic Mean/Geometric Mean

By Matt Kaufmann, using Nqthm, a predecessor to ACL2.

See: this paper.

42. Sum of the Reciprocals of the Triangular Numbers

Theorem: tri-recip-sum-limit

(defthm tri-recip-sum-limit
  (implies (and (rationalp e)
                (> e 0)
                (posp n)
                (> n (/ 2 e)))
           (< (abs (- (tri-recip-sum n) 2)) e)))

By David Russinoff, in books/projects/numbers/triangular.lisp.

44. The Binomial Theorem

Theorem: binomial-theorem

(defthm binomial-theorem
  (implies (and (integerp n) (<= 0 n))
           (equal (expt (+ x y) n)
                  (sumlist (binomial-expansion x y 0 n)))))

By Ruben Gamboa, in books/arithmetic/binomial.lisp.

45. The Partition Theorem

Theorem: dlistp-odd-parts

(defthm dm::dlistp-odd-parts
  (implies (posp n)
           (dm::dlistp (dm::odd-parts n))))

Theorem: odd-partp-odd-parts

(defthm dm::odd-partp-odd-parts
  (implies (and (posp n)
                (member-equal l (dm::odd-parts n)))
           (dm::odd-partp l n)))

Theorem: odd-parts-perm-equal

(defthm dm::odd-parts-perm-equal
  (implies (and (posp n)
                (member-equal l (dm::odd-parts n))
                (member-equal m (dm::odd-parts n))
                (dm::permutationp l m))
           (equal l m))
  :rule-classes nil)

Theorem: perm-odd-parts

(defthm dm::perm-odd-parts
  (implies (and (posp n) (dm::odd-partp l n))
           (and (member-equal (dm::sort l)
                              (dm::odd-parts n))
                (dm::permutationp (dm::sort l) l))))

Theorem: dlistp-dis-parts

(defthm dm::dlistp-dis-parts
  (implies (posp n)
           (dm::dlistp (dm::dis-parts n))))

Theorem: dis-partp-dis-parts

(defthm dm::dis-partp-dis-parts
  (implies (and (posp n)
                (member-equal l (dm::dis-parts n)))
           (dm::dis-partp l n)))

Theorem: dis-parts-perm-equal

(defthm dm::dis-parts-perm-equal
  (implies (and (posp n)
                (member-equal l (dm::dis-parts n))
                (member-equal m (dm::dis-parts n))
                (dm::permutationp l m))
           (equal l m))
  :rule-classes nil)

Theorem: dis-partp-dis-parts

(defthm dm::dis-partp-dis-parts
  (implies (and (posp n)
                (member-equal l (dm::dis-parts n)))
           (dm::dis-partp l n)))

Theorem: perm-dis-parts

(defthm dm::perm-dis-parts
  (implies (and (posp n) (dm::dis-partp l n))
           (and (member-equal (dm::dsort l)
                              (dm::dis-parts n))
                (dm::permutationp (dm::dsort l) l))))

Theorem: len-dis-parts

(defthm dm::len-dis-parts
  (equal (len (dm::dis-parts n))
         (len (dm::odd-parts n))))

By David Russinoff, in books/projects/numbers/partitions.lisp.

51. Wilson's Theorem

Theorem: wilson

(defthm dm::wilson
  (implies (dm::primep p)
           (equal (mod (dm::fact (1- p)) p)
                  (1- p)))
  :rule-classes nil)

By David Russinoff, in books/projects/numbers/euler.lisp.

52. The Number of Subsets of a Set

Theorem: len-subsets

(defthm dm::len-subsets
  (equal (len (dm::subsets l))
         (expt 2 (len l))))

By David Russinoff, in books/projects/numbers/subsets.lisp.

54. Konigsberg Bridges Problem

Theorem: konigsberg

(defthm dm::konigsberg
  (implies (and (member-equal dm::r (dm::regions))
                (dm::pathp p dm::r))
           (not (dm::permutationp p (dm::bridges)))))

By David Russinoff, in books/projects/numbers/konigsberg.lisp.

58. Formula for the Number of Combinations

Theorem: len-subsets-of-order

(defthm dm::len-subsets-of-order
  (implies (and (dm::dlistp l) (natp k))
           (equal (len (dm::subsets-of-order k l))
                  (dm::choose (len l) k))))

By David Russinoff, in books/projects/numbers/subsets.lisp.

63. Cantor's Theorem

Theorem: cantor

(defthm zf::cantor
  (implies (and (zf::funp zf::f)
                (zf::force? (zf::zfc))
                (zf::force? (zf::prod2$prop))
                (zf::force? (zf::domain$prop))
                (zf::force? (zf::inverse$prop))
                (zf::force? (zf::b$prop)))
           (not (equal (zf::image zf::f)
                       (zf::powerset (zf::domain zf::f))))))

By Matt Kaufmann, in books/projects/set-theory/cantor.lisp.

66. Sum of a Geometric Series

Theorem sumlist-geometric.

By Ruben Gamboa, in books/nonstd/nsa/exp.lisp.

Note: This theorem requires ACL2(r).

69. Greatest Common Divisor Algorithm

Theorem: gcd-divides

(defthm dm::gcd-divides
  (implies (and (integerp x) (integerp y))
           (and (or (= x 0)
                    (dm::divides (dm::gcd x y) x))
                (or (= y 0)
                    (dm::divides (dm::gcd x y) y))))
  :rule-classes nil)

Theorem: divides-gcd

(defthm dm::divides-gcd
  (implies (and (integerp x)
                (integerp y)
                (integerp d)
                (not (= d 0))
                (dm::divides d x)
                (dm::divides d y))
           (dm::divides d (dm::gcd x y))))

By David Russinoff, in books/projects/numbers/euclid.lisp.

70. The Perfect Number Theorem

Theorem: perfectp-sufficiency

(defthm dm::perfectp-sufficiency
  (implies (and (posp k)
                (dm::primep (1- (expt 2 (1+ k)))))
           (dm::perfectp (* (expt 2 k) (1- (expt 2 (1+ k)))))))

Theorem: perfectp-necessity

(defthm dm::perfectp-necessity
  (implies (and (posp n)
                (evenp n)
                (dm::perfectp n))
           (let ((k (dm::log n 2)))
             (and (dm::primep (1- (expt 2 (1+ k))))
                  (equal (* (expt 2 k) (1- (expt 2 (1+ k))))
                         n)))))

By David Russinoff, in books/projects/numbers/divisors.lisp.

71. Order of a Subgroup

Theorem: lagrange

(defthm dm::lagrange
  (implies (dm::subgroupp h dm::g)
           (equal (* (dm::order h)
                     (dm::subgroup-index h dm::g))
                  (dm::order dm::g))))

By David Russinoff, in books/projects/groups/quotients.lisp.

72. Sylow's Theorem

(def sylow-1)(def sylow-2)(def sylow-3)(def sylow-4)

By David Russinoff, in books/projects/groups/sylow.lisp.

73. Ascending or Descending Sequences

Theorem: asc-desc-subseqp

(defthm dm::asc-desc-subseqp
  (implies (and (dm::rat-listp l)
                (dm::dlistp l)
                (posp a)
                (posp b)
                (> (len l) (* (1- a) (1- b))))
           (let ((dm::asc (dm::longest-ascending-subseq l))
                 (dm::desc (dm::longest-descending-subseq l)))
             (and (dm::subseqp dm::asc l)
                  (dm::ascendingp dm::asc)
                  (dm::subseqp dm::desc l)
                  (dm::descendingp dm::desc)
                  (or (>= (len dm::asc) a)
                      (>= (len dm::desc) b))))))

By David Russinoff, in books/projects/numbers/subseq.lisp.

74. The Principle of Mathematical Induction

(encapsulate (((p *) => *))
  (local (defun p (n) n))
  (defthm p-0
    (p 0))
  (defthm p-recurrence
    (implies (and (natp n) (p n))
             (p (1+ n)))))

(defun n-induction (n)
  (if (posp n)
      (list (n-induction (1- n)))
    (list n)))

(defthm mathematical-induction
  (implies (natp n) (p n))
  :hints (("Goal" :induct (n-induction n))
          ("Subgoal *1/1" :use ((:instance p-recurrence (n (1- n)))))))

By David Russinoff.

75. The Mean Value Theorem

Theorems mvt-theorem and mvt-theorem-sk.

By Ruben Gamboa, in books/nonstd/nsa/derivatives.lisp.

Note: These theorems require ACL2(r).

78. The Cauchy-Schwarz Inequality

Theorems cauchy-schwarz-1, cauchy-schwarz-2, cauchy-schwarz-3, and cauchy-schwarz-4.

By Carl Kwan and Mark R. Greenstreet, in books/workshops/2018/kwan-greenstreet/cauchy-schwarz.lisp.

Note: These theorems require ACL2(r).

Theorems cs1, cs2, cs1-equality-implies-linear-dependence, cs2-equality-implies-linear-dependence, linear-dependence-implies-cs1-equality, and linear-dependence-implies-cs2-equality.

By Carl Kwan, Yan Peng, and Mark R. Greenstreet, in books/workshops/2020/kwan-peng-greenstreet/abstract-cs.lisp.

Note: These theorems require ACL2(r).

79. The Intermediate Value Theorem

Theorems intermediate-value-theoremand intermediate-value-theorem-sk.

By Ruben Gamboa, in books/nonstd/nsa/continuity.lisp.

Note: These theorems require ACL2(r).

80. The Fundamental Theorem of Arithmetic

First solution:

Theorem: product-lst-prime-factors

(defthm pos::product-lst-prime-factors
  (implies (and (integerp pos::x) (> pos::x 0))
           (equal (pos::product-lst (pos::prime-factors pos::x))
                  pos::x)))

Theorem: prime-factorization-uniqueness

(defthm pos::prime-factorization-uniqueness
  (implies (and (pos::prime-listp pos::lst1)
                (pos::prime-listp pos::lst2)
                (equal (pos::product-lst pos::lst1)
                       (pos::product-lst pos::lst2)))
           (pos::bag-equal pos::lst1 pos::lst2)))

By Ruben Gamboa and John Cowles, in books/workshops/2006/cowles-gamboa-euclid/Euclid/prime-fac.lisp.

Second solution:

Theorem: prime-fact-existence

(defthm dm::prime-fact-existence
  (implies (posp n)
           (let ((l (dm::prime-fact n)))
             (and (dm::prime-pow-list-p l)
                  (equal (dm::pow-prod l) n)))))

Theorem: prime-fact-uniqueness

(defthm dm::prime-fact-uniqueness
  (implies (and (posp n)
                (dm::prime-pow-list-p l)
                (equal (dm::pow-prod l) n))
           (equal (dm::prime-fact n) l)))

By David Russinoff, in books/projects/numbers/euclid.lisp.

81. Divergence of the Prime Reciprocal Series

Theorems thm-series-Recip-prime-divergess-traditional and i-large-sumRecip-prime-upto-n-i-large-integer.

By Ruben Gamboa.

85. Divisibility by 3 Rule

Theorem: divides-3-sum-list-digits

(defthm dm::divides-3-sum-list-digits
  (implies (natp n)
           (iff (dm::divides 3 (dm::sum-list (dm::digits n)))
                (dm::divides 3 n))))

By David Russinoff, in books/projects/numbers/div3.lisp.

88. Derangements Formula

Theorem: derangements-formula

(defthm dm::derangements-formula
  (implies (posp n)
           (equal (len (dm::derangements n))
                  (dm::num-derangements n))))

By David Russinoff, in books/projects/numbers/derangements.lisp.

93. The Birthday Problem

Theorem: probability-of-repetition-value

(defthm dm::probability-of-repetition-value
  (implies (and (natp k) (<= k 365))
           (equal (dm::probability-of-repetition k)
                  (- 1
                     (/ (dm::fact 365)
                        (* (dm::fact (- 365 k))
                           (expt 365 k)))))))

Theorem: probability-of-repetition-22

(defthm dm::probability-of-repetition-22
  (< (dm::probability-of-repetition 22)
     1/2))

Theorem: probability-of-repetition-23

(defthm dm::probability-of-repetition-23
  (> (dm::probability-of-repetition 23)
     1/2))

By David Russinoff, in books/projects/numbers/birthday.lisp.

96. Principle of Inclusion/Exclusion

Theorem: inclusion-exclusion-principle

(defthm dm::inclusion-exclusion-principle
  (implies (and (dm::dlistp u)
                (dm::dlistp l)
                (dm::sublistp l (dm::subsets u)))
           (equal (dm::inc-exc l)
                  (len (dm::union-list l)))))

By David Russinoff, in books/projects/numbers/sylvester.lisp.

97. Cramer's Rule

Theorem: cramer

(defthm dm::cramer
  (implies (and (dm::fmatp a n n)
                (natp n)
                (> n 1)
                (dm::invertiblep a n)
                (dm::flistnp b n)
                (dm::flistnp x n)
                (dm::solutionp x a b)
                (natp i)
                (< i n))
           (equal (nth i x)
                  (dm::f* (dm::f/ (dm::fdet a n))
                          (dm::fdet (dm::replace-col a i b) n)))))

By David Russinoff, in projects/linear/reduction.lisp.