Skip to main content

Explore our questions

0 votes
2 answers
49 views

How to write a proof of n + 0 = 0 in Lean 4 using the built in definition of addition for Nats and not the theorem for Nat.add_zero?

0 votes
1 answer
183 views

An installation error in "Mathematics in Lean"

3 votes
1 answer
126 views

Is there a complete index of Lean 4 tactics?

3 votes
1 answer
84 views

How can I implement my own deriving in Lean4?

1 vote
1 answer
34 views

Lean 4 program to insert element in binary tree shows error: failed to sythesize instance LT \alpha

3 votes
1 answer
139 views

Help needed for Lean4 book Interlude exercise

1 vote
1 answer
60 views

Define maximum of matrix entries in Lean4

0 votes
0 answers
26 views

Inductive assumption in inductive case

2 votes
1 answer
64 views

Lean4 instance management

1 vote
1 answer
97 views

Applying universally quantified equalities to propositions

0 votes
1 answer
79 views

Using lean4 to prove subset properties

11 votes
3 answers
664 views

Given `A = B`, how to prove `a: A` also has type B in Lean 4

1 vote
1 answer
41 views

Lean 4 directive to always include a section variable

0 votes
3 answers
107 views

Why can't Lean4 evaluate my function despite it being defined, Error: compiler IR check failed at '_eval', error: unknown declaration 'g'?

Browse more Questions