Mahler (1953), §4 (13): $|\pi-p/q|>10^{-8.9101n}q^{-10}$ when $p<4q$, $n\ge50$, $10^{2.9245n}>q^{10}$

This is the intermediate estimate of Mahler's 1953 paper on rational approximations to $\pi$, stated in §4 as formulas (12)–(13).

Let $p$ and $q$ be positive integers with $p<4q$, and let $n$ be an integer satisfying

Then

Here $n$ is an auxiliary integer (the degree parameter of Mahler's auxiliary polynomials) which may be chosen freely subject to the two displayed conditions. In §5 of the paper Mahler chooses $n$ as a function of $q$ by $10^{2.9245(n-1)}\le q^{10}<10^{2.9245n}$, which turns this estimate into the bound $|\pi-p/q|>q^{-42}$ for all sufficiently large $q$; it is therefore the analytic core of the irrationality-measure bound $\mu(\pi)\le 42$.

Formalization Note $p$, $q$, $n$ are natural numbers with $0<p$, $0<q$, $p<4q$, $50\le n$. The powers $10^{2.9245n}$ and $10^{-8.9101n}$ are real powers, $q^{-10}$ is written as division by $q^{10}$, and $\pi$ is Mathlib's Real.pi.