Skip to main content
Proof Assistants Beta

Enlightened

 Enlightened
First to answer and accepted with score of 10 or more. This badge can be awarded multiple times.
Awarded 90 times.
What are "locales" in Isabelle?
Awarded Feb 23, 2022 at 18:42
Tools for checking the consistency of a type theory
Awarded Feb 23, 2022 at 18:42
What is the computational complexity of theorem proving?
Awarded Feb 23, 2022 at 5:27
Lean: problems with visually indistinguishable instances
Awarded Feb 21, 2022 at 18:10
Why is Isabelle usually not just Isabelle but Isabelle/<xyz>?
Awarded Feb 21, 2022 at 0:57
What difficulties are there in basing a proof assistant on the $\lambda\mu$-calculus and has any proof assistant tried?
Awarded Feb 20, 2022 at 19:50
In Lean, why is the exact tactic necessary when the goal is the same as a hypothesis?
Awarded Feb 20, 2022 at 16:22
What is the state of coinductive types and reasoning in Coq?
Awarded Feb 18, 2022 at 19:56
Are there automated theorem provers for constructive logics? What strategy do they use?
Awarded Feb 18, 2022 at 6:46
Extends vs including a typeclass argument
Awarded Feb 15, 2022 at 14:51
Are some proof assistants better suited for given areas of math than others?
Awarded Feb 15, 2022 at 12:15
Is there something special about weak head normal form used with proof assistants?
Awarded Feb 15, 2022 at 11:36
Proof review: Sum of nCk over antidiagonal = Fibonacci
Awarded Feb 15, 2022 at 3:52
What is the difference between judgmental equality, definitional equality, and equality types?
Awarded Feb 14, 2022 at 0:11
Bringing OOP features into proof assistants?
Awarded Feb 13, 2022 at 23:11
What are the main differences between Coq and Lean?
Awarded Feb 13, 2022 at 17:17
What is the difference between refl and rfl in Lean 3?
Awarded Feb 13, 2022 at 0:17
Tutorials for formalizing mathematical definitions/statements in Lean
Awarded Feb 12, 2022 at 12:36
Why did Agda give up cumulative universes?
Awarded Feb 12, 2022 at 11:40
Any proof assistant that allows imperative computation within the language itself?
Awarded Feb 11, 2022 at 11:03
Is internal parametricity useful in theorem proving?
Awarded Feb 11, 2022 at 9:10
What is the difference between `leanprover` and `leanprover-community` GitHub repositories?
Awarded Feb 11, 2022 at 7:32
Finding symbols in Lean
Awarded Feb 10, 2022 at 19:11
Is eta-equality provable in Coq?
Awarded Feb 10, 2022 at 16:07
How to run Agda?
Awarded Feb 10, 2022 at 3:06
What is a Proof Assistant?
Awarded Feb 10, 2022 at 3:06
Usage and Importance of Proof Assistants
Awarded Feb 9, 2022 at 21:28
In Lean, what do double curly brackets mean?
Awarded Feb 9, 2022 at 21:28
What was the 1st Proof Assistant?
Awarded Feb 9, 2022 at 21:28
What are some examples of proof assistants doing something useful?
Awarded Feb 9, 2022 at 21:28
1
2