Skip to Content

Algebraic Numbers in Isabelle/HOL

Posted on

Authors:

  • Thiemann, René
  • Yamada, Akihisa
  • Joosten, Sebastiaan J. C.

Published in: Archive of Formal Proofs

https://www.isa-afp.org/entries/Algebraic_Numbers.html

Abstract:

Based on existing libraries for matrices, factorization of rational polynomials, and Sturm’s theorem, we formalized algebraic numbers in Isabelle/HOL. Our development serves as an implementation for real and complex numbers, and it admits to compute roots and completely factorize real and complex polynomials, provided that all coefficients are rational numbers. Moreover, we provide two implementations to display algebraic numbers, an injective and expensive one, or a faster but approximative version.

To this end, we mechanized several results on resultants, which also required us to prove that polynomials over a unique factorization domain form again a unique factorization domain.

BibTeX entry:

@article{Thiemann15,
 abstract = {Based on existing libraries for matrices, factorization of rational polynomials, and Sturm's theorem, we formalized algebraic numbers in Isabelle/HOL. Our development serves as an implementation for real and complex numbers, and it admits to compute roots and completely factorize real and complex polynomials, provided that all coefficients are rational numbers. Moreover, we provide two implementations to display algebraic numbers, an injective and expensive one, or a faster but approximative version.

To this end, we mechanized several results on resultants, which also required us to prove that polynomials over a unique factorization domain form again a unique factorization domain.},
 author = {Thiemann, Ren{\'e} and Yamada, Akihisa and Joosten, Sebastiaan Jozef Christiaan},
 bdsk-url-1 = {https://www.isa-afp.org/entries/Algebraic_Numbers.html},
 day = {22},
 journal = {Archive of Formal Proofs},
 month = {12},
 title = {Algebraic Numbers in Isabelle/HOL},
 url = {https://www.isa-afp.org/entries/Algebraic_Numbers.html},
 volume = {2015},
 year = {2015}
}