Skip to main content
Proof Assistants Beta

Popular Question

 Popular Question
Question with 1,000 views. This badge can be awarded multiple times.
Awarded 65 times.
Tools like leanblueprint for other proof assistants, especially Coq?
Awarded Sep 10 at 9:20
Where can I find lists of theorems that have been verified?
Awarded Sep 5 at 10:22
What is a deep embedding vs a shallow embedding? With examples?
Awarded Aug 15 at 9:47
Learning Math Proof via Proof Assistants
Awarded Aug 14 at 8:20
Using the contrapositive in lean 4
Awarded Aug 8 at 8:05
In Lean, contradiction tactic failed but actually goal accomplished
Awarded Aug 6 at 17:57
How to run Agda?
Awarded Jul 12 at 3:20
Where is the syntax of Lean 4 documented?
Awarded Jul 10 at 16:52
Getting an element of a list in Lean
Awarded Jul 2 at 5:41
What does the "motive is not type correct" error mean in Lean?
Awarded Jul 1 at 11:19
Less ridiculous way to prove that an Ascii character compares equal with itself in Coq
Awarded Jun 28 at 5:03
What is the state of coinductive types and reasoning in Coq?
Awarded Jun 27 at 6:48
Is there a way to automatically translate proofs from one proof assistant to another?
Awarded Jun 20 at 20:55
How do real-world proof assistants bind variables and check equality?
Awarded Jun 4 at 18:15
How to run the main function in lean 4?
Awarded May 27 at 14:55
A project in Lean which involves "programming"
Awarded May 3 at 23:47
How do I express a negative premise in Coq?
Awarded Apr 29 at 19:06
What is a Proof Assistant?
Awarded Apr 24 at 18:25
Is there software for interfacing Lean code with LaTeX?
Awarded Apr 15 at 15:20
What are the complex induction patterns supported by Agda?
Awarded Apr 12 at 22:46
How to prove non-existence of terms that contain themselves in Coq
Awarded Mar 24 at 16:37
How to search for an existing theorem in Lean?
Awarded Feb 29 at 16:46
Lean 4 Importing into VSCode
Awarded Feb 27 at 17:28
Doing case-by-case proofs about match statements in Lean4
Awarded Feb 22 at 18:56
In Lean, why is it possible to prove $\text{succ}\; x \neq 0$ without adding it as an axiom?
Awarded Feb 19 at 19:35
Well-foundedness: classical equivalence of no infinite descent and accessibility
Awarded Feb 19 at 0:08
Why not have `Prop : Set` in Coq?
Awarded Feb 9 at 19:56
What are "fibration/cofibration" in type theory and what are their intuitions?
Awarded Jan 29 at 15:48
What set-theoretic definitions can't easily be formalized in a type theory?
Awarded Jan 20 at 15:15
Do you need a Hilbert style Epsilon operator for definitions in set theory?
Awarded Jan 1 at 21:06
Make ChatGPT write formal proof from natural language proof
Awarded Dec 18, 2023 at 23:07
Using proof assistants to generate fast code
Awarded Dec 7, 2023 at 7:31
What is predicativity?
Awarded Nov 26, 2023 at 13:08
What are the differences between MLTT and CIC?
Awarded Nov 10, 2023 at 19:50
When should I use De Bruijn levels instead of indices?
Awarded Nov 1, 2023 at 22:30
Can the language of proof assistants be used for general purpose programming?
Awarded Oct 27, 2023 at 22:57
Proof-theoretic comparison table?
Awarded Oct 24, 2023 at 7:52
What will happen to mathlib when we transition to Lean 4?
Awarded Oct 2, 2023 at 15:08
Can we prove every provable statement with Lean?
Awarded Aug 17, 2023 at 14:25
Constructive proof of strong normalization for simply typed lambda calculus
Awarded Jul 15, 2023 at 15:51
What is an algebraic data type?
Awarded Jul 6, 2023 at 10:49
Have ideas from programming helped us create new mathematical proofs?
Awarded Jul 6, 2023 at 10:06
How to extract the witness from exists in Coq in function notation/without destructing?
Awarded Jun 29, 2023 at 2:01
Is it possible to make a proof assistant program based on ZFC?
Awarded Jun 13, 2023 at 23:42
How do I install Lean 4?
Awarded Jun 5, 2023 at 20:33
What's the difference between reflection and tactics?
Awarded May 15, 2023 at 0:20
How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?
Awarded Mar 29, 2023 at 16:53
What are the bases for different Proof Assistants?
Awarded Feb 8, 2023 at 5:07
Is there any example of a dependent product that makes sense in a non-type-theory context?
Awarded Feb 1, 2023 at 23:45
What exactly is setoid hell?
Awarded Jan 26, 2023 at 2:09
Are some proof assistants better suited for given areas of math than others?
Awarded Jan 18, 2023 at 4:40
What's the "Hello, World!" for proof assistants?
Awarded Nov 22, 2022 at 16:04
Why are these two proofs so different?
Awarded Nov 17, 2022 at 2:41
Are there computable functions which can't be expressed in Lean?
Awarded Nov 15, 2022 at 20:07
How usable is Lean for constructive mathematics?
Awarded Oct 21, 2022 at 12:40
How can we formalize a game where each player is a program having access to opponent's code?
Awarded Oct 12, 2022 at 10:57
What is bidirectional type checking?
Awarded Aug 9, 2022 at 19:42
What are the main differences between Coq and Lean?
Awarded Jul 6, 2022 at 22:04
Proof assistants for beginners - a comparison
Awarded Jul 5, 2022 at 22:12
Open source proof assistants for first order logic with equality and set theory
Awarded Jun 17, 2022 at 1:46
1
2