# 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).

117 questions
Filter by
Sorted by
Tagged with
1 vote
40 views

### What is the official way to reinstall Lean4 from scratch on a Mac or Linux?

What is the official way to reinstall Lean4 from scratch on a Mac or Linux? I want to install Lean from scratch to see if I can fix a previous issue related to the location where I can create lean ...
18 views

### How does one create a lean project even if it already exists e.g., lake +leanprover/lean4:nightly-2023-02-04 new my_project math?

I want to initialize a lean project but the folder I have already exists. How do I do this? e.g., ...
61 views

1 vote
41 views

### Inductively proving that a number is either even or odd in Lean

I have the following Lean definitions: def is_even (a : Nat) := ∃ m, a = 2 * m def is_odd (a: Nat) := ∃ m, a = 2 * m + 1 The following proof would be complete if I ...
• 13
1 vote
97 views

### Using decreasing_by to prove termination in Lean 4

Warning: This was written for Lean v4.5.0. To make the accepted answer work, please use v4.6.0-rc1. I would like to define an elementary quicksort function for ...
• 157
89 views

### Two steps induction in Lean4: how to obtain 2nd inductive hypothesis?

When trying to solve this example from "The Mechanics of Proof": ...
69 views

### What am I doing wrong when proving the add_right_cancel theorem?

So, as mentioned in my previous two questions, I have been using The Natural Number Game to help me teach myself how to use the mathematical proof assistant Lean4. I am currently trying to complete ...
• 145
164 views

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

So I have been using The Natural Number Game (as I have mentioned in my previous post) to learn Lean1. However, I am currently stuck on level 6/9 in the Algorithm world, where I am supposed to prove ...
• 145
1 vote
98 views

### Need help with induction proof in Lean for $0+d=d$

So I have been trying to learn Lean and have managed to find this resource called the "Natural Number Game" which is supposed to help me learn Lean. I am learning Lean to help me understand ...
• 145
71 views

### How to lift a binary function to a quotient?

Kia ora :) I am trying to use Quot. in Lean4 to define the integers as the quotient of the Cartesian product of two copies of the natural numbers (type Peano) under the relation: ...
88 views

### In Lean 4 how to substitute equals in an expression with other variables?

I can use 'subst' to prove that if a=b and a is positive then b is positive: example (a b : Peano) (h1 : a = b) (h2 : pos a) : pos b := Eq.subst h1 h2 How do I ...
1 vote
94 views

### How to see the value under Exists in Lean?

My understanding of dependent typing is that it allows typing functions to constrain their behavior. Say I have a Lean object ...
• 13
88 views

### Shortcut proof by calculation for addition/subtraction, "The Mechanics of Proof", and mathlib4

In Macbeth's book 'The Mechanics of Proof,' the author provides a tactic called addarith to eliminate the need to write calc ...
91 views

### In Lean 4 how to use an implication in a hypothesis?

I am experimenting with my own "natural numbers" (Peano), so I don't want to use Lean 4's natural number tactics (such as add_comm or cancellation). How can the following be proved? It ...
89 views

### An installation error in "Mathematics in Lean"

I have just started learning Lean 4 using Mathematics in Lean in Visual Studio Code, and I ran into a problem right away. I get the following error message: ...
158 views

### Verifying a basic function with Lean4

I have this simple structure to represent a person: structure Person where age: Nat lifespan: Nat deriving Repr This function takes a Person and either (a) ...
149 views

### Are type universes related to proper classes from set theory?

I'm currently learning Lean 4, and in the book they mention that the type hierarchy was introduced to avoid a version of Russell's paradox. From reading a bit about set theory a while ago, I remember ...
208 views

### How to use the most bare essentials of Lean 4?

As a learning exercise I want to use Lean 4 to prove theorems about natural numbers, but WITHOUT Mathlib (or as little as possible). I want to start with 2 Peano theorems s(x) != 0, and s(x)=s(y) ->...
1 vote
127 views

### Lean 4 exercise: Why can't I write this function definition inside an instance declaration?

In Lean 4.3.0, I'm solving an exercise from section 4.5 "Standard Classes" of the excellent book "Functional Programming in Lean". Given the structure ...
• 113
1 vote
59 views

### Peano Arithmetic in LEAN4 [duplicate]

Kia ora! I am trying to implement the Peano axioms and prove some simple theorems about the natural numbers in LEAN4. However, I am not sure how to encode the first two (as presented here) axioms in ...
112 views

### Lean 4: How can I specify that out of two universe variables, one is larger than the other?

Before Mathlib 4 was finished, I decided to implement my own ordinals, but this was as I was learning Lean 4, so my Ordinal type had type Type 1 instead of the ...
65 views

### In lean 4, how do I give names to variables when using split?

Sort of related to In lean 4, how do I refer to variables with names like a✝ When I use split to pull apart a match, I get a ...
• 437
121 views

### In lean 4, how do I refer to variables with names like a✝

When I have a tactic state that mentions a variable name like a✝, is there a way to refer to it? When I use this variable name in my code, it says it doesn't exist. ...
• 437
1 vote
81 views

### What do I need to import from MathLib to make induction a with d hd work?

I know that I need to import Mathlib to make rewrite [x] at h work. But induction a with d hd...
• 437
421 views

