Questions tagged [usage]
Questions asking how to properly and efficiently use Proof Assistants.
15
questions
11
votes
0
answers
129
views
What are the practical differences between intensional and extensional type theories?
It is already proved that MLTT with equality reflection is equivalent to MLTT with an intensional equality, plus UIP and function extensionality. So theoretically the differences between intensional ...
- 2,246
10
votes
1
answer
167
views
How much duplication does universe polymorphism actually save us?
From my rough impression, in (formalizing) everyday mathematics we almost never use universe polymorphism in a way that stretches the proof-theoretic strength. It merely saves us some duplication.
My ...
- 2,246
11
votes
1
answer
227
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 ...
- 2,246
14
votes
1
answer
255
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.
...
- 893
2
votes
1
answer
123
views
Defining Lists and Prove Associativity of Append [closed]
When I saw this question asking what is the "Hello, World!" for proof assistants I immediately thought of that exercise. Not a long time after this answer by Couchy was proposed.
Therefore, ...
- 898
5
votes
1
answer
59
views
General Guidelines and Tips for using Induction
There are many kinds of induction (induction over the natural numbers ⊂ structural induction ⊂ Noetherian induction), when do I use which flavour? And what should I keep in mind when doing proofs by ...
- 898
0
votes
1
answer
194
views
Can we use Proof Assistants beyond mathematics? [closed]
After receiving responses from this question as a Liberal Artist I'm interesting in other Proof Assistant appliances, beyond Mathematics and Software Verification. I was wondering: how one can use ...
- 1,182
24
votes
3
answers
242
views
Examples of new mathematics discovered through formalization?
In his essay Why formalize mathematics?, Patrick Massot discusses several reasons behind why a working mathematician might be interested in proof formalization. One of the the reasons he discusses is, ...
39
votes
2
answers
708
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 ...
- 928
14
votes
3
answers
213
views
Proof Assistants for Vim Users
I remember the last time I was trying to get into proof assistants, I was discouraged by the lack of functionality for vim users. At the time, it seemed like a lot of powerful features (holes, etc) ...
- 257
6
votes
2
answers
207
views
How to run Agda?
I want to run Agda, but I do not know how to run functions. I need to run "Hello, World!"; how can I do this?
- 227
19
votes
2
answers
200
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?
- 1,182
15
votes
3
answers
339
views
What is a Proof Assistant?
How would you explain to a beginner in simple terms, what a Proof Assistant is?
- 1,182
25
votes
3
answers
597
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?
- 1,182
9
votes
3
answers
282
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 ...
- 637