Towards Verified Polynomial Factorisation
Symbolic Computation
2024-09-17 v1
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.
Cite
@article{arxiv.2409.09533,
title = {Towards Verified Polynomial Factorisation},
author = {James H. Davenport},
journal= {arXiv preprint arXiv:2409.09533},
year = {2024}
}