@MISC{NUMPOLY1.MIZ,
  AUTHOR = {Grabowski, Adam},
  TITLE = {Polygonal Numbers},
  SECTION1 = {Preliminaries},
  SECTION2 = {Triangular Numbers},
  SECTION3 = {Polygonal Numbers},
  SECTION4 = {Centered Polygonal Numbers},
  SECTION5 = {On the Connection between Triangular and Other Polygonal Numbers},
  SECTION6 = {Sets of Polygonal Numbers},
  SECTION7 = {Some Well-known Properties},
  SECTION8 = {Reciprocals of Triangular Numbers},
  DAY = {19},
  MONTH = {May},
  YEAR = {2013},
  ADDRESS1 = {Institute of Informatics\\University of Bia{\l}ystok\\Akademicka 2, 15-267 Bia{\l}ystok\\Poland},
  SUMMARY = {In the article the formal characterization of
  triangular numbers (famous from \cite{Gauss:1986} and
  words "EYPHKA! num = $\Delta + \Delta + \Delta$") \cite{Heath:1921}
    is given. Our primary aim was to formalize
  one of the items (#42) from Wiedijk's Top 100 Mathematical Theorems
  list \cite{Freek-100-theorems},
  namely that the sequence of sums of reciprocals of triangular numbers
  converges to 2 and this Mizar representation was written in 2007.
  As the Mizar language evolved and attributes with arguments were
  implemented, we decided to extend these lines and we characterized
  polygonal numbers.\par
  We formalized
  centered polygonal numbers, the connection between triangular
  and square numbers, and also some equalities involving Mersenne
  primes and perfect numbers. We gave also explicit formula
  to obtain from the polygonal number its ordinal index.
  Also selected congruences modulo 10 were enumerated.
  Our work basically covers the Wikipedia item for triangular
  numbers and the Online Encyclopedia of Integer Sequences
  \url{http://oeis.org/A000217}.
  \par
  An interesting related result \cite{Guy:1994} could be the proof
  of Lagrange's four-square theorem or Fermat's polygonal number theorem
  \cite{Weil:1983}.}}

@BOOK{Gauss:1986,
 AUTHOR = {Gauss, Carl Friedrich},
 TITLE = {Disquisitiones Arithmeticae},
 PUBLISHER = {Springer},
 YEAR = 1986,
 ADDRESS = {New York},
 NOTE = {English translation}}

@ARTICLE{Guy:1994,
 AUTHOR = {Guy, Richard K.},
 TITLE = {Every number is expressible as a sum of how many
   polygonal numbers?},
 JOURNAL = {American Mathematical Monthly},
 YEAR = 1994,
 VOLUME = {101},
 PAGES={169--172}}

@BOOK{Weil:1983,
 AUTHOR = {Weil, Andr\'e},
 TITLE = {Number Theory, an Approach through History from {H}ammurapi
    to {L}egendre},
 PUBLISHER = {Birkh\"auser},
 YEAR = 1983,
 ADDRESS = {Boston, Mass.}}

@BOOK{Heath:1921,
 AUTHOR = {Heath, Thomas L.},
 TITLE = {A History of {G}reek Mathematics: From {T}hales to {E}uclid, Vol. {I}},
 PUBLISHER = {Courier Dover Publications},
 YEAR = 1921}

