Basel Problem

Karol Pąk; Artur Korniłowicz

Basel Problem

Formalized Mathematics, Tome 25 (2017), p. 149-155 / Harvested from The Polish Digital Mathematics Library

Résumé

A rigorous elementary proof of the Basel problem [6, 1] ∑n=1∞1n2=π26 $\sum_{n = 1}^{\infty} \frac{1}{n^{2}} = \frac{π^{2}}{6}$ is formalized in the Mizar system [3]. This theorem is item 14 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.

Publié le : 2017-01-01
EUDML-ID : urn:eudml:doc:288499

@article{bwmeta1.element.doi-10_1515_forma-2017-0014,
     author = {Karol P\k ak and Artur Korni\l owicz},
     title = {Basel Problem},
     journal = {Formalized Mathematics},
     volume = {25},
     year = {2017},
     pages = {149-155},
     language = {en},
     url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0014}
}

Karol Pąk; Artur Korniłowicz. Basel Problem. Formalized Mathematics, Tome 25 (2017) pp. 149-155. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0014/