### Why is lean 4 behaving differently on my machine vs in the natural number game?

In the lean 4 version of the natural number game at https://adam.math.hhu.de/#/g/leanprover-community/NNG4/ , I can use tactics like apply x at h and ...
• 437
100 views

### Print the version of lean that is running

In python, I can get the version of python I am using like this: import sys print(sys.version) ...
• 437
84 views

### In lean4 why is induction only rewriting the goal, and not the known facts?

When I do induction over a variable $x$ in lean 4, why isn't $x=0$ available as a fact in the base case of the induction? Without this fact, I can't rewrite other facts in order to make the induction ...
• 437
89 views

### Apply unfold once, instead of many times, in lean4

I have code that is similar in spirit to this: ...
• 437
1 vote
31 views

### Case assumption missing from tactic state in lean4

I'm trying to prove a <= max(a, b) by case. I have this: ...
• 437
211 views

### How do I make the rational numbers 0 and 1/2 in lean4?

I'm trying to define a function that in python I would write: def f(x: bool) -> float: if x: return 0.5 return 0.0 In lean 4 I tried writing ...
• 437
76 views

### Shortening a 4-levels-of-match lean4 proof of the CHSH inequality

In the CHSH game, Alice (Bob) is given the value $x$ ($y$) and needs to pick a value $a$ ($b$) such that $a \oplus b = xy$. The CHSH inequality proves they can win at most 75% of the time with ...
• 437
1 vote
119 views

### Rewriting certain terms in Lean4

I want to prove the following theorem using a single axiom (https://mathworld.wolfram.com/WolframAxiom.html): ...
• 113
1 vote
153 views

### How to introduce assumption in lean4

This is probably a trivial question, but I've been googling for hours and can't find the syntax I'm looking for. I'm trying to write a proof of ...
1 vote
161 views

### How to run lean4 with mathlib manually

I have a file which contents are: import Mathlib.Data.Rat.Basic I save it as file.lean in a lean project and run it like this ...
• 151
209 views

### How to understand the sigma types example from "Theorem Proving in Lean 4"?

In the Lean 4 book called "Theorem Proving in Lean 4" (https://lean-lang.org/theorem_proving_in_lean4/title_page.html), I don't understand a code example about cartesian product types in ...
• 123
181 views

### How to Prove Theorem le_zero in Lean4: If x ≤ 0, then x = 0?

I am playing the Natural Number Game found here and am trying to prove a theorem in Lean4. The theorem states that if a natural number x is less than or equal to 0, ...
• 151
1 vote
182 views

### how to prove 2+2+a=4+a in lean4?

It should be simple but dig it for a while and still not successful. theorem example (a : R) : 2 + 2 + a = 4 + a := ... can someone help to figure out how to do next? many thanks
• 11
211 views

### How to handle data from json files in lean 4?

I don't know how mature or efficient Lean 4.1.0's standard feature support is. However, I did enjoy an interesting case about benchmarking data processing languages.The challenge is to read a json ...
99 views

### Simplifying Array Access

I'm confused how to show the second example here: ...
• 123
435 views

### Benefits of HoTT compared with dependent type theory like what Lean does?

I am not an expert in type theory, so I wonder what will HoTT bring to theorem proving (ITP/ATP), compared with dependent type theory? More specially, imagine Lean is implemented using HoTT, I would ...
• 171
124 views

### Highschool level linear algebra

I would like to be able to do high-school level linear algebra in Lean/Mathlib. However, it seems pretty hard. I do understand that mathematicians don't care about being able to do this basic stuff ...
222 views

### Understanding noConfusion

Data.List.getLast is defined as follows: ...
93 views

### Is there an algebreic type in lean4?

In lean4 I've seen the Real, Rat, and Int types, but is there an Algebreic type? Loooking at: https://leanprover-community.github.io/blog/posts/dedekind-domains-and-class-number-in-lean/ which links ...
• 101
139 views

### How to think about writing Lean theorems

In Lean we make definitions and formulate theorems about the things we have defined. Seemingly, to each definition there exists several simple theorems. Let's go to ...
• 486
156 views

### Understanding Mathlib/MeasureTheory Notation

I want to understand Mathlib/MeasureTheory, and in particular I want to understand Mathlib/MeasureTheory/Integral. I'm having ...
• 486
55 views

### Automatic nightly Lean update?

I recently answered my own question for how to set up a Lean project with Mathlib dependencies. I realize I don't know everything about this. The route I follow starts by navigating to the correct ...
• 486
184 views

### What is the precise meaning of "reducible"?

In Lean 4, I've seen the terms "reducible", "semi-reducible" and "irreducible" mentioned a lot. What is the precise meaning and how are these concepts used in code? When ...
460 views

### Does lean 4 have built-in dictionary types?

Are there builtin dictionary/map types in Lean 4 prover? I'd like to use dictionaries in my program and prove properties about it, but I am not sure if there is a dictionary type in Lean 4. A similar ...
• 1,896
1 vote
78 views

### Where do I prove that a return type is valid?

I am learning Lean 4 by implementing a fixed-length vector type. Type definition: ...
132 views

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

Here's a simple dummy function in Lean 4: def foo : Nat → Nat | (m*2) => m | (m+2) => m | (m+1) => m | (0) => 0 Lean has no trouble ...
• 197