Basel Problem

Basel Problem

Formalized Mathematics

Volume 25 (2017): Issue 2 (July 2017)

By:

Karol Pąk and Artur Korniłowicz

Open Access

|Sep 2017

Abstract

A rigorous elementary proof of the Basel problem [6, 1] $\sum_{n = 1}^{\infty} \frac{1}{n^{2}} = \frac{π^{2}}{6}$ $$\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/.

DOI: https://doi.org/10.1515/forma-2017-0014 | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630

Journal RSS Feed

Language: English

Page range: 149 - 155

Submitted on: Jun 27, 2017

Published on: Sep 23, 2017

Published by: University of Bialystok

In partnership with: Paradigm Publishing Services

Publication frequency: 1 times per year

Keywords:

Related subjects:

Computer sciences, other

© 2017 Karol Pąk, Artur Korniłowicz, published by University of Bialystok
This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 License.

Previous article Volume 25 (2017): Issue 2 (July 2017)Next article