The solutions to single-variable polynomials, implemented and verified in Lean

TL;DR

This paper details the process of formalizing solutions to quadratic, cubic, and quartic polynomials in Lean, comparing it with Coq, and reports modest improvements in formal proof verification over prior work.

Contribution

It provides a detailed account of learning Lean for polynomial solutions and offers a modest advancement over existing Coq formalizations.

Findings

Successful formalization of polynomial solutions in Lean

Comparison between Lean and Coq proof assistants

Modest improvements over previous Coq work

Abstract

In this work, we describe our experience in learning the use of a computer proof assistant - specifically, Lean - from scratch, through proving formulae for the solutions of polynomial equations. Specifically, in this work we characterize the solutions of quadratic, cubic, and quartic polynomials over certain fields, specifically, fields with operations returning square and cubic roots of characteristic other than two or three. The purpose of this work is thus twofold. Firstly, it describes the learning experience of a starting Lean user, including a detailed comparison between our work in Lean and very closely related work in Coq. Secondly, our results represent a modest improvement over the aforementioned related work in Coq, which we hope will be of some scientific interest.