Email Gateway (Sep 03 2021 at 16:14): Email Gateway (Sep 03 2021 at 16:14):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: Apr 25 2024 at 12:23 UTC