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.
Can I in Coq define a recursive function with a notation such that the recursive calls can use it?
Awarded Nov 20 at 21:46
Can we prove every provable statement with Lean?
Awarded Oct 23 at 18:46
What is a universe?
Awarded Oct 10 at 16:40
can proof assistants reason about complexity of programs?
Awarded Sep 25 at 23:15
What is a neutral term?
Awarded Jul 9 at 20:43
What are some useful resources for a mathematician interested in learning Isabelle/HOL?
Awarded Jun 18 at 16:09
Is ACL2 first-order-logic and is this a limitation for proving math?
Awarded Jun 13 at 20:26
Type Checking Undecidable in Extensional Type Theory
Awarded Jan 17 at 19:25
What are the differences between theorem, example, def, etc?
Awarded Dec 11, 2023 at 5:31
What is a deep embedding vs a shallow embedding? With examples?
Awarded Nov 26, 2023 at 16:41
Constructive proof of strong normalization for simply typed lambda calculus
Awarded Aug 28, 2023 at 6:56
Termination and confluence -- which goes first?
Awarded Aug 4, 2023 at 21:35
What is hereditary substitution and why should I use it?
Awarded Jul 13, 2023 at 16:26
auto-generating the proof of infinitude of primes
Awarded Jul 3, 2023 at 16:16
Is it possible to make a proof assistant program based on ZFC?
Awarded Jun 15, 2023 at 3:19
How to replace a function by its body
Awarded Jun 11, 2023 at 12:07
Construction of inductive types "the hard way"
Awarded Apr 7, 2023 at 21:18
What are the complex induction patterns supported by Agda?
Awarded Feb 21, 2023 at 14:57
Learning Math Proof via Proof Assistants
Awarded Nov 22, 2022 at 17:56
Can the language of proof assistants be used for general purpose programming?
Awarded Nov 22, 2022 at 17:56
Can you build W-types out of natural numbers predicatively?
Awarded Sep 2, 2022 at 12:25
What are "fibration/cofibration" in type theory and what are their intuitions?
Awarded Jul 16, 2022 at 10:41
Why not have `Prop : Set` in Coq?
Awarded Jun 27, 2022 at 20:26
What is the current state of proof assistants?
Awarded Jun 1, 2022 at 23:47
Does Lean have a standard ASCII representation?
Awarded May 12, 2022 at 0:01
In Lean, contradiction tactic failed but actually goal accomplished
Awarded May 7, 2022 at 17:30
Is there a Mizar-like sublanguage for Coq?
Awarded May 2, 2022 at 23:21
Do you need a Hilbert style Epsilon operator for definitions in set theory?
Awarded May 1, 2022 at 20:57
What axioms do I need to search the naturals?
Awarded Apr 26, 2022 at 23:05
Lean "nonempty" vs "inhabited"
Awarded Apr 17, 2022 at 21:05
What set-theoretic definitions can't easily be formalized in a type theory?
Awarded Apr 14, 2022 at 17:35
What are the advantages of normalization by evaluation over traditional reduction-based normalization?
Awarded Apr 4, 2022 at 8:47
What are the possible kinds of type theories or logics with quotients?
Awarded Apr 2, 2022 at 13:15
What is the role of impredicativity in program extraction?
Awarded Apr 2, 2022 at 0:05
Has anyone ever accidentally "proven" a false theorem with type-in-type?
Awarded Mar 31, 2022 at 21:46
WLOG reasoning and Proof Assistants
Awarded Mar 30, 2022 at 16:33
Are there any proof assistants or theorem provers based on the method of analytic tableaux?
Awarded Mar 30, 2022 at 16:33
What subtyping rules does Agda support?
Awarded Mar 30, 2022 at 3:40
How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?
Awarded Mar 29, 2022 at 20:46
What work has been done on computationally intensive proofs?
Awarded Mar 27, 2022 at 14:01
What axioms have a computational interpretation?
Awarded Mar 25, 2022 at 16:27
Why should you "never resort to polymorphism when initiality would do"?
Awarded Mar 25, 2022 at 16:27
Proof assistants and formalised mathematics in the MSC database
Awarded Mar 18, 2022 at 20:10
What does the "motive is not type correct" error mean in Lean?
Awarded Mar 18, 2022 at 13:09
In Agda, why is universe polymorphism explicit?
Awarded Mar 17, 2022 at 3:04
So many data types, so little time
Awarded Mar 15, 2022 at 18:50
Can mathematical formalizations in NuPRL be trusted as correct in the greater mathematical practice?
Awarded Mar 14, 2022 at 14:40
Does the canonicity of natural number imply that of all types?
Awarded Mar 13, 2022 at 15:25
Easy ways to introduce inductive types
Awarded Mar 11, 2022 at 18:27
When should I use De Bruijn levels instead of indices?
Awarded Mar 10, 2022 at 2:41
Incorporating Markov's principle in various proof assistants
Awarded Mar 9, 2022 at 13:11
What did Coq 8.15 change about divmod?
Awarded Mar 8, 2022 at 14:20
What are well-founded inductive types?
Awarded Mar 7, 2022 at 11:25
What is realignment and is it useful in non-univalent theories?
Awarded Mar 4, 2022 at 23:25
Is there a proof assistant for Peano Arithmetic?
Awarded Mar 4, 2022 at 20:41
Representing $\Bbb RP^2$ in Lean: building a type representing a particular set
Awarded Mar 4, 2022 at 20:41
What is an algebraic data type?
Awarded Feb 28, 2022 at 19:27
Which programming languages are most similar to proof assistants?
Awarded Feb 26, 2022 at 14:45
What's the "Hello, World!" for proof assistants?
Awarded Feb 26, 2022 at 14:45
What is Artin gluing, and how is it useful in proving meta-theoretic properties?
Awarded Feb 23, 2022 at 18:42
1
2