Proof for math only

Question

Most proof-of-concept assistants are functional types with dependent types. They can check programs / algorithms. I am interested, instead, in the evidence assistant, suitable for mathematics and only (e.g. calculus). Can you recommend it? I heard about Mizar, but I don’t like the source code is closed, but if it is better for math, I will use it. How well are new languages ​​like Agda and Idris suitable for mathematical proofs?

Answer 1

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

• the standard library and projects built on it, such as the now defunct coqtail project [1] (with a wide range of power series and quite a lot of work on complex numbers) or later coquelicot . They all rely on the axiomatic definition of the reals presented here .

• A more constructive approach is provided by the C-CoRN project , which begins with the actual construction of realities .

Another way to solve this problem is to turn to non-standard analysis. This is done by people using ACL2 .

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

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