# Questions tagged [lean3]

Lean 3 is the previous version of the Lean theorem prover, and has an active "community" release. If using the final "official" release from 2019 (3.4.2) which is incompatible with [mathlib], make this clear in your question.

34 questions
Filter by
Sorted by
Tagged with
1 vote
291 views

### How to write this non-constructive proof in Lean?

There is a theorem which says that there exists two irrationals $x, y$ such that $x^y$ is rational. An interesting proof in classical logic is the following: Consider $u = \sqrt{2}^{\sqrt{2}}$. If $u$...
96 views

### Lean: what does the syntax variable [ring R] mean?

I have written a simple Lean program, inspired by things I found here and there, which compiles as shown in the web editor: ...
28 views

### Proving (((finset.range 50).erase 0).erase 1).sum id = (finset.range 50).sum id - 1

I'm trying to prove the statement (((finset.range 50).erase 0).erase 1).sum id = (finset.range 50).sum id - 1 in Lean 3. The mathlib theorem ...
1 vote
179 views

### How to parse Lean 3(?) theorem statements to JSON AST

I'd like to take a .lean file, and extract from it all the theorem statements into a fully-elaborated unambiguous textual format that is morally isomorphic to the ...
166 views

### Porting Lean 3 to Lean 4 Process (and the state of general integration in Lean 4)

I found this reference for measure-theoretic integration in Lean. However, I cannot find any integration in the Lean 4 Measure Theory library. Have these not yet been ported, or can they be found ...
106 views

### Differential Topology and Differential Geometry Porting to Mathlib4

Simple question, but I started working with Lean after Lean 4 came out, so I'm not familiar with Lean 3. To what extent have the Mathlib3 differential topology and differential geometry libraries been ...
89 views

### Recursive definition of a sum of squares

I am trying to formalise in Lean3 the notion of sum of squares in a ring. If $A$ is a ring, $n$ is an integer and $f$ is a function from  F_n:= \{ i \in \...
130 views

### Vectors in Lean

In Lean vectors are implemented using def Vec (a : Type u) (n : Nat) := { l : List a // l.length = n} I think there is another way to do this without lists: <...
302 views

### Type Theory Lean 3 to Lean 4

I'm aware of Lean's type theory. Did the type theory of lean change at all as we moved to Lean 4? Are there any references to this?
132 views

### Equality of two functions

I am wondering about definition of functions in Lean and proving equality (in some sense to be defined) of two functions. Note: I have consulted the answer to the following related question but it ...
1 vote
916 views

### Make ChatGPT write formal proof from natural language proof

I know very little about proof assistants, but I played a little with Lean, so I have some basic knowledge of how they work. I was curious whether I could make ChatGPT convert some natural language ...
109 views

### A chain of coercion in Lean fails to infer the correct type automatically but each separate step does

Context I have defined two structures corresponding to a group and a subgroup : ...
408 views

### How can I use a dummy variable to prove a lemma in Lean3?

I have the following definition for the operator D: noncomputable def D: (ℝ → ℝ) → (ℝ → ℝ) := λ f, deriv f I want to prove that ...
70 views

### Are there squeeze-versions of ring and abel?

In Lean, it is recommended to use squeeze_simp to generate simp only [a bunch of lemmas] for two reasons: (1) Otherwise the ...
204 views

### Eliminating "Exists Unique" in Lean 3

In Lean 3, similar to this question, I want to exhibit a witness of $x$ of $P(x)$, given that $\exists x,P(x)$. The difference is that I can also prove $\exists! x,P(x)$, so there is exactly 1 element ...
419 views

### Installing relevant packages for Lean's math lib

I'm using the Lean computer proof assistant on my Mac. I tried to import data.nat.basic from lean's documentation, just like this: import data.nat.basic I get this:...
94 views

### Why does an internal term produced by Lean's equation compiler have holes in it?

Section 4.7 of the Lean reference manual (version 3.3) gives an example of a division function defined by well-founded recursion. I used the #print command to ...
1 vote
74 views

### Code obtained from printing a definition from the Lean 3.46 equation compiler does not type check. Why doesn't it, and how can I fix it?

In the example below, the fibonacci function is defined via the Lean equation compiler. However, there seems to be a problem with the code that is obtained from running ...
97 views

### Prove in Lean that ∀ i, 0 ≤ X i → ∃ i, X i > 1 → ∑ i, X i > 1

How to prove that if a term in a sum is > 1 then the sum is > 1? ...
272 views

### Cardinality of Type in a given universe

I'm trying to determine the cardinality of Type u in Lean 3. So far I've been able to prove two inequalities: ...
192 views

### Proof of a certain proposition not using classical logic

I'm self-studying the textbook Theorem Proving in Lean, and there's one exercise from Section 3.7 that I'm stuck on. The exercise asks for a proof of the proposition ¬(p ↔ ¬p) that does not use ...
212 views

### Define a new Type in Lean: Tensor power of vector space

I want to define the tensor power of a vector space from the Lean library mathlib. Here's the draft I have so far: ...
945 views

### In Lean, contradiction tactic failed but actually goal accomplished

I've been playing with Lean, trying to prove the next lemma: lemma l1_cl (A B C : Prop) : ((A → B) → C) → ((A ∧ ¬ B) ∨ C) := ...
230 views

### How to prove in Lean that sums are distributive?

Assume we are given three types in Lean. constants A B C : Type There is a canonical map of the following form. ...
202 views

### Lemma about splitting of homogeneous polynomial equations into irreducible equations

Proof assistants, and Lean, are completely new to me. How can I derive the following simple lemma in Lean? How can I let Lean check if the lemma is correctly written? How can I let Lean check if the ...
615 views

### Lean "nonempty" vs "inhabited"

In the init/logic.lean file of the Lean 3 standard library, nonempty and inhabited are defined. It seems like these two classes ...
591 views

### How to define curry in Lean

I just started with Lean and with this nice SE. In the official web book/tutorial, when explaining definitions https://leanprover.github.io/theorem_proving_in_lean/index.html they ask to complete this ...
413 views

### How to speed up Lean?

I've recently been writing my first somewhat serious proof in Lean. While doing that, I noticed that Lean gets slower very fast with increasing length of the proof (slower in the sense that whenever I ...
699 views

### What does the "motive is not type correct" error mean in Lean?

Sometimes, trying to use rw in Lean, we get an error saying motive is not type correct What does this mean? Often ...
384 views

### Strong induction on ℕ with function α → ℕ

I have the following problem. I have a type $\alpha$, function $f : \alpha \to \mathbb{N}$ and predicate $P : \alpha \to \mathrm{Prop}$ and I want to prove that for all $a : \alpha, P a$. How could ...
217 views

### Explicit vs implicit universes in lean

I've seen in mathlib several cases where the universes are explicit, that is Type u instead of Type*. Is there any advantage in ...
489 views

### What is the difference between refl and rfl in Lean 3?

I already know that refl is called a tactic, and that rfl is a term; can you explain with examples how they technically differ? ...