仅数学证明助理

Question

大多数证明助手都是具有依赖类型的函数式编程语言。他们可以证明程序/算法。相反，我感兴趣的是最适合数学并且仅适合数学(例如微积分)的证明助手。你能推荐一个吗？我听说过 Mizar，但我不喜欢源代码被关闭，但如果它最适合数学，我会使用它。 Agda 和 Idris 等新语言有多适合数学证明？

Answer 1

Coq拥有涵盖实际分析的广泛库。我想到了各种发展:

• standard library以及在此基础上构建的项目，例如现已不复存在的 coqtail项目 [1](广泛涵盖幂级数，并在复数方面做了大量工作)或更新的 coquelicot 。所有这些都依赖于实数的公理定义presented here .

• the C-CoRN 提出了更具建设性的方法。项目从实际构建实数开始。

处理实数的另一种方法是转向非标准分析。这就是人们使用的ACL2一直在做。

要更全面地了解该领域，您可能应该阅读 this survey paper由参与虞美人项目的人们创建。

[1] 全面披露:我参与了该项目