<abstract xmlns="http://www.w3.org/1999/xhtml"><p>A rigorous elementary proof of the Basel problem [6, 1]
<disp-formula><alternatives><graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2017-0014_eq_001.png"></graphic><math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mrow><mstyle><msubsup><mo>∑</mo><mrow><mi>n</mi><mo>=</mo><mn>1</mn></mrow><mi>∞</mi></msubsup><mrow><mfrac><mn>1</mn><mrow><msup><mi>n</mi><mn>2</mn></msup></mrow></mfrac><mo>=</mo><mfrac><mrow><msup><mi>π</mi><mn>2</mn></msup></mrow><mn>6</mn></mfrac></mrow></mstyle></mrow></math><tex-math>$$\sum\nolimits_{n = 1}^\infty {{1 \over {n^2 }} = {{\pi ^2 } \over 6}} $$</tex-math></alternatives></disp-formula>
is formalized in the Mizar system [<xref ref-type="bibr" rid="j_forma-2017-0014_ref_003_w2aab3b7b6b1b6b1ab1ab3Aa">3</xref>]. This theorem is item #14 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at <ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="http://www.cs.ru.nl/F.Wiedijk/100/">http://www.cs.ru.nl/F.Wiedijk/100/</ext-link>.</p></abstract>

A rigorous elementary proof of the Basel problem [6, 1]
∑n=1∞1n2=π26$$\sum\nolimits_{n = 1}^\infty {{1 \over {n^2 }} = {{\pi ^2 } \over 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/.

Basel Problem

Formalized Mathematics

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

{"article-title":"Basel Problem"}

A rigorous elementary proof of the Basel problem [6, 1]
∑n=1∞1n2=π26$$\sum\nolimits_{n = 1}^\infty {{1 \over {n^2 }} = {{\pi ^2 } \over 6}} $$
is formalized in...

Basel Problem

Data publikacji: 23 wrz 2017

Zakres stron: 149 - 155

Otrzymano: 27 cze 2017

DOI: https://doi.org/10.1515/forma-2017-0014

Słowa kluczowe
Basel problem

© 2017 Karol Pąk et al., published by De Gruyter Open

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Basel Problem

Data publikacji: 23 wrz 2017

Zakres stron: 149 - 155

Otrzymano: 27 cze 2017

DOI: https://doi.org/10.1515/forma-2017-0014

Słowa kluczoweBasel problem

© 2017 Karol Pąk et al., published by De Gruyter Open

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Słowa kluczowe
Basel problem