Introduction to Diophantine Approximation. Part II

In the article we present in the Mizar system [1], [2] the formalized proofs for Hurwitz’ theorem [4, 1891] and Minkowski’s theorem [5]. Both theorems are well explained as a basic result of the theory of Diophantine approximations appeared in [3], [6]. A formal proof of Dirichlet’s theorem, namely an inequation |θ−y/x| ≤ 1/x² has infinitely many integer solutions (x, y) where θ is an irrational number, was given in [8]. A finer approximation is given by Hurwitz’ theorem: |θ− y/x|≤ 1/√5x². Minkowski’s theorem concerns an inequation of a product of non-homogeneous binary linear forms such that |a₁x + b₁y + c₁| · |a₂x + b₂y + c₂| ≤ ∆/4 where ∆ = |a₁b₂ − a₂b₁| ≠ 0, has at least one integer solution.