Abstract: 
This article gives the basic theory of Pell's equation
x^{2} = 1 +
D y^{2},
where
D ∈ ℕ is
a parameter and x, y are
integer variables. The main result that is proven
is the following: If D is not a perfect square,
then there exists a fundamental solution
(x_{0},
y_{0}) that is not the
trivial solution (1, 0) and which generates all other solutions
(x, y) in the sense that
there exists some
n ∈ ℕ
such that x +
y √D =
(x_{0} +
y_{0} √D)^{n}.
This also implies that the set of solutions is infinite, and it gives
us an explicit and executable characterisation of all the solutions.
Based on this, simple executable algorithms for
computing the fundamental solution and the infinite sequence of all
nonnegative solutions are also provided. 
BibTeX: 
@article{PellAFP,
author = {Manuel Eberl},
title = {Pell's Equation},
journal = {Archive of Formal Proofs},
month = jun,
year = 2018,
note = {\url{http://isaafp.org/entries/Pell.html},
Formal proof development},
ISSN = {2150914x},
}
