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.
In Lean, why is the exact tactic necessary when the goal is the same as a hypothesis?
Awarded Feb 21, 2022 at 11:51
What are the upsides and downsides of typed vs untyped conversion?
Awarded Feb 20, 2022 at 15:41
What mathematical topics should I learn first before I start using proof assistants?
Awarded Feb 20, 2022 at 13:58
Lean: problems with visually indistinguishable instances
Awarded Feb 20, 2022 at 12:33
PDEs and proof assistants
Awarded Feb 20, 2022 at 0:50
Why is cumulativity not a given in proof assistants?
Awarded Feb 19, 2022 at 23:03
How do I turn off the aggressive auto-indent in Proof General/Coq
Awarded Feb 17, 2022 at 19:04
Why is Isabelle usually not just Isabelle but Isabelle/<xyz>?
Awarded Feb 17, 2022 at 16:56
Could proof assistants be used to prove that some piece of code is free of bugs?
Awarded Feb 17, 2022 at 16:43
Programming language metatheory in Lean 4?
Awarded Feb 17, 2022 at 3:30
How hard is computing integrals in Lean?
Awarded Feb 16, 2022 at 19:17
Tools to check correctness of decimal floating point arithmetic
Awarded Feb 16, 2022 at 7:08
verifying combinatorial constructions - choice of a proof assistant
Awarded Feb 16, 2022 at 3:52
What is the state of coinductive types and reasoning in Coq?
Awarded Feb 15, 2022 at 21:33
What is known about performance bottlenecks in proof assistants?
Awarded Feb 15, 2022 at 19:35
Extends vs including a typeclass argument
Awarded Feb 15, 2022 at 13:21
What are the possible kinds of type theories or logics with quotients?
Awarded Feb 15, 2022 at 8:12
What difficulties are there in basing a proof assistant on the $\lambda\mu$-calculus and has any proof assistant tried?
Awarded Feb 15, 2022 at 3:03
Bringing OOP features into proof assistants?
Awarded Feb 14, 2022 at 17:48
Proof review: Sum of nCk over antidiagonal = Fibonacci
Awarded Feb 14, 2022 at 14:45
Proof Assistants with support for creating executable software artifacts
Awarded Feb 14, 2022 at 12:04
What is the difference between refl and rfl in Lean 3?
Awarded Feb 13, 2022 at 21:55
How to use a proof assistant to reason in a topos?
Awarded Feb 13, 2022 at 17:17
Attempts to accommodate theories of different consistency strength in single assistant
Awarded Feb 13, 2022 at 12:47
Impact of "Formalizing 100 Theorems" and what is next
Awarded Feb 13, 2022 at 11:42
How to deal with Binders?
Awarded Feb 13, 2022 at 9:57
Why does apply_instance fail to generate decidable_pred here?
Awarded Feb 12, 2022 at 13:25
How to search for an existing theorem in Lean?
Awarded Feb 12, 2022 at 12:51
What is the state of recompilation avoidance in proof assistants?
Awarded Feb 12, 2022 at 11:49
In the "Simply Easy!" paper, why is it safe to evaluate types in the empty environment?
Awarded Feb 12, 2022 at 10:00
Code generation from Locales and Sublocales in Isabelle
Awarded Feb 12, 2022 at 8:10
What is in an olean file?
Awarded Feb 11, 2022 at 23:48
How can I prove facts about floating point calculations?
Awarded Feb 11, 2022 at 23:48
Are there automated theorem provers for constructive logics? What strategy do they use?
Awarded Feb 11, 2022 at 22:31
Proof assistants for forward reasoning?
Awarded Feb 11, 2022 at 17:40
Is there a proof assistant for Peano Arithmetic?
Awarded Feb 11, 2022 at 10:34
Tutorials for formalizing mathematical definitions/statements in Lean
Awarded Feb 11, 2022 at 9:18
What is predicativity?
Awarded Feb 11, 2022 at 8:51
Are there any proof assistants which integrate JITs?
Awarded Feb 11, 2022 at 8:20
Is eta-equality provable in Coq?
Awarded Feb 11, 2022 at 7:05
Successes of machine learning in formal theorem proving
Awarded Feb 11, 2022 at 6:25
Has there been any attempt at a tutorial that doesn't start with natural numbers?
Awarded Feb 11, 2022 at 0:45
Have any proof assistants incorporated a notion of unsafety with Type : Type?
Awarded Feb 11, 2022 at 0:35
Finding symbols in Lean
Awarded Feb 10, 2022 at 20:56
What are good books for learning about proof assistants for Functional Analysis?
Awarded Feb 10, 2022 at 19:36
What will happen to mathlib when we transition to Lean 4?
Awarded Feb 10, 2022 at 19:36
What are the differences between MLTT and CIC?
Awarded Feb 10, 2022 at 19:16
What is the difference between judgmental equality, definitional equality, and equality types?
Awarded Feb 10, 2022 at 18:11
What are the major formal mathematics libraries and how big are they? [duplicate]
Awarded Feb 10, 2022 at 13:26
Can we automatically get around set-theoretic difficulties?
Awarded Feb 10, 2022 at 9:57
Are there any proof assistants or theorem provers based on the method of analytic tableaux?
Awarded Feb 10, 2022 at 9:08
What are the advantages of normalization by evaluation over traditional reduction-based normalization?
Awarded Feb 10, 2022 at 3:42
Are there any non-English based proof assistants?
Awarded Feb 10, 2022 at 3:25
What are "locales" in Isabelle?
Awarded Feb 10, 2022 at 3:25
Are there any well-known Internal DSL Proof Assistants?
Awarded Feb 10, 2022 at 1:33
When to use coinductive types?
Awarded Feb 10, 2022 at 0:25
Can theorem provers be used to form foundations for programming languages?
Awarded Feb 9, 2022 at 23:11
What set-theoretic definitions can't easily be formalized in a type theory?
Awarded Feb 9, 2022 at 22:34
Where can I find lists of theorems that have been verified?
Awarded Feb 9, 2022 at 22:11
How can all functions be total in Isabelle?
Awarded Feb 9, 2022 at 20:34
1 2
3
4