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?
Proof assistant for mathematics only
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
Can I assume from your answer that Agda is not suitable for mathematical proofs? –
Merriman
All my work (at the interface of programming & proving) for the past 4 years has been done in Agda. And there are pretty big formalisation projects fully done in Agda. But Coq benefits from a lot of work aiming to automate some annoying proofs (e.g. all the (in)equalities when dealing with rings, fields, etc.). In the end, the answer will depend on what kind of mathematics you want to do. –
Charolettecharon
Is there any benefits for using Mizar? –
Gaal
© 2022 - 2024 — McMap. All rights reserved.