Niven’s Theorem

摘要

This article formalizes the proof of Niven’s theorem [ 12 ] which states that if x/π and sin(x) are both rational, then the sine takes values 0, ±1/2, and ±1. The main part of the formalization follows the informal proof presented at Pr∞fWiki ( 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 [ 8 , 9 ].