Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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?

like image 919
Yury Avatar asked Feb 16 '15 09:02

Yury


1 Answers

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

like image 63
gallais Avatar answered Sep 22 '22 16:09

gallais