From: Lawrence Paulson <lp15@cam.ac.uk>

I am happy to announce a new entry, Solving Cubic and Quartic Equations, by René Thiemann:

We formalize Cardano's formula to solve a cubic equation,

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.

It’s another example of an entry building on a great heap of previous entries, taking close to an hour of CPU time to fully process. And I see that we recently passed the 3 million mark for the number of lines of formal proofs!

You’ll find it online here: https://www.isa-afp.org/entries/Cubic_Quartic_Equations.html

Larry Paulson

Last updated: Dec 05 2021 at 22:18 UTC