@ARTICLE{NUMBER11.MIZ,
  AUTHOR = {Naumowicz, Adam},
  TITLE = {Elementary Number Theory Problems. {P}art {XI}},
  NOTE = {The Mizar processing has been performed using the infrastructure
    of the University of Bialystok High Performance Computing Center.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Problem 36},
  DAY = {12},
  MONTH = {December},
  YEAR = {2023},
  ADDRESS1 = {Faculty of Computer Science\\University of Bia{\l}ystok\\ Konstantego Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SUMMARY = {In this paper we present the Mizar formalization of the 36th problem from
  W. Sierpinski's book ``250 Problems in Elementary Number Theory'' \cite{Sierpinski:1970}.
  For every positive integer $s\leq25$ and for $s=100$ we provide the least
  positive integer with the sum of digits (in decimal system) equal to $s$,
  which is divisible by $s$. The last case calls for a number with decimal digits
  composed of a leading $1$, followed by a sequence of eleven $9$s, and two trailing $0$s.}
  }

@BOOK{Sierpinski:1970,
 AUTHOR={Sierpi{\'n}ski, Wac{\l}aw},
 TITLE={250 Problems in Elementary Number Theory},
 PUBLISHER={Elsevier},
 YEAR=1970}
