Skip to main content

Questions tagged [lean]

Lean is a theorem prover and programming language, based on the calculus of constructions with inductive types. For version-specific questions, also add the [lean3] or [lean4] tags.

Filter by
Sorted by
Tagged with
2 votes
1 answer
105 views

Is there any way to approximate noncomputable functions in Lean4?

As you may know, there are some definitions in lean4 that can't be evaluated due to the noncomputable tag. Is there any way to approximate their value in lean4? For ...
ArshakParsa 's user avatar
2 votes
1 answer
37 views

Proper LEAN_PATH environment variable value for Windows Lean Visual Studio project?

I have a Lean 4 test project in C:\Temp\MyProject I open with Visual Studio. In that directory, I have a Main.lean file. And, in ...
Jérôme Verstrynge's user avatar
7 votes
3 answers
200 views

Why is $\Bbb Z = \Bbb N$ independent of Lean?

In this answer, it is noted For a silly example, in ZFC with the usual encoding, $\mathbb{Z} \neq \mathbb{N}$, but in Lean it is well-known that this is independent. Of course in both ZFC or Lean, ...
Mike Battaglia's user avatar
5 votes
3 answers
965 views

Tools like leanblueprint for other proof assistants, especially Coq?

In my (relatively little) experience with Lean, one of the things I’ve appreciated most is the leanblueprint tool. For those not familiar with it, it’s a tool for planning a Lean development and ...
Peter LeFanu Lumsdaine's user avatar
2 votes
1 answer
75 views

What does "rintro rfl" do in LEAN?

Here is a block of LEAN code: ...
12121's user avatar
  • 175
0 votes
1 answer
47 views

Implication and Disjunction Classical Propositional Logic Proof

...
Jim Falkner's user avatar
0 votes
0 answers
23 views

How does one install new dependencies to a Lean 4 programatically e.g., adding aesop by editing lakefile.lean in bash?

I have a github repo at (note it's not a Lean 4 project): $HOME/learning_lean with a Lean 4 project at: ...
Charlie Parker's user avatar
11 votes
5 answers
2k views

How do real-world proof assistants bind variables and check equality?

There are many possible ways to represent syntax with variable binding, such as named variables, De Bruijn indices, De Bruijn levels, locally nameless terms, nominal type theories, etc. There are also ...
0 votes
2 answers
84 views

Proving `succ_mul` without using `nth_rewrite`

I'm trying level 3 in the multiplication world of the Natural Number Game. My proof is given below, but I am not satisfied with it since it uses nth_rewrite. This ...
Greg Nisbet's user avatar
  • 3,095
1 vote
2 answers
93 views

How to write a proof of n + 0 = n in Lean 4 using the built in definition of addition for Nats and not the theorem for Nat.add_zero?

I want to do the proof of n + 0 = n in Lean 4 using mathlib 4, my attempt: ...
Charlie Parker's user avatar
3 votes
2 answers
106 views

Offline install of Lean

I have fast internet, but my friend, who would like to install Lean on his computer, does not. What should I download to put on a USB stick for him? Any special installation instructions for such an ...
Chris Gray's user avatar
3 votes
1 answer
304 views

Why does `#check add_mul (R := ℕ)` return `add_mul : ∀ (a b c : ℕ), (a + b) * c = a * c + b *` instead of `add_mul : Prop`?

I don't understand why #check add_mul (R := ℕ) returns add_mul : ∀ (a b c : ℕ), (a + b) * c = a * c + b * c instead of ...
12121's user avatar
  • 175
1 vote
1 answer
72 views

Define maximum of matrix entries in Lean4

In Lean4 I would like to define a function max that finds the largest entry of an $n\times n$ matrix with entries in a ...
Strichcoder's user avatar
1 vote
1 answer
99 views

Applying universally quantified equalities to propositions

In Lean, given an equality eq: e0 = e1, one may rewrite either e0 or e1 with the other one ...
Jozef Mikušinec's user avatar
2 votes
1 answer
442 views

How does one import Natural numbers in Lean 4 -- unknown identifier 'ℕ'?

I found the definition of Nat's but lean still complains that it doesn't exist. Why is it? ...
Charlie Parker's user avatar
2 votes
1 answer
51 views

Pattern Matching on List x Fin

So, here is the example I'm working on: ...
redjamjar's user avatar
  • 165
3 votes
2 answers
138 views

Lean4: How to construct an HEq between dependent functions?

I have an extremely simple goal to prove: HEq (fun px rd => match px, rd with | Sum.inr _ppos, dir => dir) fun x => id The reason the match ...
André Muricy's user avatar
0 votes
1 answer
75 views

How does one define a structure with the ext theorem in Lean 4?

I get this error: unknown attribute [ext] and my code is literally a copy paste of the code from mathematics in lean: ...
Charlie Parker's user avatar
0 votes
1 answer
98 views

Given some proposition in Lean 4, how do we state a theorem saying that we want that property to hold a number of times?

I have a definition of the form in Lean 4: ...
Charlie Parker's user avatar
0 votes
1 answer
137 views

Can proof assistants reflect the informal notion of a “theory” as the formally logical notion of a “theory”?

Let us say that I wish to study and understand gauge symmetry using a formally verified mathematical programming language like Lean or Coq. Lean has many libraries you can import to express ...
Julius Hamilton's user avatar
1 vote
1 answer
172 views

Where does one find the keyword documentation for Lean4?

I find that Lean4 is rather hard to work to find keywords and related things. In coq the docs are pretty to search if I recall correctly. A quick search for Inductive send me to the grammer and lots ...
Charlie Parker's user avatar
3 votes
1 answer
194 views

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 projects (and a related issue). The official instructions don't seem to make it ...
Charlie Parker's user avatar
0 votes
0 answers
28 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., ...
Charlie Parker's user avatar
1 vote
2 answers
190 views

How does one create a lean project and have mathlib import work when not creating the lean project at the $HOME directory?

I want to create a lean project inside another folder besides the $HOME folder. So I was going through the official Creating a Lean project instructions on how to ...
Charlie Parker's user avatar
3 votes
1 answer
278 views

Determining why my proof depends on the axiom of choice

I would like to write constructive proofs in Lean 4, so I don't want my proofs to depend on Classical.choice, the axiom of choice. However, one of my proofs does, ...
Robin Green's user avatar
6 votes
2 answers
315 views

Lean and inaccessible cardinals

It seems well known that Lean's type theory is equiconsistent with ZFC + the existence of $n$ inaccessible cardinals for every $n>0$. Suppose I want to ensure that my lean proofs depend only on ZFC,...
Potato's user avatar
  • 161
0 votes
1 answer
172 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 ...
CrSb0001's user avatar
  • 145
2 votes
2 answers
263 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 ...
CrSb0001's user avatar
  • 145
1 vote
1 answer
134 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 ...
CrSb0001's user avatar
  • 145
3 votes
1 answer
149 views

Implementing and verifying algorithms for solving equations in Lean

In computer algebra systems, one can enter an equation and ask for integer solutions. Sometimes it is solved. But the output is not guaranteed to be correct. In Lean, one can formalize the solutions ...
Bogdan's user avatar
  • 33
2 votes
2 answers
215 views

Coq / Lean endpoint for GPT actions

I'm trying to produce Coq and Lean code using a custom GPT but I want GPT to try running its proof scripts (and revising them if they fail) before suggesting them to me (via gpt actions). Right now, ...
Rand00's user avatar
  • 233
1 vote
1 answer
154 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 ...
antilope's user avatar
2 votes
1 answer
179 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) ...
probablygrigsby's user avatar
0 votes
1 answer
147 views

