Certified integer polynomial factorization in Lean
I'm happy to announce the release of further packages for Hex, the computer algebra library for Lean.
Today we have an integer polynomial factorization library, including tactics for factorizing and irreducibility.
To get started, add to your lakefile.toml:
[[require]] name = "hex" git = "https://github.com/leanprover/hex.git" rev = "main"
and then:
import HexBerlekampZassenhausMathlib
open Polynomial
example : Irreducible (X ^ 4 + 8 * X + 12 : Polynomial ℤ) := ⊢ Irreducible (X ^ 4 + 8 * X + 12)
All goals completed! 🐙
-- Factor the product of two cyclotomic polynomials.
noncomputable def cyclo :=
factor_poly (X^10+2*X^9+3*X^8+4*X^7+5*X^6+5*X^5+5*X^4+4*X^3+3*X^2+2*X+1 : Polynomial ℤ)
-- The two factors it found are Φ₅ and Φ₇.
example : cyclo.factors = [1+X+X^2+X^3+X^4, 1+X+X^2+X^3+X^4+X^5+X^6] := ⊢ cyclo.factors = [1 + X + X ^ 2 + X ^ 3 + X ^ 4, 1 + X + X ^ 2 + X ^ 3 + X ^ 4 + X ^ 5 + X ^ 6]
All goals completed! 🐙
-- They are irreducible, and they multiply back to the input.
example : ∀ q ∈ cyclo.factors, Irreducible q := cyclo.factors_irred
example : C cyclo.scalar * cyclo.factors.prod =
X^10+2*X^9+3*X^8+4*X^7+5*X^6+5*X^5+5*X^4+4*X^3+3*X^2+2*X+1 := cyclo.factors_mul
-- The degree-8 Swinnerton-Dyer polynomial, the minimal polynomial of
-- √2 + √3 + √5. It is irreducible over ℤ but factors modulo every prime,
-- so no modular witness certifies it (even with multiple primes).
-- `irreducibility!` re-runs the factorizer in the kernel instead.
example : Irreducible
(X ^ 8 - 40 * X ^ 6 + 352 * X ^ 4 - 960 * X ^ 2 + 576 : Polynomial ℤ) := ⊢ Irreducible (X ^ 8 - 40 * X ^ 6 + 352 * X ^ 4 - 960 * X ^ 2 + 576)
All goals completed! 🐙
There's quite a lot going on here. We implement the Berlekamp algorithm for factoring mod p, Hensel lifting, and the Berlekamp-Zassenhaus algorithm, with efficient factor reconstruction using van Hoeij's knapsack method (Factoring polynomials and the knapsack problem, J. Number Theory 95 (2002) 167-189).
The van Hoeij algorithm has never previously been formally verified! We build on top of the previously released lattice basis reduction library in Hex.
(Isabelle has a lattice based reconstruction algorithm, but it is the original LLL algorithm, which is polynomial time but with poor constants. The van Hoeij method is efficient in practice as well!)
Our performance numbers are quite good: we are consistently faster than Isabelle, and appear to have similar asymptotic behaviour to the state-of-the-art unverified libraries, running about 5x slower than FLINT.
Two plots, both cumulative "cactus" plots of instances solved against time:
As usual for Hex, these libraries are split into purely computational libraries that do not depend on Mathlib, plus associated libraries that make the connection with Mathlib theory. (The irreducibility and factoring tactics work in the purely computational setting, and then gain capabilities to handle Mathlib polynomials once you import the Mathlib libraries.) In the medium term I am interested in merging the "with Mathlib" libraries into Mathlib (adding the computational libraries as dependencies), which would make these tactics available within Mathlib, and to all projects that import Mathlib without the need for further dependencies.
Unreleased libraries, and all future development, live at github.com/kim-em/hex-dev. Contributions and pull requests are welcome, but specs must be updated before any new features or substantial changes, as separately reviewed PRs.