A Verified Implementation of Algebraic Numbers in Isabelle/HOL

Sebastiaan J.C. Joosten, René Thiemann* (Corresponding Author), Akihisa Yamada

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

3 Citations (Scopus)
21 Downloads (Pure)


We formalize algebraic numbers in Isabelle/HOL. Our development serves as a verified implementation of algebraic operations on real and complex numbers. We moreover provide algorithms that can identify all the real or complex roots of rational polynomials, and two implementations to display algebraic numbers, an approximative version and an injective precise one. We obtain verified Haskell code for these operations via Isabelle’s code generator. The development combines various existing formalizations such as matrices, Sturm’s theorem, and polynomial factorization, and it includes new formalizations about bivariate polynomials, unique factorization domains, resultants and subresultants.
Original languageEnglish
Pages (from-to)363-389
Number of pages27
JournalJournal of automated reasoning
Early online date9 Dec 2018
Publication statusPublished - Mar 2020
Externally publishedYes


  • Algebraic numbers
  • Real algebraic geometry
  • Resultants
  • deal
  • Theorem proving


Dive into the research topics of 'A Verified Implementation of Algebraic Numbers in Isabelle/HOL'. Together they form a unique fingerprint.

Cite this