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.

Filter by
Sorted by
Tagged with
0 votes
2 answers
49 views

How to write a proof of n + 0 = 0 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
1 vote
1 answer
60 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
2 votes
1 answer
64 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 ...
Neil Strickland's user avatar
3 votes
2 answers
125 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
1 vote
2 answers
131 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
0 votes
1 answer
105 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 ...
probablygrigsby's user avatar
3 votes
0 answers
149 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
4 votes
2 answers
148 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
320 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
159 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
73 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
2 votes
1 answer
82 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,...
amit9oct's user avatar
0 votes
0 answers
249 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
148 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
5 votes
1 answer
376 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?
Alex Byard's user avatar
4 votes
1 answer
455 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 ...
Alex Byard's user avatar
1 vote
1 answer
48 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?
Alex Byard's user avatar
4 votes
1 answer
113 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 ...
Alex Byard's user avatar
2 votes
0 answers
94 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 ...
Alex Byard's user avatar
0 votes
0 answers
39 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 ...
Alex Byard's user avatar
6 votes
2 answers
349 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?
Alex Byard's user avatar
4 votes
1 answer
1k 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 ...
Alex Byard's user avatar
1 vote
1 answer
95 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?
AgentSmith's user avatar
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 ...
Strichcoder's user avatar
4 votes
1 answer
377 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 ...
Strichcoder's user avatar
0 votes
1 answer
642 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:...
Ronald J. Zallman's user avatar
0 votes
1 answer
111 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? ...
user120404's user avatar
6 votes
2 answers
190 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 ...
Trebor's user avatar
  • 3,967
5 votes
1 answer
221 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: ...
user120404's user avatar
3 votes
2 answers
184 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 ...
Joachim Breitner's user avatar
13 votes
0 answers
555 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 ...
GraffL's user avatar
  • 471
23 votes
4 answers
506 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 ...
Dustin G. Mixon's user avatar
11 votes
1 answer
236 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 ...
mcd's user avatar
  • 213
8 votes
0 answers
284 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 ...
Jason Rute's user avatar
  • 8,685
6 votes
1 answer
112 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: ...
Neil Strickland's user avatar
22 votes
1 answer
551 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 ...
Wojowu's user avatar
  • 1,058
14 votes
1 answer
197 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 ...
Bubbler's user avatar
  • 674
15 votes
2 answers
445 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 ...
Joachim Breitner's user avatar
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'...
Dustin G. Mixon's user avatar
16 votes
1 answer
224 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 "<...
Bolton Bailey's user avatar
22 votes
1 answer
178 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 ...
Neil Strickland's user avatar