Abstract: 
We formalize Cardano's formula to solve a cubic equation
$$ax^3 + bx^2 + cx + d = 0,$$ as well as Ferrari's formula to
solve a quartic equation. We further turn both formulas into
executable algorithms based on the algebraic number implementation in
the AFP. To this end we also slightly extended this library, namely by
making the minimal polynomial of an algebraic number executable, and
by defining and implementing $n$th roots of complex
numbers. 
BibTeX: 
@article{Cubic_Quartic_EquationsAFP,
author = {RenĂ© Thiemann},
title = {Solving Cubic and Quartic Equations},
journal = {Archive of Formal Proofs},
month = sep,
year = 2021,
note = {\url{https://isaafp.org/entries/Cubic_Quartic_Equations.html},
Formal proof development},
ISSN = {2150914x},
}
