Questions tagged [lean-mathlib]
Mathlib is Lean's Math Library. The library is hosted on the GitHub leanprover-community account. Do not use this tag for Lean the software. Do not use this tag for other math libraries of other proof assistants.
44
questions
1
vote
0
answers
45
views
Using HEq inside a structure
Here is a proof involving HEq which I can't manage. It's a cut down version of a problem I had while writing a functor ...
- 203
1
vote
1
answer
71
views
Lean Proving a Prop that has a match
I am working on making the surreal numbers in Lean from scratch. I came across a problem when trying to write proofs for propositions that are defined using match statements. I boiled down the problem ...
2
votes
1
answer
140
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 ...
- 21
1
vote
2
answers
142
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:
...
- 333
1
vote
1
answer
100
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 ...
- 193
2
votes
1
answer
81
views
Lean4 instance management
I have a group $G$ and $G$-sets $X$ and $Y$. I would like to let $G$ act on the type $(X\to Y)$ by the usual rule $(g\bullet u)(x)=g\bullet u(g^{-1}\bullet x)$. I define a ...
- 1,051
3
votes
2
answers
149
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 ...
- 41
1
vote
2
answers
287
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 ...
- 333
0
votes
1
answer
139
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 ...
3
votes
0
answers
179
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 ...
- 233
4
votes
2
answers
161
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 ...
- 506
2
votes
1
answer
343
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$...
- 313
2
votes
1
answer
168
views
Understanding Mathlib/MeasureTheory Notation
I want to understand Mathlib/MeasureTheory, and in particular I want to understand Mathlib/MeasureTheory/Integral. I'm having ...
- 506
0
votes
1
answer
97
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 ...
- 506
2
votes
1
answer
88
views
Converting Lean formulations of Lemmas to Coq formulation
I want to contribute to the repository MiniF2F (https://github.com/facebookresearch/miniF2F/tree/main) which has formal formulation of problems asked in Math Olympiads in different languages like Lean,...
- 21
0
votes
0
answers
290
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 ...
- 506
0
votes
2
answers
174
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 ...
- 506
5
votes
1
answer
442
views
Aesop Tactic in Lean
Simple question, but can someone explain the role of the aesop tactic in general, and as it pertains to SimpleGraph?
- 506
4
votes
1
answer
592
views
Graph Theory in Lean
I can't find an implementation of graph theory in Mathlib. Am I overlooking the file, or is it particularly difficult to do this, or has no one been interested in taking this on yet?
If it hasn't been ...
- 506
1
vote
1
answer
57
views
inherit_doc attribute Lean 4
This is a rather simple question which I cannot find an answer to in the Lean 4 API or anywhere else online. What does the @[inherit_doc] attribute do?
- 506
4
votes
1
answer
129
views
Auxiliary Typeclasses in Lean
It's a common theme in Mathlib to use some auxiliary typeclass to define the one we actually want to use. For example, to define PseudoMetricSpace we use the ...
- 506
2
votes
0
answers
104
views
Must-read Lean 4 Mathlib Files
I am starting to understand Lean 4, but I feel a bit overwhelmed by the amount of dependencies for most files in Mathlib. To become more familiar, particularly with the module typeclass, I decided to ...
- 506
0
votes
0
answers
48
views
General Relativity in Mathlib for Class Project
I'm interested in writing a general relativity folder for Lean 4, along the lines of Wald's book. Has this been done before? Since this is for a class project, I want to avoid using less elementary ...
- 506
6
votes
2
answers
371
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?
- 506
5
votes
1
answer
2k
views
Lean 4 Importing into VSCode
I am working on Lean4 for a class project. I want to import some of mathlib4, but I keep getting "unknown package". I got Lean4 through the VSCode extension on Windows. How do I import ...
- 506
1
vote
1
answer
116
views
Question about the tactic "obtain"
I am having difficulty activating the tactic obtain. Is it part of mathlib and where is its exact location?
- 113
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 ...
- 193
4
votes
1
answer
415
views
Error when starting a project in Lean, 'binary package was not provided for 'windows''
after taking a break of half a year I would like to get back to proving things in Lean. I followed the instructions to install a fresh lean project. When I do
...
- 193
0
votes
1
answer
714
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:...
0
votes
1
answer
112
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?
...
- 163
6
votes
2
answers
194
views
Defining essentially unique objects with typeclasses
I noticed that in Lean, the localization of rings (which is unique up to isomorphism) is defined as a predicate is_localization.
I am not an expert in Lean, and I'm ...
- 4,087
5
votes
1
answer
227
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:
...
- 163
3
votes
2
answers
186
views
Like arbitrary, but for nonempty instead of inhabited
I wrote some code that used a [inhabited ι] assumption, and then used arbitrary ι in the proof. The mathlib linter then ...
- 1,934
13
votes
0
answers
652
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 ...
- 471
23
votes
4
answers
531
views
To what extent is formalized mathematics publishable?
I am interested in contributing to the formalization of mathematics, but I don't know the extent to which such activities are publishable. Here are some questions in this vein:
How can one determine ...
- 981
11
votes
1
answer
256
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 ...
- 213
8
votes
0
answers
320
views
What would a fully classical and fully univalent ITP and library look like?
Consider two developments in dependent type theory:
Lean’s mathlib library (as well many other ITP libraries) is unashamedly fully classical. There is no ...
- 9,653
6
votes
1
answer
116
views
Lean: how to use the refine_struct tactic for commutative ring structures?
Suppose I want to make bool (i.e. the type {ff,tt} of boolean values) into a commutative ring. The following works:
...
- 1,051
22
votes
1
answer
614
views
How hard is computing integrals in Lean?
Are there tools in mathlib which let you give computations of integrals which would roughly follow standard methods for solving them? For now let me restrict attention to some undergrad-level ...
- 1,058
14
votes
1
answer
207
views
Proof review: Sum of nCk over antidiagonal = Fibonacci
Theorem to prove:
The sum of the binomial coefficients over an antidiagonal is a Fibonacci number. More specifically, the $n$th antidiagonal sums to the $n+1$th Fibonacci number, where the ...
- 684
15
votes
2
answers
531
views
What is in an olean file?
It seems Lean can produce .olean files from Lean files, and the mathlib project provides an infrastructure to download olean files, which seems to allow the ...
- 1,934
32
votes
1
answer
1k
views
What will happen to mathlib when we transition to Lean 4?
Today, there's an exciting large-scale effort to digitize mathematics in Lean's mathematics library mathlib.
I understand that a transition to Lean 4 is looming. I'...
- 981
16
votes
1
answer
258
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 "<...
- 716
22
votes
1
answer
181
views
How to track backwards-incompatible changes in mathlib?
I am trying to update a large body of Lean code to work with the current version of mathlib. This is difficult because there have been a large number of backwards-incompatible changes even since I ...
- 1,051