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
-
HOL Light, John Harrison:
-
Mizar, Yasushige Watase:
-
Coq, Guillaume Allais & Jean-Marie Madiot:
-
Isabelle, Roelof Oosterhuis:
-
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?
-
Jeremy Avigad, John Harrison
Formally Verified Mathematics
,
Communications of the ACM, Vol. 57 No. 4, Pages 66-75.
-
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.
-
QED Manifesto
, and references therein.
-
The FLYSPECK project
, and references therein.
-
V. Voevodsky's
Project
UniMath Project
.
-
Will Computers Redefine the Roots of Math?
, by Kevin Hartnett, in Quanta magazine,
May 19, 2015.