Skip to main content

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.

Filter by
Sorted by
Tagged with
2 votes
1 answer
320 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$...
Weier's user avatar
  • 313
3 votes
1 answer
107 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: ...
Weier's user avatar
  • 313
2 votes
0 answers
30 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 ...
Arnoud Nijon's user avatar
1 vote
2 answers
233 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 ...
Michael Norrish's user avatar
0 votes
0 answers
249 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 ...
Alex Byard's user avatar
0 votes
2 answers
148 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 ...
Alex Byard's user avatar
2 votes
1 answer
110 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 \...
Matematiflo's user avatar
2 votes
1 answer
276 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: <...
Alex Byard's user avatar
6 votes
2 answers
349 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?
Alex Byard's user avatar
2 votes
1 answer
175 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 ...
Matematiflo's user avatar
1 vote
2 answers
1k 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 ...
domotorp's user avatar
  • 121
0 votes
1 answer
119 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 : ...
Blumer's user avatar
  • 11
2 votes
3 answers
421 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 ...
Ícaro Lorran's user avatar
3 votes
1 answer
94 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 ...
Strichcoder's user avatar
2 votes
1 answer
299 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 ...
Zongshu Wu's user avatar
0 votes
1 answer
642 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:...
Ronald J. Zallman's user avatar
2 votes
1 answer
105 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 ...
ttbo's user avatar
  • 35
1 vote
1 answer
80 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 ...
ttbo's user avatar
  • 35
0 votes
1 answer
111 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? ...
user120404's user avatar
7 votes
1 answer
357 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: ...
Matt Diamond's user avatar
2 votes
0 answers
245 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 ...
Gavin Dooley's user avatar
5 votes
1 answer
221 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: ...
user120404's user avatar
7 votes
1 answer
982 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) := ...
Pavel Snopov's user avatar
6 votes
2 answers
265 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. ...
Nico's user avatar
  • 722
2 votes
1 answer
206 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 ...
IV_'s user avatar
  • 131
15 votes
1 answer
773 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 ...
Bolton Bailey's user avatar
9 votes
1 answer
636 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 ...
magma's user avatar
  • 193
13 votes
0 answers
553 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 ...
GraffL's user avatar
  • 471
16 votes
1 answer
936 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 ...
Ricky's user avatar
  • 968
8 votes
2 answers
508 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 ...
burek's user avatar
  • 137
11 votes
1 answer
236 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 ...
mcd's user avatar
  • 213
20 votes
2 answers
704 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? ...
Jia Ming جيا ميڠ's user avatar
16 votes
1 answer
224 views

Extends vs including a typeclass argument

In the Lean mathlib, I see some places where a typeclass argument is included in a class definition, such as locally_finite_order. In other places, I see the "<...
Bolton Bailey's user avatar
30 votes
1 answer
675 views

In Lean, what do double curly brackets mean?

In Lean, explicit function arguments are enclosed in round brackets and implicit ones in curly brackets, as in this example: ...
Neil Strickland's user avatar