Skip to main content
36 votes

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

BIG UPDATE The port to Lean4 is officially complete. There is a couple changes that we are still hoping to officially put into mathlib3 before moving it into ...
It'sNotALie.'s user avatar
  • 1,445
12 votes
Accepted

What are the differences between theorem, example, def, etc?

An outline of the differences in Lean 4, which you mentioned is the version you are interested in: A def is the primary way to define a named function / value in ...
tydeu's user avatar
  • 341
11 votes
Accepted

How do I install Lean 4?

Install the latest Lean 4 nightly through elan: in any bash-compatible shell, run: ...
taylor.2317's user avatar
  • 1,318
11 votes

A project in Lean which involves "programming"

First there is no reason to put quotes around "programming". Lean 4 is a fully capable programming language with all the needed features. But it is also a (very pure) functional ...
Jason Rute's user avatar
  • 8,655
10 votes
Accepted

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

[Note: Anyone reading this should also check Jason Rute's answer which shows how to do these things in Lean idiomatically.] Indeed, you are experiencing the XY problem. You are not taking the ...
Andrej Bauer's user avatar
  • 9,104
9 votes
Accepted

Preserve equality with match expression

The syntax for this is match h : x with, no whitespace after h or :, which will leave you ...
ammkrn's user avatar
  • 161
9 votes

Preserve equality with match expression

In Lean 3, you can solve this using the following syntax: ...
Eric's user avatar
  • 971
9 votes

Are there computable functions which can't be expressed in Lean?

Yes. This is always going to be the case because of the halting problem: The set of functions accepted by lean is computable (because lean computes it), so if all halting functions are in the set then ...
Mario Carneiro's user avatar
8 votes
Accepted

How to run the main function in lean 4?

You may extract C source and compile it: ...
siegment's user avatar
  • 272
8 votes
Accepted

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

Here are a few ways of getting this goal without really knowing anything about what the definition of LT is etc. In rough order of low-tech to high-tech, we have: a tactic that tries to apply ...
Alex J Best's user avatar
8 votes
Accepted

Are there computable functions which can't be expressed in Lean?

Since Lean programs always terminate, it cannot be Turing-complete. In particular, one specific computable-but-not-Lean-computable problem is the problem of evaluating computable Lean expressions (i.e....
soktinpk's user avatar
  • 196
8 votes
Accepted

What are the goals of Lean 4?

There are many aspects to this: It's faster (e.g. the ~80% portion of mathlib that has been ported so far compiles between 3 and 4 times faster than it did under Lean 3.) The metaprogramming ...
Kim Liesinger's user avatar
6 votes

Preserve equality with match expression

Your question is for Lean, but users of other languages might stumble over it as it is a quite common problem, so it might be useful to collect design patterns in all languages. In Agda, the inspect ...
Maximilian Doré's user avatar
6 votes
Accepted

Lean4 Exercise: Double negation implies law of excluded middle

TLDR: Supply the argument p ∨ ¬ p to both dne and p to ...
Jason Rute's user avatar
  • 8,655
6 votes
Accepted

Speeding up large data structures in Lean

(This question has since been solved on Zulip, so I'm copying the resolution here for posterity.) This is an implementation which reads the tree via an external ...
Mario Carneiro's user avatar
6 votes
Accepted

How do I prove $\operatorname{succ}(a)$ cannot be equal to $0$ in Lean4?

The exercise gives starting instructions: intro h rw [<- is_zero_suc a] These give the following proof state: ...
James Wood's user avatar
  • 1,053
5 votes
Accepted

Explain all the arguments to this rec eliminator

I found hints of the answer here The original definition of JSON "falls outside the strict specification of an inductive type" because ...
Felipe's user avatar
  • 273
5 votes
Accepted

Unclarity about Preorder class in Lean4

The extra fields are a convenience. It is useful to have both $<$ and $\leq$ at disposal when working with preorders, so how can we have that? We could decide which one is “primary”, include it in ...
Andrej Bauer's user avatar
  • 9,104
5 votes
Accepted

Equality of records with members whose types are dependent (Lean 4)

It is pretty simple. I'll give you a few options so you can learn more about Lean. A brute force way to do it is to use calc. I know I taught you last time about <...
Jason Rute's user avatar
  • 8,655
5 votes

Programming language metatheory in Lean 4?

We've been developing the metatheory of SSA based programs at https://github.com/opencompl/ssa/. In particular, we develop: An intrinsically well-typed encoding of SSA+Regions A mechanized peephole ...
Siddharth Bhat's user avatar
5 votes
Accepted

Is there a way in LeanProver to declare an inline recursive function, like fix in Coq?

You can use let rec or where to introduce a helper function mutually recursive with cmp and ...
Sebastian Ullrich's user avatar
5 votes
Accepted

Pattern matching from `Prop` to `Type` in Lean

There are situations in which every morphism $A \to B$ is constant: In topological spaces, if $A$ is a space with the trivial topology and $B$ is a $T_0$-space then a continuous map $A \to B$ is ...
Andrej Bauer's user avatar
  • 9,104
5 votes

How to prove the termination of Ackermann in Lean?

Usually x-1 is harder to work with (but not impossible). Pattern matching is much easier from a type theoretic perspective. So (this is actually one of the test ...
Trebor's user avatar
  • 3,927
5 votes
Accepted

Auxiliary Typeclasses in Lean

This is done so that formalization matches mathematical practice. Defining only PseudoMetricSpace directly with dist would ...
Andrej Bauer's user avatar
  • 9,104
5 votes
Accepted

Aesop Tactic in Lean

SimpleGraph is a definition of a "simple graph" in the mathlib4 library. The API for SimpleGraph uses ...
Kim Liesinger's user avatar
5 votes

Where is the syntax of Lean 4 documented?

It seems in general there are two approaches to learning a programming language. I think an older approach is a complete encyclopedic reference manual which lays out the whole language in one go, ...
Jason Rute's user avatar
  • 8,655
5 votes
Accepted

proof of termination for zip in Lean

It seems you are trying to use Simultaneous Matching on the two lists as and bs but messed up the syntax, and instead are ...
Meven Lennon-Bertrand's user avatar
5 votes

Why can addition be used in pattern matching Nats but not multiplication

The short answer is two fold: For a pattern to be matchable it has to be only using variables and the basic constructors for a given inductive/structure type. For ...
Jason Rute's user avatar
  • 8,655
5 votes
Accepted

What is the precise meaning of "reducible"?

The short version is that these are just settings you can apply to definitions. When you define a definition you say whether it is reducible (abbrev or ...
Mario Carneiro's user avatar
5 votes
Accepted

How to see the value under Exists in Lean?

It comes down to how you interpret your questions. Can I run this as a function? The main issue in this case is that in Lean uses ...
Jason Rute's user avatar
  • 8,655

Only top scored, non community-wiki answers of a minimum length are eligible