Algebraic numbers in Isabelle/HOL. (English) Zbl 1478.68443

Blanchette, Jasmin Christian (ed.) et al., Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9807, 391-408 (2016).
Summary: We formalize algebraic numbers in Isabelle/HOL, based on existing libraries for matrices and Sturm’s theorem. Our development serves as a verified implementation for real and complex numbers, and it admits to compute roots and completely factor 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, and a faster but approximative version.
To this end, we mechanize several results on resultants, which also required us to prove that polynomials over a unique factorization domain form again a unique factorization domain. We moreover formalize algorithms for factorization of integer polynomials: Newton interpolation, factorization over the integers, and Kronecker’s factorization algorithm, as well as a factorization oracle via Berlekamp’s algorithm with the Hensel lifting.
For the entire collection see [Zbl 1343.68004].


68V20 Formalization of mathematics in connection with theorem provers
03B35 Mechanization of proofs and logical operations
11R04 Algebraic numbers; rings of algebraic integers
13P15 Solving polynomial systems; resultants
68W30 Symbolic computation and algebraic computation
Full Text: DOI


[1] Brown, W.S.: The subresultant PRS algorithm. ACM Trans. Math. Softw. 4(3), 237–249 (1978) · Zbl 0385.68044
[2] Cohen, C.: Construction of real algebraic numbers in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 67–82. Springer, Heidelberg (2012) · Zbl 1360.68744
[3] Cohen, C., Djalal, B.: Formalization of a Newton series representation of polynomials. In: CPP 2016, pp. 100–109. ACM (2016)
[4] Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Log. Methods Comput. Sci. 8(1:02), 1–40 (2012) · Zbl 1241.68096
[5] Collins, G.E.: Subresultants and reduced polynomial remainder sequences. J. ACM 14, 128–142 (1967) · Zbl 0152.35403
[6] Eberl, M.: A decision procedure for univariate real polynomials in Isabelle/HOL. In: CPP 2015, pp. 75–83. ACM (2015)
[7] Haftmann, F., Krauss, A., Kunčar, O., Nipkow, T.: Data refinement in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 100–115. Springer, Heidelberg (2013) · Zbl 1317.68212
[8] Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131–146. Springer, Heidelberg (2013) · Zbl 1426.68284
[9] Knuth, D.E.: The Art of Computer Programming. Seminumerical Algorithms, vol. 2, 2nd edn. Addison-Wesley, Boston (1981) · Zbl 0477.65002
[10] Krauss, A.: Recursive definitions of monadic functions. In: PAR 2010. EPTCS, vol. 43, pp. 1–13 (2010)
[11] Li, W., Paulson, L.C.: A modular, efficient formalisation of real algebraic numbers. In: CPP 2016, pp. 66–75. ACM (2016)
[12] Mahboubi, A.: Proving formally the implementation of an efficient gcd algorithm for polynomials. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 438–452. Springer, Heidelberg (2006) · Zbl 1222.68369
[13] Mishra, B.: Algorithmic Algebra. Texts and Monographs in Computer Science. Springer, Heidelberg (1993)
[14] Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL–A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002) · Zbl 0994.68131
[15] Prasolov, V.V.: Polynomials. Springer, Heidelberg (2004) · Zbl 1272.12001
[16] Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle/HOL. In: CPP 2016, pp. 88–99. ACM (2016)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.