Skip to main content

Explore our questions

5 votes
2 answers
437 views

Is there a complete index of Lean 4 tactics?

3 votes
1 answer
87 views

Stochastic calculus in Lean4?

3 votes
2 answers
274 views

What is the unicode braces {| |} (⦃ ... ⦄) in lean 4?

1 vote
1 answer
24 views

Passing functions to casesOn which do not depend on a pattern match

2 votes
1 answer
175 views

Could proof assistants fill in single theorems automatically?

1 vote
0 answers
43 views

How to enter in Lean 4 the unicode for "LEFT SQUARE BRACKET WITH TICK IN TOP CORNER"

2 votes
1 answer
127 views

How to do recursive type coercion in Lean

4 votes
0 answers
133 views

How do I write a definition/theorem with an arbitrary number $n$ of types?

4 votes
2 answers
111 views

How to make lean 4's rw tactic rewrite at a given position of ocurrence?

1 vote
2 answers
112 views

why I cannot apply `ring` to `y = x * y / x`

3 votes
1 answer
194 views

Why is this not definitionally held?

2 votes
0 answers
68 views

Proof Checking for State Machines Similar to TLA+

1 vote
1 answer
145 views

Can some existing proof assistant, in its current state of the art, encode this small theory about a twin prime counting function?

1 vote
1 answer
71 views

Lean Proving a Prop that has a match

Browse more Questions