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.
What is the role of impredicativity in program extraction?
Awarded Apr 2, 2022 at 1:36
What's "predicative" about pC(u)IC?
Awarded Apr 1, 2022 at 9:41
Has anyone ever accidentally "proven" a false theorem with type-in-type?
Awarded Mar 31, 2022 at 19:42
Proof assistants with dynamic scope/local instances/etc.?
Awarded Mar 31, 2022 at 7:57
Proof-theoretic comparison table?
Awarded Mar 30, 2022 at 9:42
How to speed up Lean?
Awarded Mar 30, 2022 at 2:32
Naming conventions (letter case, underscores, &c) for Coq
Awarded Mar 29, 2022 at 13:09
What's "Swedish" style of doing type theory or proof assistants?
Awarded Mar 28, 2022 at 22:06
Constructive proof of strong normalization for simply typed lambda calculus
Awarded Mar 28, 2022 at 21:11
How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?
Awarded Mar 28, 2022 at 18:20
Incorporating Markov's principle in various proof assistants
Awarded Mar 27, 2022 at 6:48
What work has been done on computationally intensive proofs?
Awarded Mar 26, 2022 at 12:20
Is there any example of a dependent product that makes sense in a non-type-theory context?
Awarded Mar 25, 2022 at 15:25
How does the formal proof of the four color theorem work?
Awarded Mar 25, 2022 at 13:30
Why should you "never resort to polymorphism when initiality would do"?
Awarded Mar 25, 2022 at 7:41
What are the practical differences between intensional and extensional type theories?
Awarded Mar 23, 2022 at 14:41
Formalizations of unsolved problems
Awarded Mar 23, 2022 at 10:40
How usable is Lean for constructive mathematics?
Awarded Mar 22, 2022 at 13:36
Algorithms obtained through constructive formalization
Awarded Mar 21, 2022 at 22:34
What's the difference between reflection and tactics?
Awarded Mar 21, 2022 at 8:27
What is bidirectional type checking?
Awarded Mar 19, 2022 at 23:42
What are the motivations for different variants of categorical models of dependent type?
Awarded Mar 19, 2022 at 4:21
Well-foundedness: classical equivalence of no infinite descent and accessibility
Awarded Mar 18, 2022 at 18:06
How much duplication does universe polymorphism actually save us?
Awarded Mar 18, 2022 at 15:06
What are "fibration/cofibration" in type theory and what are their intuitions?
Awarded Mar 18, 2022 at 8:45
Proof assistants and formalised mathematics in the MSC database
Awarded Mar 17, 2022 at 18:19
Tutorial implementations of NbE
Awarded Mar 17, 2022 at 15:42
Easy ways to introduce inductive types
Awarded Mar 17, 2022 at 8:12
What does the "motive is not type correct" error mean in Lean?
Awarded Mar 17, 2022 at 7:47
In Agda, why is universe polymorphism explicit?
Awarded Mar 15, 2022 at 16:25
Does the canonicity of natural number imply that of all types?
Awarded Mar 14, 2022 at 22:26
Ergonomic use of multicategories in proof assistants
Awarded Mar 13, 2022 at 20:27
What are the advantages to impredicativity?
Awarded Mar 13, 2022 at 15:20
So many data types, so little time
Awarded Mar 12, 2022 at 21:25
Rules for mutual inductive/coinductive types
Awarded Mar 12, 2022 at 15:40
What axioms have a computational interpretation?
Awarded Mar 12, 2022 at 1:50
Can mathematical formalizations in NuPRL be trusted as correct in the greater mathematical practice?
Awarded Mar 11, 2022 at 9:25
Is there computational interpretation for countable choice?
Awarded Mar 11, 2022 at 3:17
Does Lean have a standard ASCII representation?
Awarded Mar 8, 2022 at 8:30
What is the trade-off to accepting impredicative propositions?
Awarded Mar 7, 2022 at 17:55
What is a universe?
Awarded Mar 7, 2022 at 17:55
When should I use De Bruijn levels instead of indices?
Awarded Mar 7, 2022 at 17:42
Why does it matter if canonicity holds for irrelevant types?
Awarded Mar 7, 2022 at 17:07
Is induction over mutually inductive coinductive types possible?
Awarded Mar 7, 2022 at 9:51
Are there proof assistants for multi-valued logics?
Awarded Mar 6, 2022 at 4:10
Expressivity of mutual/nested inductives vs. regular inductives
Awarded Mar 5, 2022 at 4:15
Converting between formulations of reals in Coq
Awarded Mar 4, 2022 at 17:01
To what extent is formalized mathematics publishable?
Awarded Mar 4, 2022 at 16:16
Why did Agda give up cumulative universes?
Awarded Mar 3, 2022 at 21:56
Exotic natural language summaries of formal proofs
Awarded Mar 3, 2022 at 16:57
What is known about the consistency of proof assistant metatheories?
Awarded Mar 2, 2022 at 21:42
What are well-founded inductive types?
Awarded Mar 2, 2022 at 17:56
What exactly is setoid hell?
Awarded Mar 1, 2022 at 13:06
What is an algebraic data type?
Awarded Feb 28, 2022 at 13:41
Tools for checking the consistency of a type theory
Awarded Feb 25, 2022 at 16:15
WLOG reasoning and Proof Assistants
Awarded Feb 25, 2022 at 11:57
In what intensional type theories can absurdity be made definitionally proof irrelevant?
Awarded Feb 24, 2022 at 16:18
Are Logics Based on Dependent Types Stronger Than Ones Without?
Awarded Feb 23, 2022 at 21:46
Integration of proof assistants and Wikipedia-like websites?
Awarded Feb 23, 2022 at 16:16
What games are there?
Awarded Feb 21, 2022 at 19:35
1
2
3 4