Proof assistant for mathematics only

问题:

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?

回答1:

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

• 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.

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

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] full disclosure: I was involved in that project