大多数证明助手都是具有依赖类型的函数式编程语言。他们可以证明程序/算法。相反，我对最适合数学且仅适用于数学的证明助手感兴趣（例如微积分）。你能推荐一个吗？我听说过 Mizar，但我不喜欢源代码是封闭的，但如果它最适合数学，我会使用它。Agda 和 Idris 等新语言在多大程度上适合数学证明？
问问题
905 次
1 回答
12
Coq拥有涵盖实际分析的广泛库。各种发展浮现在脑海中：
标准库和建立在其上的项目，例如现已解散的coqtail项目 [1]（广泛涵盖幂级数和大量关于复数的工作）或最近的coquelicot。所有这些都依赖于此处介绍的实数的公理化定义。
C-CoRN项目提供了一种更具建设性的方法，该项目从实际构建实数开始。
另一种处理实数的方法是转向非标准分析。这就是人们ACL2一直在做的事情。
为了更全面地了解该领域，您可能应该阅读参与 coquelicot 项目的人员撰写的这份调查报告。
[1] 完全披露：我参与了那个项目
于 2015-02-16T14:37:48.380 回答