仅限数学证明助理

Question

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

Answer 1

Coq拥有广泛的图书馆,涵盖实际分我想到了各种各样的发展:

解决实际问题的另一种方法是转向非标准分析.这是人们使用的ACL2一直在做的事情.

有关该领域的更一般视图,您可能应该阅读这篇涉及虞美人项目的人员的调查报告.

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

我在Agda完成了过去4年的所有工作(在编程和证明的界面).在Agda中完成了相当大的正规化项目.但Coq受益于许多旨在自动化一些令人讨厌的证据的工作(例如,处理环,字段等时的所有(in)等式).最后,答案取决于你想做什么样的数学. (2认同)