A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm

Jose Divason, Sebastiaan J. C. Joosten, Rene Thiemann and Akihisa Yamada

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), pp. 17 – 29, 2017.


We formalize the Berlekamp–Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun’s square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials.
The algorithm first performs a factorization in the prime field GF(p) and then performs computations in the ring of integers modulo p^k, where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using Isabelle’s recent addition of local type definitions.
Through experiments we verify that our algorithm factors polynomials of degree 100 within seconds.


  PDF |    doi:10.1145/3018610.3018617  


author = {Jos{\'{e}} Divas{\'{o}}n and Sebastiaan J. C. Joosten and Ren{\'{e}} Thiemann and Akihisa Yamada},
title = {A Formalization of the {B}erlekamp--{Z}assenhaus Factorization Algorithm},
booktitle = {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs},
series = {CPP 2017},
year = {2017},
isbn = {978-1-4503-4705-1},
location = {Paris, France},
pages = {17--29},
numpages = {13},
url = {},
doi = {10.1145/3018610.3018617},
acmid = {3018617},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Isabelle, Polynomial Factorization, Prime Fields}
Nach oben scrollen