Abstract

We formalize Berlekamp’s algorithm for factoring polynomials over prime
fields in Isabelle/HOL. We first formalize the algorithm by defining a
dedicated type for prime fields, and state the initial soundness theorem
depending on this type. We then eliminate the type from the statement using
the recently added functionality of local type definitions.

In order to efficiently execute Berlekamp’s algorithm, and to employ the
algorithm in factorization of integer polynomials,we further generalize
and optimize polynomial division algorithms.

The generated code is already used in the formalization for algebraic
numbers, where it is an ingredient of a modern factorization algorithm
for integer polynomials, although currently only as an oracle.

BibTeX

@inproceedings{JDSJRTAY-Isabelle2016,
  author    = "Jose Divas\'on and Sebastiaan Joosten and Ren\'e Thiemann
               and Akihisa Yamada",
  title     = "A Formalization of Berlekamp’s Factorization Algorithm",
  booktitle = "Isabelle Workshop 2016",
  year      = 2016
}