作为多元与对称多项式应用的 e 与 $\pi$ 超越性形式化证明
计算机科学中的逻辑
2015-12-10 v1
摘要
我们描述了在 Coq 中形式化证明数 e 和 为超越数的过程。该证明位于两个常被视为独立领域的数学分支的交界面：微积分（实分析与初等复分析）与代数。关于微积分部分，我们依赖于 Coquelicot 库；关于代数部分，我们依赖于 Mathematical Components 库。此外，我们形式化证明的某些元素源自 Coq 发行版中包含的更早期的实数库。 的情况广泛依赖于多元多项式的性质，且本实验也是检验新开发的多元多项式库的一次机会。
引用
@article{arxiv.1512.02791,
title = {Formal Proofs of Transcendence for e and $\pi$ as an Application of Multivariate and Symmetric Polynomials},
author = {Sophie Bernard and Yves Bertot and Laurence Rideau and Pierre-Yves Strub},
journal= {arXiv preprint arXiv:1512.02791},
year = {2015}
}
备注
in Jeremy Avigad and Adam Chlipala. Certified Programs and Proofs, Jan 2016, St Petersburg, Florida, United States. ACM Press, pp.12, 2016