仅数学证明助手 [英] Proof assistant for mathematics only

问题描述

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

Most proof assistants are functional programming languages with dependent types. They can proof programs/algorithms. I'm interested, instead, in proof assistant suitable best for mathematics and only (calculus for instance). Can you recommend one? I heard about Mizar but I don’t like that the source code is closed, but if it is best for math I will use it. How well the new languages such as Agda and Idris are suited for mathematical proofs?

推荐答案

Coq 具有涵盖实际分析的广泛库.各种发展浮现在脑海:

Coq has extensive libraries covering real analysis. Various developments come to mind:

• 标准库以及在其上构建的项目，例如现已失效的coqtail 项目[1](广泛覆盖幂级数，并在复数上作了大量工作)或更新的此处呈现的实物的公理定义.

• the standard library and projects building on it such as the now defunct coqtail project [1] (with extensive coverage of power series and quite a bit of work on Complex numbers) or the more recent coquelicot. All of these rely on an axiomatic definition of the reals presented here.

C-CoRN 项目提供了一种更具建设性的方法，该项目从实际构建实体开始./p>

A more constructive approach is delivered by the C-CoRN project which starts by actually building the reals.

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

Another way to tackle the reals is to turn to non-standard analysis. This is what people using ACL2 have been doing.

要更全面地了解该领域，您可能应该阅读有关遗赠的人本调查文件项目.

For a more general view of the field, you should probably read this survey paper by the people involved in the coquelicot project.

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

[1] full disclosure: I was involved in that project

这篇关于仅数学证明助手的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！