  Diophantine equations are a popular and active area of research in number
theory. In this paper we consider Mordell equations, which are of the form
$y^2=x^3+d$, where $d$ is a (given) nonzero integer number and all solutions in
integers $x$ and $y$ have to be determined. One non-elementary approach for
this problem is the resolution via descent and class groups. Along these lines
we formalized in Lean 3 the resolution of Mordell equations for several
instances of $d<0$. In order to achieve this, we needed to formalize several
other theories from number theory that are interesting on their own as well,
such as ideal norms, quadratic fields and rings, and explicit computations of
the class number. Moreover we introduced new computational tactics in order to
carry out efficiently computations in quadratic rings and beyond.
