$zeta(3)$的无理性的形式证明
摘要：在 Coq 证明助手上，我们完成了一项关于黎曼 zeta 函数在 3 处的求值是无理数的证明的完整形式验证。这个结果最初由 Ap''ery 在 1978 年提出，我们所验证的证明基本上遵循了他原始演示的路径。这个证明的关键在于确立某些序列满足共同的递归关系。我们通过对在 Maple 会话中通过计算机代数算法进行的计算进行事后验证，形式上证明了这个结果。证明的其余部分则结合了算数元素和渐近分析，我们通过扩展 Mathematical Components 库进行了这些分析。
作者：Assia Mahboubi and Thomas Sibut-Pinote
论文ID：1912.06611
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22