<abstract xmlns="http://www.w3.org/1999/xhtml"><p>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].</p><p>This theorem is item #19 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.</p></abstract>

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/.

Lagrange’s Four-Square Theorem

Suginami-ku Matsunoki 6, 3-21 Tokyo, Japan

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

{"article-title":"Lagrange\u2019s Four-Square Theorem"}

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...

Lagrange’s Four-Square Theorem

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
Lagrange’s four-square theorem

© 2014 Yasushige Watase

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

Lagrange’s Four-Square Theorem

Data publikacji: 30 cze 2014

Zakres stron: 105 - 110

Otrzymano: 04 cze 2014

DOI: https://doi.org/10.2478/forma-2014-0012

Słowa kluczoweLagrange’s four-square theorem

© 2014 Yasushige Watase

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

Słowa kluczowe
Lagrange’s four-square theorem