@MISC{NIVEN.MIZ,
  AUTHOR = {Korni{\l}owicz, Artur and Naumowicz, Adam},
  TITLE = {Niven's Theorem},
  NOTE = {The work on the formalization presented in this article
    was completed thanks to the Mizar Mathematical Library maintenance
    and refactoring carried out at the Computer Center of the
    University of Bia{\l}ystok.},
  DAY = {15},
  MONTH = {December},
  YEAR = {2016},
  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},
  SUMMARY = {This article formalizes the proof of Niven's theorem which
  states that if $x/\pi$ and $sin x$ are both rational, then the sine takes
  values $0$, $\pm 1/2$, and $\pm 1$. The main part of the formalization follows
  the informal proof presented at Pr$\infty$fWiki
  (\url{https://proofwiki.org/wiki/Niven's_Theorem#Source_of_Name}).
  For this proof, we have also formalized the rational and integral root
  theorems setting constraints on solutions of polynomial equations with
  integer coefficients.}}

