All Questions
3
questions
3
votes
0
answers
52
views
Bounding Volume Proof Assistant Library
I am interested in learning Lean/Coq/Isabelle etc. and wanted to try to formalize Joseph O'Rourke's Minimum Bounding Box Algorithm. I do not have much experience with proof assistant tools.
Is there a ...
- 31
5
votes
1
answer
169
views
Looking for an entry point in the universe of proof assistants and proof IDE's
This is my first question in this part of StackExchange.
What I would like to achieve is the following.
Suppose I want to study ( or give a course on ) basic Real Analysis, I want to 1) document the ...
- 151
57
votes
10
answers
9k
views
Proof assistants for beginners - a comparison
What is a good starting point to learn about proof assistants?
The answer will invariably depend on the area of interest: mathematics (and its areas, e.g. algebra,combinatorics, analysis, logic), CS - ...
- 711