Formalized Mathematics
Special Issue: 25 years of the Mizar Mathematical Library
O artykule
Data publikacji: 30 cze 2014
Zakres stron: 105 - 110
Otrzymano: 04 cze 2014
DOI: https://doi.org/10.2478/forma-2014-0012
Słowa kluczowe
© 2014 Yasushige Watase
This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)
This article provides a formalized proof of the so-called “the four-square theorem”, namely any natural number can be expressed by a sum of four squares, which was proved by Lagrange in 1770. An informal proof of the theorem can be found in the number theory literature, e.g. in [14], [1] or [23].
This theorem is item #19 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.