Questions tagged [lean4]

Lean 4 is the latest major version of the Lean theorem prover by Microsoft Research. Use this tag for questions specific to Lean 4; if it's about Lean in general, use the tag (lean).

Filter by
Sorted by
Tagged with
3 votes
2 answers
67 views

How to run the main function in lean 4?

I am following the lean 4 tutorial and see a main function as follows: ...
user avatar
  • 1,310
5 votes
1 answer
97 views

How do I convince the Lean 4 type checker that addition is commutative?

In order to get acquainted with Lean and programming with dependent types I am trying to implement basic operations for a Vector datatype defined following the ...
user avatar
7 votes
1 answer
100 views

How to quickly look up what constructor/lemma I should use in Lean4?

When writing this answer, I had a hard time finding the lemma I needed to prove 2 ≤ 3. In Agda, when I have a goal, I can press ...
user avatar
  • 4,136
4 votes
2 answers
136 views

Non-trivial examples of dependent sum ($\Sigma$-types) in Lean?

I am trying to understand the concept of dependent sum types ($\Sigma$ types) using concrete examples. The example given in Theorem Proving in Lean 4 seems to be a degenerate case rendering the ...
user avatar
  • 1,310
10 votes
1 answer
77 views

Rewriting with context in nested expressions (congruence rules)

I am trying to prove the following example in Lean 4: ...
user avatar
6 votes
3 answers
130 views

Preserve equality with match expression

How can I prove that the matched pattern is equal to the original argument? For example, in the following function, what can I write instead of sorry to prove the ...
user avatar
24 votes
1 answer
243 views

What will happen to mathlib when we transition to Lean 4?

Today, there's an exciting large-scale effort to digitize mathematics in Lean's mathematics library mathlib. I understand that a transition to Lean 4 is looming. I'...
user avatar
15 votes
0 answers
113 views

Programming language metatheory in Lean 4?

I'm looking for developments of programming language metatheory done in Lean 4. We have a calculus with a lot of mutually recursive judgements and we want to formalise its denotational semantics. ...
user avatar
7 votes
2 answers
232 views

How do I install Lean 4?

I want to get started with Lean 4, but I need to install it. The download page links to binaries to download, but I don't know what to do with them. Is there a "best practice" way to install ...
user avatar
  • 220