Gregory V. Chudnovsky

The irrationality exponent of the lemniscate period: A determinant proof with a Lean 4 formalization

Let $\Omega=2\int_0^1(1-t^4)^{-1/2}dt$. We prove that, for every real $\nu>2$, there is $Q\geq2$ such that $q^{-\nu}<|\Omega-p/q|$ for every integer $p$ and every integer $q\geq Q$. Consequently $\Omega$ is irrational and its irrationality exponent is two. The proof combines elliptic separated-weight interpolation, ari...