Lagrange's Four Square Theorem

Every natural number is the sum of four squares. Lagrange's Theorem in the wikipedia.

The proof uses Euler's Four Square Identity, see wikipedia

An alternative proof can be found here .

Lagrange's Theorem has been certified in

  1. HOL Light, John Harrison:
  2. Mizar, Yasushige Watase:
  3. Coq, Guillaume Allais & Jean-Marie Madiot:
  4. Isabelle, Roelof Oosterhuis:
  5. Metamath, Mario Carneiro:
This is Theorem 19 in the list of 100 certified theorems by Freek Wiedijk.

Computer checked proofs of mathematical theorems

Freek Wiedijk's book comparing 17 Proof Checkers can be found here. An updated list of Proof Checkers can be found here.

What is the meaning and value of computer checked proofs?

  1. Jeremy Avigad, John Harrison Formally Verified Mathematics , Communications of the ACM, Vol. 57 No. 4, Pages 66-75.
  2. Jesse Alama and Reinhard Kahle Checking proofs, . This is published as a chapter in the book The Argument of Mathematics , Eds. A. Aberdein and I. Dove, Springer, 2013. pp. 147-170.
  3. QED Manifesto , and references therein.
  4. The FLYSPECK project , and references therein.
  5. V. Voevodsky's Project UniMath Project .
  6. Will Computers Redefine the Roots of Math? , by Kevin Hartnett, in Quanta magazine, May 19, 2015.