Skip to main content
Proof Assistants Beta

Student

 Student
First question with score of 1 or more.
Awarded 431 times.
Best tool for proving that a (big) first order model is actually the model of some (big) first order theory.
Awarded yesterday
Why the result of pattern matching don't get propagated in some expressions?
Awarded 2 days ago
Coq: when to give a context variable of imported package as argument
Awarded Dec 9 at 13:12
Induction over multiple arguments in Isabelle
Awarded Dec 8 at 9:47
Constructing elements of Fin type after using `<?`
Awarded Dec 7 at 10:12
How to automate resolving circular dependencies between definitions and obligations in Coq?
Awarded Dec 7 at 6:31
how to proof on coq double negation of p is logical equivalent to p
Awarded Dec 6 at 23:53
How to do simultaneous induction in Coq?
Awarded Dec 6 at 2:13
Inductive Hypothesis is wrongly generated
Awarded Dec 5 at 15:20
Proof assistants for undergraduate analysis
Awarded Nov 29 at 5:01
In LEAN4 prover, what's the problem of generalising a type from String to a free type?
Awarded Nov 28 at 10:36
Need help to prove that a variable is extracted using pattern matching from a pair (or a dependent pair) in Lean 4
Awarded Nov 24 at 14:58
How to prove basic lemmas about divisibility in Coq?
Awarded Nov 21 at 1:58
Type annotation of fixpoint combinator intereferes with Lean4's strictness
Awarded Nov 20 at 17:26
State of homotopy canonicity of HoTT with univalence axiom
Awarded Nov 20 at 17:12
Why unknown identifier for a declared variable in Lean 4
Awarded Nov 18 at 10:15
(post deleted or otherwise unavailable)
Awarded Nov 15 at 3:40
Conclude from 2 * m = 3 * n, that n is divisible by 2
Awarded Nov 12 at 11:01
How to implement DecidableEq on a inductive datatype manually in Lean 4?
Awarded Nov 10 at 21:26
Overwrite notation in LEAN4
Awarded Nov 10 at 12:41
constructing new types
Awarded Nov 9 at 18:03
Error when making CoqProject
Awarded Nov 5 at 12:37
Searching for alternative of doing maths with pen and paper
Awarded Nov 4 at 3:55
Proofs with summations ∑ in Lean 4
Awarded Oct 31 at 19:35
Axiom of Choice in COQ
Awarded Oct 28 at 17:03
I need help with min problem
Awarded Oct 23 at 9:48
Proving fact about reduction function and natural addition
Awarded Oct 21 at 15:31
Principle like UIP on Types with Decidable Equality but for Inequality Proofs
Awarded Oct 21 at 9:23
How does the case (destruct) tactic change the goal?
Awarded Oct 16 at 13:10
Why does Lean 4 not execute the given code?
Awarded Oct 14 at 8:05
How can I limit the decimal places a real variable can have in Z3 Theorem Prover?
Awarded Oct 9 at 19:41
Isabelle/HOL eprover processes do not exit
Awarded Oct 4 at 16:35
Unknown Identifier issue in Lean 4
Awarded Sep 29 at 8:05
How to prove that < implies <= for real numbers in Coq
Awarded Sep 24 at 18:07
An installation error in "Mathematics in Lean"
Awarded Sep 24 at 18:07
How to reason with notations directly?
Awarded Sep 18 at 21:51
How to use Modus Ponens in L axiomatic system
Awarded Sep 15 at 14:30
Extensional sets in Coq and induction
Awarded Sep 5 at 20:12
Stochastic calculus in Lean4?
Awarded Sep 3 at 17:27
Passing functions to casesOn which do not depend on a pattern match
Awarded Sep 2 at 19:16
What the differences between equivalence in HoTT and isomorphism in category？
Awarded Aug 25 at 17:47
How do I write a definition/theorem with an arbitrary number $n$ of types?
Awarded Aug 18 at 1:06
Bad session in Isabelle
Awarded Aug 16 at 5:40
How do I apply a lemma to both sides of an equality hypothesis?
Awarded Aug 12 at 9:53
why I cannot apply `ring` to `y = x * y / x`
Awarded Aug 6 at 18:56
Why is this not definitionally held?
Awarded Aug 2 at 15:19
Proof Checking for State Machines Similar to TLA+
Awarded Aug 1 at 23:01
STLC substitution behaviour with lambda body normalisation
Awarded Jul 31 at 10:03
Open source implementations of euclidean geometery automated theorem provers
Awarded Jul 27 at 20:40
Introductory resources on rewriting logic
Awarded Jul 17 at 2:40
Lean Proving a Prop that has a match
Awarded Jul 15 at 14:52
The relationship between "true formula" and types in the Curry–Howard correspondence
Awarded Jul 13 at 9:19
Inconsistent failures of coercions when type checking in Coq
Awarded Jul 6 at 4:26
Using Isabelle's Archive of Formal Proofs
Awarded Jul 2 at 1:44
Best practices: Should I prefer definitions or iff when defining predicates?
Awarded Jun 28 at 15:48
Is there any way to approximate noncomputable functions in Lean4?
Awarded Jun 26 at 20:55
Finding reflexive, transitive closure
Awarded Jun 24 at 9:36
Formalizing "finite or infinite" in Coq
Awarded Jun 23 at 16:45
Use of `by` on first line of lean proof - when to / when not to? [duplicate]
Awarded Jun 21 at 0:48
Proper LEAN_PATH environment variable value for Windows Lean Visual Studio project?
Awarded Jun 20 at 19:21
1
2 3 4 5
…
8