|
| | | | |
| | | |
| Stat |
Members: 3669
Articles: 2'599'751
Articles rated: 2609
16 March 2025 |
|
| | | | |
|
Article overview
| |
|
|
The solutions to single-variable polynomials, implemented and verified in Lean | | Nicholas Dyson
; Benedikt Ahrens
; Jacopo Emmenegger
; | | Date: |
2 Jan 2022 | | 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. | | Source: | arXiv, 2201.00255 | | Services: | Forum | Review | PDF | Favorites | |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
|
| |
|
|
|
REGISTER