### 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.

### License

BSD License

### Topics

- Mathematics/Analysis

### Session Cubic_Quartic_Equations

- Ferraris_Formula
- Cardanos_Formula
- Complex_Roots
- Cubic_Polynomials
- Quartic_Polynomials

### Depends on

- Algebraic Numbers in Isabelle/HOL
- Complex Geometry
- Factorization of Polynomials with Algebraic Coefficients

## Cite

×

Cubic_Quartic_Equations-AFP

    @article{Cubic_Quartic_Equations-AFP,
      author  = {René Thiemann},
      title   = {Solving Cubic and Quartic Equations},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Cubic_Quartic_Equations.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Sep 3, 2021 : Isabelle2021