Skip to main content
Proof Assistants Beta

Nice Question

 Nice Question
Question score of 10 or more. This badge can be awarded multiple times.
Awarded 205 times.
How do real-world proof assistants bind variables and check equality?
Awarded Jun 7 at 11:49
What are the differences between theorem, example, def, etc?
Awarded May 12 at 14:36
How does Metamath Zero handle CIC as in Lean or Coq?
Awarded May 1 at 23:41
Which proof assistant would you advise me to learn (in 2022) considering my interests?
Awarded Mar 29 at 16:33
Can you build W-types out of natural numbers predicatively?
Awarded Mar 10 at 23:05
can proof assistants reason about complexity of programs?
Awarded Mar 4 at 14:43
What are some good (bad) examples of "green slime"?
Awarded Mar 1 at 14:47
Type Checking Undecidable in Extensional Type Theory
Awarded Jan 17 at 18:50
How "generic" are "generic proof assistants"?
Awarded Nov 18, 2023 at 19:10
How does Prop relate to h-prop and double negation?
Awarded Sep 18, 2023 at 9:21
What is hereditary substitution and why should I use it?
Awarded Jul 13, 2023 at 16:26
Have ideas from programming helped us create new mathematical proofs?
Awarded Jul 6, 2023 at 23:33
Uses of first-class implicit function types
Awarded May 17, 2023 at 19:16
Universe inconsistency as an effect
Awarded Apr 27, 2023 at 0:51
Construction of inductive types "the hard way"
Awarded Mar 9, 2023 at 9:57
What are the complex induction patterns supported by Agda?
Awarded Feb 21, 2023 at 16:42
What is realignment and is it useful in non-univalent theories?
Awarded Feb 12, 2023 at 10:02
Counterexamples in Type Theory
Awarded Jan 1, 2023 at 7:11
Categorical semantics of Agda
Awarded Dec 12, 2022 at 4:43
Are eliminators useful in practice, or are they only useful in the metatheory?
Awarded Dec 11, 2022 at 8:40
Why are impredicative constructions used less in type theory than in material set theory?
Awarded Nov 12, 2022 at 5:56
Seven Trees in One, or How to formalize the Semiring of Types?
Awarded Nov 3, 2022 at 21:05
How can we formalize a game where each player is a program having access to opponent's code?
Awarded Nov 1, 2022 at 9:04
Given `A = B`, how to prove `a: A` also has type B in Lean 4
Awarded Sep 23, 2022 at 1:06
Representing $\Bbb RP^2$ in Lean: building a type representing a particular set
Awarded Sep 22, 2022 at 11:15
Can the language of proof assistants be used for general purpose programming?
Awarded Sep 11, 2022 at 11:17
Learning materials for doing analysis (calculus) in a mechanized way
Awarded Aug 23, 2022 at 19:00
Performance of de Bruijn indices?
Awarded Aug 16, 2022 at 5:15
Is there something special about weak head normal form used with proof assistants?
Awarded Aug 16, 2022 at 5:15
Is coercion to a higher universe injective?
Awarded Aug 8, 2022 at 5:22
Why not have `Prop : Set` in Coq?
Awarded Jun 29, 2022 at 19:55
Open source proof assistants for first order logic with equality and set theory
Awarded Jun 16, 2022 at 18:26
Can Lean simp arguments be ordered?
Awarded Jun 13, 2022 at 4:58
Reasoning with the definition of Standard ML
Awarded Jun 6, 2022 at 19:25
Normalization by evaluation for extensional type theories
Awarded May 24, 2022 at 17:45
Rewriting with context in nested expressions (congruence rules)
Awarded May 22, 2022 at 2:50
auto-generating the proof of infinitude of primes
Awarded May 21, 2022 at 17:26
Can a theorem prover reason about its own faulty hardware?
Awarded May 17, 2022 at 17:21
How do Coq's bidirectionality hints (`&`) affect type checking?
Awarded May 12, 2022 at 14:10
Explicit vs implicit universes in lean
Awarded May 11, 2022 at 21:19
Proof assistants or libraries in proof assistants for working with model theory
Awarded May 9, 2022 at 8:33
Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?
Awarded May 7, 2022 at 17:05
How to represent mathematical partial functions in a type-theory based proof assistant?
Awarded May 4, 2022 at 2:55
Is there a Mizar-like sublanguage for Coq?
Awarded May 2, 2022 at 23:04
Do you need a Hilbert style Epsilon operator for definitions in set theory?
Awarded May 1, 2022 at 3:43
How to extract the witness from exists in Coq in function notation/without destructing?
Awarded Apr 26, 2022 at 9:19
Any proof assistant that allows imperative computation within the language itself?
Awarded Apr 25, 2022 at 9:07
Is there an official recommendation for editors to input Lean unicode characters?
Awarded Apr 25, 2022 at 9:07
Unintentionally proven false theorem with type-in-type outside logic and foundations?
Awarded Apr 25, 2022 at 9:02
How to implement the type checking of `transp` in de Morgan cubical type theory?
Awarded Apr 25, 2022 at 8:31
Lean "nonempty" vs "inhabited"
Awarded Apr 22, 2022 at 22:18
Do any automated theorem provers have the ability to stop, save state, reboot computer, restore state, continue?
Awarded Apr 18, 2022 at 9:41
What are the differences between jsCoq and the versions of Coq that can be downloaded?
Awarded Apr 18, 2022 at 7:08
Examples of formalisation of abelian categories
Awarded Apr 12, 2022 at 17:56
Is there a proof assistant (or an embedding) for the (co)end calculus?
Awarded Apr 11, 2022 at 7:26
Proving uniqueness of an instance of an indexed inductive type
Awarded Apr 10, 2022 at 3:51
Replacing (strict) positivity with monotonicity on propositions
Awarded Apr 7, 2022 at 1:51
What is a commuting conversion and why are they problematic?
Awarded Apr 4, 2022 at 2:42
What did Coq 8.15 change about divmod?
Awarded Apr 2, 2022 at 22:45
What about dependent types is useful for theorem provers?
Awarded Apr 2, 2022 at 22:45
1
2 3 4