  In this article we consider mathematical fundamentals of one method for
proving inequalities by computer, based on the Remez algorithm. Using the
well-known results of undecidability of the existence of zeros of real
elementary functions, we demonstrate that the considered method generally in
practice becomes one heuristic for the verification of inequalities. We give
some improvements of the inequalities considered in the theorems for which the
existing proofs have been based on the numerical verifications of Remez
algorithm.
