A verified factorization algorithm for integer polynomials with polynomial complexity

Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada

    Research output: Contribution to journalArticleAcademicpeer-review

    39 Downloads (Pure)


    Short vectors in lattices and factors of integer polynomials are related. Each factor of an integer polynomial belongs to a certain lattice. When factoring polynomials, the condition that we are looking for an irreducible polynomial means that we must look for a small element in a lattice, which can be done by a basis reduction algorithm. In this development we formalize this connection and thereby one main application of the LLL basis reduction algorithm: an algorithm to factor square-free integer polynomials which runs in polynomial time. The work is based on our previous Berlekamp–Zassenhaus development, where the exponential reconstruction phase has been replaced by the polynomial-time basis reduction algorithm. Thanks to this formalization we found a serious flaw in a textbook.
    Original languageEnglish
    Number of pages79
    JournalArchive of Formal Proofs
    Publication statusPublished - 6 Feb 2018


    Dive into the research topics of 'A verified factorization algorithm for integer polynomials with polynomial complexity'. Together they form a unique fingerprint.

    Cite this