Skip to main content
Proof Assistants Beta

Teacher

 Teacher
Answer a question with score of 1 or more.
Awarded 282 times.
Using crude but effective stratification & cong to implement transitivity of `=`
Awarded Dec 7 at 2:12
(post deleted or otherwise unavailable)
Awarded Nov 29 at 14:08
What exactly is setoid hell?
Awarded Nov 29 at 8:16
Which natural deduction rule is this "application"?
Awarded Nov 19 at 16:07
Is the Archive of Formal Proofs indexed in journal databases?
Awarded Nov 15 at 17:13
Conclude from 2 * m = 3 * n, that n is divisible by 2
Awarded Nov 12 at 9:56
How does Z3 "exhaustively search" real numbers?
Awarded Nov 4 at 3:55
Toy proof assistants with very small codebases
Awarded Oct 30 at 18:06
How can I generate equalities from an application in Coq?
Awarded Oct 28 at 18:20
First order logics exercise
Awarded Oct 17 at 11:08
(post deleted or otherwise unavailable)
Awarded Sep 22 at 14:32
Is there a complete index of Lean 4 tactics?
Awarded Sep 7 at 13:07
What is the unicode braces {| |} (⦃ ... ⦄) in lean 4?
Awarded Sep 3 at 18:25
Using Isabelle's Archive of Formal Proofs
Awarded Aug 11 at 6:47
Proving factors of GCD in Dafny
Awarded Jul 15 at 11:34
What is an assumption in Isar?
Awarded Jul 7 at 19:25
Code Review: $\mathbb{Z}[\sqrt{-2}]$ is an integral domain
Awarded Jul 7 at 4:30
What to import to use le_not_gt_iff?
Awarded Jul 3 at 9:10
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
1
2 3 4 5