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.

Filter by
Sorted by
Tagged with
6 votes
2 answers
120 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 ...
user avatar
  • 2,688
6 votes
1 answer
176 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: ...
user avatar
3 votes
2 answers
146 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 ...
user avatar
12 votes
0 answers
266 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 ...
user avatar
  • 431
22 votes
3 answers
312 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 ...
user avatar
10 votes
1 answer
143 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 ...
user avatar
  • 203
5 votes
0 answers
128 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 ...
user avatar
  • 3,833
6 votes
1 answer
60 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: ...
user avatar
19 votes
1 answer
275 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 ...
user avatar
  • 978
14 votes
1 answer
140 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 ...
user avatar
  • 664
14 votes
2 answers
175 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 ...
user avatar
25 votes
1 answer
280 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'...
user avatar
15 votes
1 answer
103 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 "<...
user avatar
22 votes
1 answer
147 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 ...
user avatar