Questions tagged [lean-mathlib]
Mathlib is Lean 3'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.
35
questions
2
votes
0
answers
105
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 ...
- 173
4
votes
2
answers
124
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 ...
- 456
1
vote
1
answer
294
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$...
- 273
2
votes
1
answer
152
views
Understanding Mathlib/MeasureTheory Notation
I want to understand Mathlib/MeasureTheory, and in particular I want to understand Mathlib/MeasureTheory/Integral. I'm having ...
- 456
0
votes
1
answer
39
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 ...
- 456
2
votes
1
answer
72
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
177
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 ...
- 456
0
votes
2
answers
110
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 ...
- 456
4
votes
1
answer
237
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?
- 456
4
votes
1
answer
247
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 ...
- 456
1
vote
1
answer
37
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?
- 456
4
votes
1
answer
95
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 ...
- 456
2
votes
0
answers
64
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 ...
- 456
0
votes
0
answers
34
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 ...
- 456
5
votes
2
answers
307
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?
- 456
3
votes
1
answer
658
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 ...
- 456
1
vote
1
answer
68
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
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 ...
- 183
4
votes
1
answer
289
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
...
- 183
0
votes
1
answer
432
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:...
- 381
0
votes
1
answer
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?
...
- 163
6
votes
2
answers
186
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 ...
- 3,688
5
votes
1
answer
215
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
174
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,794
13
votes
0
answers
424
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
22
votes
3
answers
410
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 ...
- 961
11
votes
1
answer
220
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
6
votes
0
answers
229
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 ...
- 7,240
6
votes
1
answer
103
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:
...
- 997
21
votes
1
answer
469
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,038
14
votes
1
answer
183
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 ...
- 674
14
votes
2
answers
375
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,794
31
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'...
- 961
16
votes
1
answer
166
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 "<...
- 686
22
votes
1
answer
172
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 ...
- 997