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
1 vote
1 answer
81 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
341 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
47 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
112 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
59 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
73 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
131 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
76 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
2 votes
1 answer
90 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
21 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
107 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
252 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
258 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
91 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
190 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
116 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
114 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
1 vote
2 answers
188 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
  • 223
1 vote
1 answer
110 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
167 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
135 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
92 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
4 answers
367 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
211 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 ...
kid111's user avatar
  • 123
6 votes
1 answer
532 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
  • 167
2 votes
2 answers
105 views

Simplifying Array Access

I'm confused how to show the second example here: ...
redjamjar's user avatar
  • 165
7 votes
1 answer
524 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
2 votes
0 answers
136 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
251 views

Understanding noConfusion

Data.List.getLast is defined as follows: ...
retonlage's user avatar
4 votes
2 answers
145 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
319 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
158 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
66 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
230 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
309 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
105 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
319 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
2 votes
0 answers
196 views

Lean proofs for graph algorithms

I am new to lean but am interested in proving correctness of graph algorithms. Is there a repository/website that talks about a proof using lean of Dijkstra's shortest path algorithm, for example?
Simd's user avatar
  • 121
1 vote
1 answer
199 views

Prove an upper bound on the computation time of the Euclidean algorithm in lean4

I've heard that proof assistants like lean4 can formalize all the usual math. I'm interested to see how they formalize the complexity estimates of algorithms, since they are not often discussed ...
Kitamado's user avatar
  • 171
5 votes
1 answer
270 views

Programming challenge site for lean4

I recently discovered that Codewars supports lean language. https://www.codewars.com/ However, lean4 does not seem to be supported. Do you know of any programming challenge sites that support lean4? ...
Kitamado's user avatar
  • 171
3 votes
4 answers
2k views

Can we prove every provable statement with Lean?

This question was originally posted on math.stackexchange. People there directed me here. I just discovered Lean and using computers for stating and proving theorems. The first question that came to ...
Hatchi Roku's user avatar
0 votes
1 answer
121 views

increasing the universe level of a type in Lean by force

Given some term A : Sort u in Lean, is there a way to artificially increase the universe level and promote A to a term ...
Nico's user avatar
  • 722
1 vote
1 answer
96 views

Type of Sets with an Assocaitive Operation in Lean

This is probably a really simple question, but I am no able to find something in the Lean reference manual. I want to define a type of sets equipped with an associative operation. I have tried the ...
Nico's user avatar
  • 722
0 votes
1 answer
65 views

Minimizing proof environment change while proving in Lean

As a matter of (Lean) style, I would like to minimize changing the proof environment, and instead apply lemmas directly (to be "less imperative" and "more functional"). So, can ...
nicolas's user avatar
  • 193
1 vote
2 answers
224 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
6 votes
2 answers
197 views

How does one show termination of a function that is structurally recursive over a type T with subterms of type List T?

I've been having a bit of difficulty proving termination of a particular kind of function. I'm quite new to using Lean, so it's possible that what I'm missing is a language feature and not a technique,...
mobotsar's user avatar
  • 135
4 votes
2 answers
311 views

Reasoning about CwFs in a proof assistant

I've been chatting with folks on Mastodon about this but the perspective there is markedly Agda-focused, so I thought I'd ask here for some broader opinions. What tools/libraries are there for ...
Joey Eremondi's user avatar
0 votes
0 answers
238 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
138 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
4 votes
1 answer
355 views

Linear types in lean?

Is the LEAN type checker able to count the number of times a parameter is used in a function body? In Idris2 for comparison I might use (1 x:Nat) which then makes ...
Algeboy's user avatar
  • 147