Skip to main content
Proof Assistants Beta

Teacher

 Teacher
Answer a question with score of 1 or more.
Awarded 265 times.
What to import to use le_not_gt_iff?
Awarded 2 days ago
Using if in Fixpoint
Awarded Jul 1 at 22:41
Less ridiculous way to prove that an Ascii character compares equal with itself in Coq
Awarded Jun 27 at 20:25
Using if-then-else in Program Definition's obligation
Awarded Jun 19 at 20:47
Applying an axiom from a class in a proof
Awarded Jun 19 at 16:11
ACL2: Is there a way to check that a Skolem function does what it says on the tin?
Awarded Jun 19 at 15:32
Which proof assistant would you advise me to learn (in 2022) considering my interests?
Awarded Jun 19 at 5:55
Proving `succ_mul` without using `nth_rewrite`
Awarded Jun 17 at 14:55
Coq can you enter a tactic context inside of a `Fixpoint` definition?
Awarded Jun 15 at 4:45
Enumerating all formulae of any first-order language
Awarded Jun 12 at 20:20
When is the lean 4 "by" required?
Awarded Jun 12 at 19:04
Is the validity of induction in Coq axiomatic?
Awarded Jun 9 at 21:42
Offline install of Lean
Awarded Jun 3 at 23:32
How to prove termination of mutually recursive functions if only some decrease their arguments?
Awarded Jun 2 at 13:05
Proving `succ_mul` without using `nth_rewrite`
Awarded Jun 1 at 21:46
How do I properly interact with CertiCoq's garbage collector when calling library functions from C++?
Awarded May 21 at 9:16
How do I properly interact with CertiCoq's garbage collector when calling library functions from C++?
Awarded May 20 at 21:16
Book on Coq that helps me write proofs regarding integral equations
Awarded May 4 at 6:11
My Inductive function over a pair of lists gives "Cannot guess decreasing argument of fix."
Awarded Apr 27 at 17:35
Define maximum of matrix entries in Lean4
Awarded Apr 26 at 7:15
Why can't Lean4 evaluate my function despite it being defined, Error: compiler IR check failed at '_eval', error: unknown declaration 'g'?
Awarded Apr 23 at 20:00
Applying universally quantified equalities to propositions
Awarded Apr 14 at 16:27
Lean4: How to construct an HEq between dependent functions?
Awarded Apr 4 at 18:34
Pattern Matching on List x Fin
Awarded Mar 28 at 0:55
Paths Between Quotient Types in Cubical Agda
Awarded Mar 27 at 15:55
To what extent is formalized mathematics publishable?
Awarded Mar 22 at 14:48
How to convert Agda's with statement to a helper function?
Awarded Mar 17 at 14:55
Concrete examples in an Isabelle theory
Awarded Mar 8 at 14:27
Binding variables to terms involving later variables
Awarded Mar 1 at 8:40
Why can't Lean4 evaluate my function despite it being defined, Error: compiler IR check failed at '_eval', error: unknown declaration 'g'?
Awarded Feb 29 at 14:47
What is the well-established η law for naturals?
Awarded Feb 27 at 3:32
Stuck in a proof about sum types and nonempty lists
Awarded Feb 22 at 19:52
Recursive notations with forall quantifier
Awarded Feb 21 at 21:35
Determining why my proof depends on the axiom of choice
Awarded Feb 18 at 22:51
How to search for an existing theorem in Lean?
Awarded Feb 17 at 21:04
Proof Assistants in OOP languages
Awarded Feb 16 at 17:27
How to run lean4 with mathlib manually
Awarded Feb 8 at 18:38
Comparing indexed induction to recursion
Awarded Feb 4 at 7:07
Need help with induction proof in Lean for $0+d=d$
Awarded Jan 23 at 19:09
In Lean 4 how to use an implication in a hypothesis?
Awarded Dec 31, 2023 at 20:17
(post deleted or otherwise unavailable)
Awarded Dec 27, 2023 at 22:05
What is the state of Nuprl and Extensional Type Theory?
Awarded Dec 23, 2023 at 4:19
Coq makefile complains about extension points on Windows 10
Awarded Dec 18, 2023 at 6:50
How to to use the fact that combining these hypothesis is false in Coq
Awarded Dec 15, 2023 at 0:08
Why is lean 4 behaving differently on my machine vs in the natural number game?
Awarded Dec 5, 2023 at 1:26
What is a context mapping in dependent type checking?
Awarded Nov 29, 2023 at 2:05
metamath meta variables
Awarded Nov 26, 2023 at 10:05
What is the best way to learn Iris completely independently
Awarded Nov 20, 2023 at 10:10
Is there a multiway system which is equivalent to taking ZFC as axioms?
Awarded Nov 19, 2023 at 22:43
How to introduce assumption in lean4
Awarded Nov 9, 2023 at 4:17
Lean 4 Importing into VSCode
Awarded Nov 2, 2023 at 11:56
How to Prove Theorem le_zero in Lean4: If x ≤ 0, then x = 0?
Awarded Oct 30, 2023 at 12:57
Programming language metatheory in Lean 4?
Awarded Oct 25, 2023 at 13:46
Use proof irrelevance in cast
Awarded Oct 17, 2023 at 20:21
Is the Archive of Formal Proofs indexed in journal databases?
Awarded Oct 12, 2023 at 19:28
Simplifying Array Access
Awarded Oct 11, 2023 at 4:40
Proving that a minimum example exists if any example exists in nat
Awarded Oct 9, 2023 at 17:11
Benefits of HoTT compared with dependent type theory like what Lean does?
Awarded Oct 6, 2023 at 23:46
How to write this non-constructive proof in Lean?
Awarded Sep 25, 2023 at 19:27
Lean: what does the syntax `variable [ring R]` mean?
Awarded Sep 20, 2023 at 14:49
1
2 3 4 5