All Questions
1,062
questions
65
votes
2
answers
7k
views
What are the main differences between Coq and Lean?
Coq and Lean are two of the most common proof assistants out there (but the question of course applies to other proof assistants too).
What are the main differences between Coq and Lean? Ideally it ...
- 988
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
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 ...
- 1,058
44
votes
9
answers
2k
views
What's the "Hello, World!" for proof assistants?
Many programming language tutorials start with a simple program which just outputs "Hello, World!" to the console or another output. For the various proof assistants, is there some widely-...
- 731
41
votes
3
answers
3k
views
What exactly is setoid hell?
One of the only arguments I've heard about why Lean is better than Coq is that you can construct quotients of built-in structures by default. (In Coq, you apparently have to use Setoids instead of ...
- 511
38
votes
3
answers
1k
views
What is predicativity?
Type systems, and the proof assistants based on them, are frequently divided into predicative and impredicative.
What exactly does this mean? I've heard the slogan "impredicativity means you can'...
- 3,073
32
votes
3
answers
1k
views
What are the bases for different Proof Assistants?
From the Wikipedia article on Proof Assistant it shows some Proof Assistants are based on Higher Order Logic, (HOL Light) and some are based on Dependent Types, (Coq).
Are there any other means upon ...
- 2,846
32
votes
1
answer
1k
views
What will happen to mathlib when we transition to Lean 4?
Today, there's an exciting large-scale effort to digitize mathematics in Lean's mathematics library mathlib.
I understand that a transition to Lean 4 is looming. I'...
- 981
32
votes
2
answers
2k
views
What work has been done on computationally intensive proofs?
Fifty years ago, few would have imagined that the process of verifying the correctness of a known proof of a mathematical theorem might be so costly that the mathematical community would hesitate to ...
- 505
32
votes
3
answers
1k
views
How to search for an existing theorem in Lean?
When proving things in a theorem prover, I am often using sizable libraries that I don’t know by heart, so it is crucial to be effective in discovering existing theorems.
What are the best approaches ...
- 1,904
31
votes
2
answers
4k
views
Has anyone ever accidentally "proven" a false theorem with type-in-type?
It is possible (with some cleverness) to prove false from type-in-type. For instance, Girard proved false in Martin Lof's original system (as described in the introduction of An Intuitionistic Theory ...
- 443
30
votes
1
answer
704
views
In Lean, what do double curly brackets mean?
In Lean, explicit function arguments are enclosed in round brackets and implicit ones in curly brackets, as in this example:
...
- 1,051
29
votes
1
answer
1k
views
What is an algebraic data type?
When I first learned Haskell, I was told that you use data keyword to define an "algebraic data type", or a "sum type". Then I learned the idea ...
- 6,306
28
votes
2
answers
1k
views
Is there software for interfacing Lean code with LaTeX?
The Natural Number Game suggests the possibility of rewriting mathematics textbooks with embedded interactive Lean code. I'm envisioning something like Google Colab or Mathematica, where you can ...
- 413
27
votes
8
answers
942
views
Where can I find lists of theorems that have been verified?
I recall many years ago seeing a very large and well-interlinked (by computer) list of verified results starting from base assumptions and leading to all sorts of things that naive me did not expect ...