Skip to main content
56 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 ...
Kevin Buzzard's user avatar
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 &...
Namdak Tönpa's user avatar
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 ...
Kevin Buzzard's user avatar
23 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 ...
gallais's user avatar
  • 1,126
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 ...
Alex Nelson's user avatar
  • 1,564
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 ...
Namdak Tönpa's user avatar
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 ...
Jason Rute's user avatar
  • 8,655
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 ...
Andrej Bauer's user avatar
  • 9,104
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 ...
Li-yao Xia's user avatar
  • 1,757
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 ...
Pierre-Marie Pédrot's user avatar
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 ...
Lawrence Paulson's user avatar
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 ...
Nike Dattani's user avatar
  • 1,165
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 ...
Greg Nisbet's user avatar
  • 2,761
9 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 ...
Alex J Best's user avatar
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.
Li-yao Xia's user avatar
  • 1,757
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 ...
Couchy's user avatar
  • 2,221
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: ...
Dan Doel's user avatar
  • 982
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....
Dima Pasechnik's user avatar
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 ...
Neel Krishnaswami's user avatar
5 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 ...
Ms. Molly Stewart-Gallus's user avatar
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: ...
Meven Lennon-Bertrand's user avatar
4 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 ...
djao's user avatar
  • 434
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 ...
ice1000's user avatar
  • 6,176
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. ...
Cheery's user avatar
  • 721
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 ...
Jason Gross's user avatar
  • 1,537
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 ...
Alex Nelson's user avatar
  • 1,564
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 ...
tinlyx's user avatar
  • 2,034
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 ...
Meven Lennon-Bertrand's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible