@MISC{BASEL_2.MIZ,
  AUTHOR = {P\k{a}k, Karol and Korni{\l}owicz, Artur},
  TITLE = {Basel Problem},
  DAY = {27},
  MONTH = {June},
  YEAR = {2017},
  NOTE = {This work has been financed by the
    resources of the Polish National Science Centre granted by decision
    no. DEC-2015/19/D/ST6/01473.},
  ADDRESS1 = {Institute of Informatics\\University of Bia{\l}ystok\\Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  ADDRESS2 = {Institute of Informatics\\University of Bia{\l}ystok\\Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SECTION1 = {Preliminaries},
  SECTION2 = {Imaginary complex numbers},
  SECTION3 = {Main facts},
  SUMMARY = {A~rigorous elementary proof of the Basel problem $$\Sigma_{n=1}^\infty\frac{1}{n^2} = \frac{\pi^2}{6}$$
  is formalized in the Mizar system \cite{Mizar-State-2015}.
  It is item #14 from the ``Formalizing 100 Theorems'' list maintained by Freek Wiedijk
  at http://www.cs.ru.nl/F.Wiedijk/100/.},
}
