Pell's Equation

In Freek's list of theorems, the existence of non-trivial solutions to Pell's equation $x^2-dy^2=1$ was previously resolved for $d$ of the form $d = a^2-1$. In this work, we formalize the existence of non-trivial solutions to Pell's equation $x^2-dy^2=1$ in Lean in the most general setting - when $d$ is nonsquare.

Our formalization closely follows the proof using Dirichlet's theorem on diophantine approximation. For example, see this.

Contents

No.	File	Contents
1	Theorem1	Dirichlet's theorem (Lemma 1 here)
2	Corollary2	Descent step (Lemma 2 here)
3	Theorem3	Existence of Solutions to Pell's (Theorem 3 here)
4	Theorem4	Characterization of Solutions to Pell's (WIP)