2 papers
cs.SC2024
Towards Verified Polynomial Factorisation
James H. Davenport
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,…
cs.SC2024
First steps towards Computational Polynomials in Lean
James Harold Davenport
The proof assistant Lean has support for abstract polynomials, but this is not necessarily the same as support for computations with polynomials. Lean is also a functional programm…