Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Verified Polynomial Factorisation

James H. Davenport

TL;DR

This work tackles the problem of producing machine-checked evidence that a polynomial factorization in $\mathbf{Z}[x]$ is irreducible by proposing a family of certificate-based verifications implemented or planned for Lean. It develops several certificate variants (Simple, pre-Musser, Simple post-Musser, Complex post-Musser) that combine modular factorizations, Hensel lifting, and p-adic checks to certify irreducibility without relying on external trust. A core technical component is irreducibility modulo primes via Distinct Degree Factorisation and gcd tests like $\gcd(f(t), t^{p^j}-t)$, together with a robust bound-calculation framework based on Mignotte lemmas to control factor coefficients. The project aims to deliver a formally verified, certificate-backed pathway for polynomial factorization in proof assistants, improving reliability for computer algebra systems and formal proofs of irreducibility, with ongoing work to complete the bound proofs and Lean formalizations.

Abstract

Computer algebra systems are really good at factoring polynomials, i.e. writing f as a product of irreducible factors. It is relatively easy to verify that we have a factorisation, but verifying that these factors are irreducible is a much harder problem. This paper reports work-in-progress to do such verification in Lean.

Towards Verified Polynomial Factorisation

TL;DR

This work tackles the problem of producing machine-checked evidence that a polynomial factorization in is irreducible by proposing a family of certificate-based verifications implemented or planned for Lean. It develops several certificate variants (Simple, pre-Musser, Simple post-Musser, Complex post-Musser) that combine modular factorizations, Hensel lifting, and p-adic checks to certify irreducibility without relying on external trust. A core technical component is irreducibility modulo primes via Distinct Degree Factorisation and gcd tests like , together with a robust bound-calculation framework based on Mignotte lemmas to control factor coefficients. The project aims to deliver a formally verified, certificate-backed pathway for polynomial factorization in proof assistants, improving reliability for computer algebra systems and formal proofs of irreducibility, with ongoing work to complete the bound proofs and Lean formalizations.

Abstract

Computer algebra systems are really good at factoring polynomials, i.e. writing f as a product of irreducible factors. It is relatively easy to verify that we have a factorisation, but verifying that these factors are irreducible is a much harder problem. This paper reports work-in-progress to do such verification in Lean.
Paper Structure (13 sections, 3 theorems, 11 equations, 1 figure, 1 algorithm)

This paper contains 13 sections, 3 theorems, 11 equations, 1 figure, 1 algorithm.

Table of Contents

  1. Introduction
  2. The Standard Algorithm for Factoring
  3. A proof of irreducibility
  4. The Simple Certificate
  5. The pre-Musser Certificate
  6. The Simple post-Musser Certificate
  7. A Complex post-Musser Certificate
  8. Irreducibility Modulo $p$
  9. Distinct Degree Factorisation
  10. Bounds
  11. Formal Proof and "Similarly"
  12. Formal proof of the rest of the bound
  13. Conclusions

Key Result

Theorem 1

For $i \ge 1$ the polynomial is the product of all monic irreducible polynomials in $\mathbf {F} _{q}[x]$ whose degree divides $i$.

Figures (1)

  • Figure 1: Mignotte Lemma 1a in Lean

Theorems & Definitions (4)

  • Theorem 1
  • Remark 1
  • Corollary 1: To Theorem \ref{['Thm:DD']}
  • Lemma 1