How to reason with notations directly?

Intuitive notations are always a big boost when stating and proving things. Modern interactive theorem provers usually have some way of building syntactic sugars aside from their ordinary abstraction ...
yiyuan-cao's user avatar
-2 votes
1 answer
99 views

Lean predicate logic problem. existentially quantified proposition

I am trying to prove a theorem using lean and I am unsure on how to fix the rest of my code. I am trying to prove with these 2 premises h₁ : ∀ x, P(x) → Q(x), h₂ : ∃ y, P(y) ∨ Q(y) that ∃ z, Q(z). The ...
Emjay23's user avatar
2 votes
5 answers
461 views

LEM, the halting problem, the curry-howard correspondence -> deep connection?

I posted the following on the math stackexchange, but it occurs to me that this might be a more (or at least equally?) appropriate forum: It was recently said to me by a prominent mathematician, who I ...
user avatar
2 votes
1 answer
225 views

Are all LEAN tactics equivalent to applying some theorem?

I don't understand LEAN well enough, but from my rough understanding that tactics delete old pairs of conditions and goals and create new pairs of conditions and goals, it seems all tactics are ...
12121's user avatar
  • 175
7 votes
1 answer
556 views

Examples of theories where tactic language is required for simple proofs

I was always under the impression, that separate tactic languages were generally considered to be vital for writing long proofs. I see tactic languages as a kind of interpreted DSL to generate ...
uhbif19's user avatar
  • 177
2 votes
2 answers
110 views

Simplifying Array Access

I'm confused how to show the second example here: ...
redjamjar's user avatar
  • 165
7 votes
1 answer
707 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 ...
ch271828n's user avatar
  • 171
3 votes
0 answers
162 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 ...
Adomas Baliuka's user avatar
3 votes
1 answer
302 views

Understanding noConfusion

Data.List.getLast is defined as follows: ...
retonlage's user avatar
4 votes
2 answers
154 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 ...
Alex Byard's user avatar
2 votes
1 answer
325 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
2 votes
1 answer
165 views

Understanding Mathlib/MeasureTheory Notation

I want to understand Mathlib/MeasureTheory, and in particular I want to understand Mathlib/MeasureTheory/Integral. I'm having ...
Alex Byard's user avatar
0 votes
1 answer
85 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 ...
Alex Byard's user avatar
5 votes
1 answer
327 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 ...
Adomas Baliuka's user avatar
8 votes
1 answer
380 views

How does Lean `simp` tactic work?

The doc at https://leanprover-community.github.io/extras/simp.html says about simp: all it does is repeatedly replace (or rewrite) subterms of the form A by B, for ...
Weier's user avatar
  • 313
3 votes
1 answer
109 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
6 votes
1 answer
329 views

(Dis)Advantages of basing a proof assistant on CH correspondence?

Major proof assistants like Lean and Coq are fundamentally based on the Curry-Howard correspondence: propositions are encoded as types, quantified propositions are encoded as dependent types, proofs ...
Weier's user avatar
  • 313