57
votes
Accepted
Are some proof assistants better suited for given areas of math than others?
I think that to a large extent this is an open problem, and I think that one reason it's still open is that not enough people are working on it. I would love to see some change here but right now I ...
- 2,520
28
votes
What was the 1st Proof Assistant?
The first (1968) fibrational proof assistant for computers is known to be AUTOMATH prover which was implemented under the lead of Nicolaas Govert de Bruijn (AUT-68). It's the direct ancestor of the &...
- 1,297
26
votes
Accepted
Usage and Importance of Proof Assistants
In mathematics, I believe they're important for the following reasons:
They might change the way we teach. There are plenty of computer tools for teaching at school level but a proof assistant offers ...
- 2,520
24
votes
Accepted
Why should you "never resort to polymorphism when initiality would do"?
Initiality comes with a powerful universal property which allows you to, internally, prove statements about the constructions you perform. If you give me an element of ...
- 1,264
23
votes
Accepted
What was the 1st Proof Assistant?
Arguably, the first theorem prover was the Logic Theorist, developed by a team at RAND back in the 1950s, which was used to generate alternate proofs for parts of Russell and Whitehead's Principia.
If ...
- 1,574
19
votes
What is a Proof Assistant?
Let us clarify some jargon. Usually we call proof assistants systems which can really help us finding proofs, i.e. they should have a tactic language. Systems which lack this feature (tactics) are ...
- 1,297
19
votes
Examples of new mathematics discovered through formalization?
One quite concrete example of this is discussed by Massot in the essay linked in the original post. During the work on the Liquid Tensor Experiment (formalizing the proof of a theorem due to Scholze ...
19
votes
Usage and Importance of Proof Assistants
(A lightly edited copy and paste of my answer to a similar question on the Lean Zulip chat: What is the point of Lean's maths library.)
In my talk about Lean-GPT-f at Harvard, I gave five different ...
- 9,663
18
votes
Accepted
How to run Agda?
Given that you arrived here "having no idea" how to run it, the easiest might be:
Install Visual Studio Code
Install banacorn.agda-mode package in Visual ...
- 10.1k
18
votes
Accepted
Could proof assistants be used to prove that some piece of code is free of bugs?
An important point to clarify is the meaning of "free of bugs". Correctness only makes sense relative to a specification. Only once you have decided what property you care about (your ...
- 2,087
16
votes
Accepted
Incorporating Markov's principle in various proof assistants
There are different ways to implement Markov's principle, and they're not equivalent. I know of at least three techniques to implement MP.
MP as a loop
I personally find this to be a hack inherited ...
- 2,353
13
votes
What was the 1st Proof Assistant?
I regard "proof assistant" as synonymous with "interactive theorem prover", which rules out many of the systems mentioned in other answers. For example, the input to AUTOMATH was a ...
- 806
11
votes
What is a Proof Assistant?
The term "proof assistant" is usually used to describe a computer software that assists humans with developing formal proofs. A formal proof is a finite sequence of declarative sentences ...
- 1,175
10
votes
Could proof assistants be used to prove that some piece of code is free of bugs?
Sort of. Bugs are a nebulous concept, so it's difficult to prove their absence. Theorem provers can show that certain components of a software program are behaving exactly as specified, so bugs must ...
- 3,105
10
votes
Proof Assistants for Vim Users
Neovim support in Lean has come a long way recently: The Neovim plugin (by Julian Berman, Rishikesh Vaishnav and Gabriel Ebner predominantly) supports both Lean 3 and Lean 4 and supports both ...
- 635
8
votes
Proof Assistants for Vim Users
Coq has the Coqtail plugin for vim and neovim. It doesn't have all the bells and whistles of Proof General but the classic 3-pane UI is all I really need to be productive.
- 2,087
7
votes
Accepted
What are some good (bad) examples of "green slime"?
If all you want is a very simple example, it's pretty easy to build one. Here's one simplified from a question on the Agda zulip:
...
- 982
7
votes
Accepted
What is a Proof Assistant?
A proof assistant is a system that translates user input into a formal proof. Ideally, this formal proof should be verifiable by a third party.
For example,
the user designates a theorem they would ...
- 2,320
6
votes
Are some proof assistants better suited for given areas of math than others?
I don't think most theorem provers are very different from each other. In my opinion most provers are based around classical logic, intuitionistic logic or possibly linear logic.
Many theorem provers ...
- 2,868
6
votes
Accepted
Can we use Proof Assistants beyond mathematics?
They are used a lot in software development,to verify correctness of implementations, and even to generate executable code (this is called program extraction). See https://softwarefoundations.cis....
- 480
6
votes
Examples of new mathematics discovered through formalization?
As David Roberts mentioned in a comment, this happens relatively frequently in the field of homotopy type theory / univalent foundations. Often in that area (at least, in my experience), a proof-...
6
votes
Why is it hard to formalize informal proofs?
Are there any theoretical obstacles in formalizing what we actually do when we mentally verify equations, etc?
Yes: we don't know what we actually do when we mentally verify equations!
This is a glib ...
- 2,053
5
votes
Accepted
How to install dependencies correctly? [Cannot find a physical path bound to logical path]
If you use opam, it should just be as simple as
git clone https://github.com/jwiegley/category-theory
cd category-theory
opam install .
Once complete, add ...
- 619
4
votes
Accepted
Universe polymorphism and modules in Coq
If you go polymorphic, you should probably go all the way, and also use a polymorphic product type, like so:
...
- 5,645
3
votes
Accepted
How much duplication does universe polymorphism actually save us?
I don't have a statistical conclusion (I wish this question is still answerable without statistical analysis :D), but my impression on universe levels is that we usually use up to 2 different levels ...
- 6,346
3
votes
Defining Lists and Prove Associativity of Append
Here's a little list module written in Adga. To do this we are going to need cong -rule, and it resides in PropositionalEquality -module.
...
- 731
3
votes
General Guidelines and Tips for using Induction
The best guideline is: If you don't know how to do the proof on pen-and-paper, you probably will get lost doing it in a proof assistant. If you don't know what your induction hypothesis is supposed ...
- 1,547
3
votes
Could proof assistants be used to prove that some piece of code is free of bugs?
I don't mean to be a "doubting Thomas", but I've always been under the impression that proof assistants check the code implements the specification and can verify the specification satisfies ...
- 1,574
3
votes
How to run Agda?
One possibility is to use Emacs. Quoting the book Programming Language Foundations in Agda:
Agda ships with the editor support for Emacs built-in, so if you’ve
installed Agda, all you have to do to ...
- 2,320
3
votes
Accepted
Universe polymorphism and Coq standard library
Sadly, at the moment, there are no standard-ish libraries using universe polymorphism. A similar question arose some time ago and the Coq Zulip, and it seems multiple people from multiple projects ...
- 5,645
Only top scored, non community-wiki answers of a minimum length are eligible