The Factorization Algorithm of Berlekamp and Zassenhaus

Jose Divasón 🌐, Sebastiaan J. C. Joosten 📧, René Thiemann 🌐 and Akihisa Yamada 📧

October 14, 2016


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 integer ring 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.


BSD License


April 12, 2024
Added interface to simplify usage of generated code.


Related publications

  • Divasón, J., Joosten, S. J. C., Thiemann, R., & Yamada, A. (2019). A Verified Implementation of the Berlekamp–Zassenhaus Factorization Algorithm. Journal of Automated Reasoning, 64(4), 699–735.
  • von zur Gathen, J., & Gerhard, J. (2013). Modern Computer Algebra.
  • Wikipedia

Session Berlekamp_Zassenhaus