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

18 Downloads (Pure)

Abstract

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

Fingerprint

Polynomial Complexity
Factorization
Polynomial
Integer
Polynomial time
Irreducible polynomial
Square free
Factoring
Formalization

Cite this

@article{cc976070e26a4a21bdfa2e5d5d19bbd8,
title = "A verified factorization algorithm for integer polynomials with polynomial complexity",
abstract = "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.",
author = "Jose Divas{\'o}n and Sebastiaan Joosten and Ren{\'e} Thiemann and Akihisa Yamada",
note = "Formal proof development",
year = "2018",
month = "2",
day = "6",
language = "English",
journal = "Archive of Formal Proofs",
issn = "2150-914x",
publisher = "SourceForge",

}

A verified factorization algorithm for integer polynomials with polynomial complexity. / Divasón, Jose; Joosten, Sebastiaan; Thiemann, René; Yamada, Akihisa.

In: Archive of Formal Proofs, 06.02.2018.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - A verified factorization algorithm for integer polynomials with polynomial complexity

AU - Divasón, Jose

AU - Joosten, Sebastiaan

AU - Thiemann, René

AU - Yamada, Akihisa

N1 - Formal proof development

PY - 2018/2/6

Y1 - 2018/2/6

N2 - 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.

AB - 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.

M3 - Article

JO - Archive of Formal Proofs

JF - Archive of Formal Proofs

SN - 2150-914x

ER -