Skip to main content

# 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
Filter by
Sorted by
Tagged with
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 ...
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: ...
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 ...
1 vote
2 answers
287 views

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 ...
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 ...
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'...
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 "<...
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