Proof Assistants Beta

Self-Learner

 Self-Learner
Answer your own question with score of 3 or more.
Awarded 19 times.
Is there a formalism of "coinductive" data types with negative occurrences?
Awarded Aug 8 at 14:57
What proof assistants can reason about the complexity of its *own* programs?
Awarded Mar 24 at 20:27
How to show that an expression of a finite type must be one of the finitely many possible values?
Awarded Mar 17 at 2:25
Counterexamples in Type Theory
Awarded Jan 1 at 16:34
Explain all the arguments to this rec eliminator
Awarded Nov 12, 2022 at 1:42
How to unfold definitions in Lean / find the right theorems to apply?
Awarded Oct 30, 2022 at 17:47
I'm stuck trying to prove ∀x : ℕ, 3 | (x + 5x) with Coq
Awarded Aug 1, 2022 at 15:42
What's "predicative" about pC(u)IC?
Awarded Apr 1, 2022 at 7:07
How does the formal proof of the four color theorem work?
Awarded Mar 25, 2022 at 13:30
What provers are using quote, quotations or quasiquotations?
Awarded Mar 19, 2022 at 6:25
What is Artin gluing, and how is it useful in proving meta-theoretic properties?
Awarded Mar 4, 2022 at 14:55
Why is `--irrelevant-projections` unsafe in Agda?
Awarded Mar 2, 2022 at 16:35
What's the difference between a universe level and a natural number?
Awarded Feb 23, 2022 at 22:26
How to install Lean-4 stable only?
Awarded Feb 21, 2022 at 8:32
How do you import part of the standard library in Coq?
Awarded Feb 14, 2022 at 20:17
How can I derive other type classes in Isabelle/HOL?
Awarded Feb 13, 2022 at 22:21
What is the state of recompilation avoidance in proof assistants?
Awarded Feb 11, 2022 at 15:19
How can all functions be total in Isabelle?
Awarded Feb 9, 2022 at 20:52
Examples of new mathematics discovered through formalization?
Awarded Feb 9, 2022 at 20:52

Your privacy

By clicking “Accept all cookies”, you agree Stack Exchange can store cookies on your device and disclose information in accordance with our Cookie Policy.