Skip to main content
36 votes

What will happen to mathlib when we transition to Lean 4?

BIG UPDATE The port to Lean4 is officially complete. There is a couple changes that we are still hoping to officially put into mathlib3 before moving it into ...
It'sNotALie.'s user avatar
  • 1,445
17 votes

How to track backwards-incompatible changes in mathlib?

The mathlib commit log serves as a de facto changelog. Since the project updates far too frequently to keep a traditional changelog, a good method if you know approximately when breaking changes ...
Rob Lewis's user avatar
  • 593
14 votes
Accepted

Proof review: Sum of nCk over antidiagonal = Fibonacci

I'll first go through piece-by-piece and suggest some local improvements. For the induction principle, when you find yourself doing intros as the first step of a ...
Kyle Miller's user avatar
13 votes
Accepted

Extends vs including a typeclass argument

Section 2.2 of Anne Baanen's recent paper Use and abuse of instance parameters in the Lean mathematical library gives a very nice explanation of this, referring to them as "unbundled subclasses&...
Rob Lewis's user avatar
  • 593
13 votes
Accepted

What is in an olean file?

(My answer is for Lean 3. I don't know how .oleans changed in Lean 4.) Also, see this discussion on the Lean Zulip. TL;DR An ...
Jason Rute's user avatar
  • 8,685
12 votes

To what extent is formalized mathematics publishable?

The ITP and CPP conferences regularly accept papers on mechanised mathematics. See previous programs at, for example: ITP 2016, where there were among others, papers such as A Formal Proof of Cauchy’...
Michael Norrish's user avatar
11 votes

How hard is computing integrals in Lean?

I'm going to inflate Mario's comment to an answer: You can absolutely write tactics in Lean to do this. What you'll be doing is creating a large part of a CAS, but as a Tactic. This would be largely a ...
Jacques Carette's user avatar
10 votes
Accepted

Like arbitrary, but for nonempty instead of inhabited

What you're seeing here is the behavior of the inhabited_nonempty linter: ...
Eric's user avatar
  • 971
8 votes
Accepted

Explicit vs implicit universes in lean

Type* is just a shorthand for Type _, where the _ is a wildcard (or more accurately, a ...
Eric's user avatar
  • 971
8 votes
Accepted

Defining essentially unique objects with typeclasses

The question is about declarative versus computational formalization. In the declarative style we characterize a “thing” by stating conditions, quite often universal properties, that determine it up ...
Andrej Bauer's user avatar
  • 9,154
7 votes
Accepted

Error when starting a project in Lean, 'binary package was not provided for 'windows''

You need to update elan because of upstream changes at github. Try elan self update. If this doesn't work then reinstall ...
Kevin Buzzard's user avatar
6 votes

Like arbitrary, but for nonempty instead of inhabited

The most convenient option is classical.arbitrary (or nonempty.some if your nonempty α is an ...
Astaulphe's user avatar
6 votes

To what extent is formalized mathematics publishable?

I don't know if there are well-established rules yet. My guess would be that it depends on how significant the differences are between X and Y. If the mathematics is new, then of course it can be ...
Mike Shulman's user avatar
  • 3,060
5 votes
Accepted

Are there squeeze-versions of ring and abel?

Both ring and abel produce a proof term that is going to be about as good as you could hope for from a putative ...
Kim Liesinger's user avatar
5 votes
Accepted

Aesop Tactic in Lean

SimpleGraph is a definition of a "simple graph" in the mathlib4 library. The API for SimpleGraph uses ...
Kim Liesinger's user avatar
5 votes
Accepted

Auxiliary Typeclasses in Lean

This is done so that formalization matches mathematical practice. Defining only PseudoMetricSpace directly with dist would ...
Andrej Bauer's user avatar
  • 9,154
5 votes
Accepted

Lean: how to use the refine_struct tactic for commutative ring structures?

What changed since November 2021​​​ is that comm_ring got several new data members in order to resolve various diamond issues. ...
Mario Carneiro's user avatar
5 votes

To what extent is formalized mathematics publishable?

I know I am almost two years late in the game, but a new journal dedicated to publishing articles about formalized mathematics, and aimed at mathematicians rather than computer scientists, has just ...
Filippo Alberto Edoardo's user avatar
5 votes

To what extent is formalized mathematics publishable?

I once asked a similar question in the Coq Zulip chat (regular link, no-login-needed link). This was my takeaway: If your formalization is interesting as code, you can publish it from that angle. In ...
Ana Borges's user avatar
4 votes
Accepted

Define a new Type in Lean: Tensor power of vector space

As of about two hours after you asked this question, this exists in mathlib as tensor_power, with notation ⨂[ℂ]^n ℋ for the ...
Eric's user avatar
  • 971
4 votes
Accepted

Differential Topology and Differential Geometry Porting to Mathlib4

The answer to any questions of the form "What is the status of mathlib3's [X] in mathlib4" can be answered with the porting dashboard, where you can search for file based on its mathlib3 ...
Eric's user avatar
  • 971
4 votes
Accepted

inherit_doc attribute Lean 4

The syntax is @[inherit_doc declaration_name]: it adds the doc-string of declaration_name to the following declaration. In the ...
damiano's user avatar
  • 156
4 votes

Type Theory Lean 3 to Lean 4

As already commented by Sebastian Ullrich, there are a few small changes to the Lean 4 kernel, detailed in his PhD thesis. Now, that it is done (and has been for a few months), I want to make sure it ...
Jason Rute's user avatar
  • 8,685
4 votes
Accepted

Lean4 instance management

A common solution to this problem is to define a type synonym with its own instances. You can find this throughout mathlib, for example with Multiplicative and <...
Kyle Miller's user avatar
3 votes

Graph Theory in Lean

I guess it would be pretty fun and pretty efficient to implement a Graph library on top of AC-sets following AlgebraicRewriting.jl's lead. Lots of work though... But might be possible to leverage ...
Alex Chichigin's user avatar
3 votes

Differential Topology and Differential Geometry Porting to Mathlib4

The next step towards porting geometry/manifolds to Lean 4 is porting the file cont_mdiff, see https://github.com/leanprover-...
Yury Kudryashov's user avatar
3 votes
Accepted

Understanding Mathlib/MeasureTheory Notation

You could start with reading the relevant chapter of Mathematics in Lean. You can also right click and choose "Go to definition" when you see an unknown notation or definition.
Patrick Massot's user avatar
3 votes
Accepted

How does one create a lean project and have mathlib import work when not creating the lean project at the $HOME directory?

Your screenshot indicates that you are opening VS Code in $HOME. You need to open the root directory of the project folder instead. For example on the command line ...
Kevin Buzzard's user avatar
3 votes

Define maximum of matrix entries in Lean4

In Lean, the first two arguments to Matrix aren't actually integers m x n that define the size of the matrix, as you've now found out -- they are the types that let you index into the matrix. For all ...
Mark Pock's user avatar
2 votes

Converting Lean formulations of Lemmas to Coq formulation

First, I would like to say that translating the MiniF2F benchmark to Coq is important and someone should do it, so thank you for raising awareness of this. There is no good automatic way to translate ...
Jason Rute's user avatar
  • 8,685

Only top scored, non community-wiki answers of a minimum length are eligible