Skip to main content

Questions tagged [usage]

Questions asking how to properly and efficiently use Proof Assistants.

Filter by
Sorted by
Tagged with
46 votes
2 answers
2k views

Are some proof assistants better suited for given areas of math than others?

There are many different proof assistants out there, and I think it is reasonable to expect that more or less all results we prove in everyday mathematics can be proven in any of them. One nice way to ...
Wojowu's user avatar
  • 1,058
18 votes
3 answers
1k views

What is a Proof Assistant?

How would you explain to a beginner in simple terms, what a Proof Assistant is?
taylor.2317's user avatar
  • 1,318
13 votes
1 answer
406 views

Incorporating Markov's principle in various proof assistants

The Markov's principle states that if a Turing machine does not run forever, then it halts. Equivalently, if I have a function $f : \mathbb N \to \mathrm{Bool}$, such that I have proved that $\neg\neg ...
Trebor's user avatar
  • 3,967
25 votes
3 answers
866 views

What was the 1st Proof Assistant?

What was the first proof assistant? What was it used for? When and by who was it created? Is it still used today? And what was its purpose?
taylor.2317's user avatar
  • 1,318
19 votes
2 answers
483 views

Usage and Importance of Proof Assistants

How would you explain so a beginner in simple terms why Proof Assistants are important, and how / why they are used?
taylor.2317's user avatar
  • 1,318
15 votes
1 answer
373 views

Why should you "never resort to polymorphism when initiality would do"?

In the concluding statement of "universe hierarchies", Conor McBride calls it [...] that key lesson which I learned from James McKinna: never resort to polymorphism when initiality will do. ...
James Martin's user avatar
  • 1,025
9 votes
3 answers
392 views

Could proof assistants be used to prove that some piece of code is free of bugs?

Formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of ...
Glorfindel's user avatar