Towards Verified Polynomial Factorisation

TL;DR

This paper explores methods to verify the irreducibility of polynomial factors within computer algebra systems using the Lean proof assistant, addressing a challenging aspect of polynomial factorization verification.

Contribution

It introduces an approach to verify polynomial irreducibility in Lean, advancing formal methods in computer algebra verification.

Findings

Initial framework for irreducibility verification in Lean

Potential for improved reliability of polynomial factorization proofs

Foundation for future complete verification tools

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.