论文标题
在精益中实现和验证的单变量多项式的解决方案
The solutions to single-variable polynomials, implemented and verified in Lean
论文作者
论文摘要
在这项工作中，我们描述了通过证明多项式方程解决方案的公式，描述了学习计算机证明助手的使用 - 特别是从头开始的经验。具体而言，在这项工作中，我们表征了某些字段上二次，立方和四分位多项式的解决方案，特别是具有返回正方形和立方根的特征和三个以外的两个或三个特征的字段。因此，这项工作的目的是双重的。首先，它描述了初学者的学习体验，包括我们在精益工作和COQ非常相关的工作之间的详细比较。其次，我们的结果代表了对COQ中上述相关工作的适度改进，我们希望这将具有一定的科学利益。
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.
