A Formal Proof of the Irrationality of $\hat{I}\P (3)$ in Lean 4

Junqi Liu, Jujian Zhang, Lihong Zhi

We formalize a proof of the irrationality of $\hat{I}\P (3)$ in Lean 4, using Beukers' method. To support this, we extend the Lean mathematical library (Mathlib) by formalizing shifted Leg…