Skip to main content
Proof Assistants Beta

Nice Answer

 Nice Answer
Answer score of 10 or more. This badge can be awarded multiple times.

earned this badge 29 times.
Given `A = B`, how to prove `a: A` also has type B in Lean 4
Awarded Apr 21 at 10:55
What is a deep embedding vs a shallow embedding? With examples?
Awarded Nov 26, 2023 at 16:34
Have ideas from programming helped us create new mathematical proofs?
Awarded Jul 6, 2023 at 13:21
Open source proof assistants for first order logic with equality and set theory
Awarded Jun 16, 2022 at 18:26
Do you need a Hilbert style Epsilon operator for definitions in set theory?
Awarded May 1, 2022 at 15:51
How to extract the witness from exists in Coq in function notation/without destructing?
Awarded Apr 25, 2022 at 19:25
What is the role of impredicativity in program extraction?
Awarded Apr 1, 2022 at 7:17
Formalizations of unsolved problems
Awarded Mar 31, 2022 at 19:03
What work has been done on computationally intensive proofs?
Awarded Mar 27, 2022 at 10:49
What's the difference between reflection and tactics?
Awarded Mar 21, 2022 at 8:27
Can mathematical formalizations in NuPRL be trusted as correct in the greater mathematical practice?
Awarded Mar 14, 2022 at 14:16
What is known about the consistency of proof assistant metatheories?
Awarded Mar 5, 2022 at 13:55
Can the development of proof assistants make mathematicians switch their framework?
Awarded Feb 28, 2022 at 23:15
What is an algebraic data type?
Awarded Feb 28, 2022 at 15:11
What's “conservativity” in terms of type theory and how is it useful?
Awarded Feb 27, 2022 at 22:26
Tools for checking the consistency of a type theory
Awarded Feb 23, 2022 at 15:26
What are the pros and cons of continuous checking over keychord-triggered checking?
Awarded Feb 21, 2022 at 20:17
Why is cumulativity not a given in proof assistants?
Awarded Feb 20, 2022 at 15:56
How to use a proof assistant to reason in a topos?
Awarded Feb 14, 2022 at 18:33
Impact of "Formalizing 100 Theorems" and what is next
Awarded Feb 13, 2022 at 10:11
Can theorem provers be used to form foundations for programming languages?
Awarded Feb 12, 2022 at 10:00
What is predicativity?
Awarded Feb 11, 2022 at 18:17
What set-theoretic definitions can't easily be formalized in a type theory?
Awarded Feb 10, 2022 at 0:17
How to run Agda?
Awarded Feb 9, 2022 at 23:51
Proof Assistants with support for creating executable software artifacts
Awarded Feb 9, 2022 at 23:51
Where can I find lists of theorems that have been verified?
Awarded Feb 9, 2022 at 22:11
In Lean, what do double curly brackets mean?
Awarded Feb 9, 2022 at 20:34
Non-trivial difference(s) between Computer Algebra System and Proof Assistant
Awarded Feb 9, 2022 at 20:34
How can I prove facts about floating point calculations?
Awarded Feb 9, 2022 at 20:34

Others with this badge