mathlib

Stream: lean4

[Kenny Lau]

is there a mathlib for lean 4 yet? as in, a place to port lean 3 mathlib to

[Kenny Lau]

@Mario Carneiro I heard that you're working on logic.basic

[Mario Carneiro]

working is a strong word

[Mario Carneiro]

There is certainly no place to port mathlib yet, and I think that's still premature

[Mario Carneiro]

I think for the present we should be doing single file experiments

[Kenny Lau]

what do you have now?

[Mario Carneiro]

~nothing

[Kenny Lau]

Well at least it would be better if there's an empty repository on github that has Lean 4 environment

[Aaron Anderson]

Is it too early to start threads to discuss design changes to mathlib that could be implemented during the port?

[Kenny Lau]

I think we should get logic.basic working first

[Bryan Gin-ge Chen]

Zulip threads are cheap, so I would say no; it's not too early. Proposals with supporting evidence from code experiments will of course be more useful, and it will also take some time before enough people are comfortable with Lean 4 for there to be much feedback.

(I agree that porting logic.basic is a reasonable first milestone.)

[Kevin Buzzard]

It's the logic.basic game!

[Johan Commelin]

Johannes Holzl used to warn against mixing porting and design changes. He said you would fail on both parts if you tried that.

[Eric Wieser]

I can't see full porting ever happening unless we either:

• Work out a compatibility layer, like how the python ecosystem ran against both 2 and 3 with the same source code.
• Freeze the lean3 mathlib
• Automate the translation (a la 2to3.py)

Is there a path I'm missing?

[Kevin Buzzard]

Manual porting over the next few years

[Daniel Selsam]

I am planning to implement a preliminary version of the tool Leo suggested yesterday, with the hope that it will be easy enough for the community to tweak and extend as desired.

[Bryan Gin-ge Chen]

(For reference, here's the relevant timestamp to Leo's talk)

[Kevin Lacker]

which tool do you mean Daniel - a tool to let include both lean 3 and lean 4 files in the same build, or a tool to export lean 3 things to lean 4?

[Daniel Selsam]

Kevin Lacker said:

which tool do you mean Daniel - a tool to let include both lean 3 and lean 4 files in the same build, or a tool to export lean 3 things to lean 4?

1. add functionality to Lean3 to allow exporting the declarations plus metadata such as typeclass instances and notation in (say) a foo.lean3port file for each foo.lean
2. a stand-alone executable that transforms .lean3port files into the .olean format that Lean4 can import.

[Reid Barton]

Aaron Anderson said:

Is it too early to start threads to discuss design changes to mathlib that could be implemented during the port?

I'd say instead: it's not too late to start threads about design changes that could be implemented before the port :upside_down:

[Reid Barton]

@Gabriel Ebner had a similar tool described here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Importing.20mathlib.20into.20Lean.204/near/187561178

[Eric Wieser]

Presumably we'll want a tool in both directions if we're starting from logic.basic - otherwise we'd have to start at the other end

[Eric Wieser]

That is, importing lean 4 data into lean3 source files

[Daniel Selsam]

Reid Barton said:

Gabriel Ebner had a similar tool described here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Importing.20mathlib.20into.20Lean.204/near/187561178

Thanks, looking at it now. It seems like the two things missing (besides all the tweaks I wasn't planning to add) are:

• don't require a monolithic import, and instead do this for each file individually
• export more metadata, in particular instances and notation

[Eric Wieser]

Is "exporting instances" anything other than exporting attributes?

[Gabriel Ebner]

My importer tool actually handles classes, instances, and simp lemmas. (There's a separate text file for the additional metadata).

[Gabriel Ebner]

The hard parts are:

1. Recursors are now different. (The construction of the old recursor is not hard, but you to invent a new name, etc.)
2. I think it's important to map at least some core definition to the Lean 4 equivalent, such as natural numbers, logical constants, decidability, etc. Otherwise the imported library is basically impossible to use. A lot of stuff maps directly, but it's a chore to list all the new names.
3. However many definitions in core were already different when I wrote the tool. Now the core library has diverged even further. (Think HasCoe, or numerals, etc.)
4. Some definitions no longer check because of subtle changes in the type checker. (Think large numerals, e.g. in unsigned.) This should be trivial to fix when porting manually, but in an automatic tool it's a nasty curveball.

[Kenny Lau]

my current translation of the very beginning of logic.basic:

universes u v

/-- Ex falso, the nondependent eliminator for the `Empty` type. -/
def Empty.elim {C : Sort u} (t : Empty) : C := nomatch t

instance : Subsingleton Empty := ⟨λ a => a.elim⟩

instance {α : Type u} {β : Type v} [Subsingleton α] [Subsingleton β] : Subsingleton (α × β) :=
⟨λ ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ => congr (congrArg _ $ Subsingleton.elim _ _) (Subsingleton.elim _ _)⟩

instance : DecidableEq Empty := λa => a.elim

instance instSortInhabited' : Inhabited (Inhabited.default : Sort u) := ⟨PUnit.unit⟩

instance decidableEqOfSubsingleton {α : Sort u} [Subsingleton α] : DecidableEq α :=
fun a b => isTrue (Subsingleton.elim a b)

@[simp] theorem eqIffTrueOfSubsingleton [Subsingleton α] (x y : α) : x = y ↔ true :=
⟨λ _ => ⟨_⟩, λ _ => Subsingleton.elim x y⟩

[Kevin Buzzard]

Porting has officially begun :D

[Adam Topaz]

So where's the repo? :smile:

[Bryan Gin-ge Chen]

Rather than creating a new community repo and reinviting everyone, for now I think we could create one (or several) orphan branches in the mathlib repo for Lean 4 experiments. These branches won't share any history or files with the Lean 3 mathlib (so CI won't run on them).

Instructions (copied from this SO post):

git checkout --orphan my_lean4_experiment
git rm -rf .
<do work>
git add your files
git commit -m 'Initial commit'

[Bryan Gin-ge Chen]

Then anyone can add commits to these branches as usual. leanproject get-cache won't work on these branches (until we set up some kind of CI), so anyone checking out such a branch will have to compile everything themselves.

[Bryan Gin-ge Chen]

(Feel free to point out reasons why this might be a terrible idea...)

[Alex Peattie]

If there's no CI/olean compilation concerns, I guess a Lean 4 mathlib repo could theoretically use the "normal" model for a Github repository. E.g. a repo with the maintainers invited, but then people work on forks + PRing rather than pushing their branches to the main repo? Which would mean no worries about reinviting everyone? Although I think orphan branches is a certainly clever approach if the preference is to avoid a new repo :smile:

[Daniel Selsam]

Has anyone made a back-of-the-envelope estimate of how much time it would take to just port Mathlib manually, bottom-up? Here is a heavily-simplified first attempt:

Assuming:

• 50,000 theorems
• 100 collaborators
• X minutes on average to port a theorem (this has high variance)
• 40 hour work-weeks

It would take:

• 500 theorems per person
• 500 * X minutes per person
• 500 * X / (60 * 40) weeks in total

After an initial investment to write Lean3-parity tactics/automation in Lean4 (which will presumably be necessary anyway), what would be a good estimate for X? 2? 5? 10? Even if X is 10, the porting would only take two weeks under this model. Even if a better model predicted 2 months, it might still be worth just pulling off the band-aid. Note: I am not suggesting this approach, only floating the idea.

[Huỳnh Trần Khanh]

I think we should be using some sort of automation, maybe parse the current mathlib into some sort of abstract syntax tree and then visit that syntax tree to emit Lean 4 code. https://blog.isquaredsoftware.com/2018/11/git-js-history-rewriting/

[Huỳnh Trần Khanh]

At the end of the day there would many steps that are purely mechanical and doing them by hand would be a waste of time.

[Daniel Selsam]

Yes, there is a lot that could be done automatically, though I expect the porting time will be dominated by the time it takes to fix the tactic scripts that (even after syntactically adjusting them) no longer work for subtle reasons.

[Jason Rute]

As someone who has written automation to parse proofs into abstract syntax trees, it is really hard to do. Lean's grammar is dynamic and only Lean can truly parse Lean. One option is to modify the current C++ Lean 3 parser to output the needed information.

Or, we were able to get pretty far by hacking into to parts of the Lean parsing framework and writing a light weight parser to get the rest of the way there. (It would also be possible to build on the current C++ Lean 3 parser to get this data as well.) I'm happy to share what we have when it's ready. We don't have ASTs for the whole file, just for tactic proofs and we don't parse expressions (which one would have to change because of capitalization changes). We just store the expressions as strings right now. I'm not sure if this would be helpful or not (especially in light of Daniel's comments).

[Joe Hendrix]

I'm wondering how feasible it would be to adopt an incremental approach where files in Lean 3 are incrementally "frozen" in Lean 3 and then ported to Lean 4. Once a given file is done, you shouldn't merge any PR changes into those files, but before then, it's ok to keep working on the Lean 3 versions. If you are predominantly working in certain files, then you could migrate to Lean 4 once they are ported. A file would only be eligible for freezing after all it's imports are.

[Huỳnh Trần Khanh]

That sounds a lot like the "strangler pattern".

[Daniel Selsam]

@Joe Hendrix One risk for any incremental approach is a bad Nash-equilibrium. I fear that individuals may not have sufficient incentive to invest heavily in Lean4 until they are confident that others will as well. In the 'pulling off the band-aid' approach, the community-optimal incentives could be achieved immediately by a community decision to freeze mathlib3 and to port to Lean4 before resuming business-as-usual.

[Joe Hendrix]

I was thinking kinda thinking that it would be good to let people interested in formalizing particular theories continue to do so while the more fundamental building blocks (e.g., decision procedures, logical foundations) are ported. The collective community decision though would be that Lean 3 versions are not to be updated for any reason once the Lean 4 porting of those versions is underway.
There could be a long tail of porting various particular contributions over with this though, so maybe there would be a deadline associated with freezing the entire codebase.
I'm not familiar with the strangler pattern, but I wasn't thinking about intermingling the ability to use Lean 3 within Lean 4 (or vice versa).

[Johan Commelin]

@Daniel Selsam the problem with your calculation is that it only works if you can port file xyzzy even though you don't know what its ported dependencies foo, bar, and quux look like. You can do it with 100 people in two weeks if you can parallelise the tasks. But I don't know if that is true.

[Johan Commelin]

We had a lintsprint two months ago. That worked well, with say 10-15 people contributing several PRs a day. But there were no interdependencies between those PRs.

[Johan Commelin]

So, if we can get lean 4 to work with special .lean3olean_plus_mathlib_metadata files, then we might be able to parallelise the porting effort.

[Johan Commelin]

Also, as warned above, porting would need to be very very strict, otherwise the parallelism will break. Everytime you see some bad design, leave a comment, but copy it faithfully. People importing your file will thank you later.

[Johan Commelin]

Daniel Selsam said:

Assuming:

• 50,000 theorems
• 100 collaborators
• X minutes on average to port a theorem (this has high variance)
• 40 hour work-weeks

It would take:

• 500 theorems per person
• 500 * X minutes per person
• 500 * X / (60 * 40) weeks in total

Also, I don't think 100 people will invest 2 weeks of 40 hours in porting stuff. In Feb/March I can probably invest 3 full weeks, but I guess I'm an exception. So it will probably be more like 10 people working for 20 weeks... and then, I don't have 20 weeks that I can work nonstop on this project.

[Patrick Massot]

I guess the olean export/import is what is meant to allow parallelism. But I also think that some kind of automatic preliminary translation of statements would be nice (tactic proofs are probably hopeless and for term proofs we want to use the new features of Lean 4 to kill @ _ _ _ _).

[Rob Lewis]

My two cents here:

Some of us remember the old days when Lean was always changing underneath us, and we all know the "bump Lean to 3.24.0c" PRs to mathlib. These can be painful, and Lean 4 is brand new and presumably in flux. This is fine, even good. It's a sign the system is improving. But it adds tremendously to the cost of a port.

[Rob Lewis]

I don't think we should start a full port now, or even necessarily soon. It's time to experiment. And there are a number of experiments to do, all somewhat independent.

[Rob Lewis]

One is what Leo suggested in his talk: import Lean 3 mathlib with metadata and try to build on that, or port files at the top of the import hierarchy. This gives very important information about how Lean 4 features will scale. There was a lot about Lean 3 that we didn't learn until mathlib got big.

[Rob Lewis]

This is a really important experiment but I'm skeptical about it as a long-term survival strategy for mathlib. IMO the Frankenstein approach will be harder to maintain and much harder for new contributors to wrap their heads around. The community development style is an essential part of mathlib and if we arrive at something that we can't teach newcomers, we've lost the game.

[Rob Lewis]

Two is what people started yesterday, just start porting things from the ground up. Learn Lean 4 syntax and bug hunt on smaller proofs. This is totally independent of the first approach. As I said, I think it's too early to dump everyone's full effort into doing this. But carving out an initial chunk -- logic.basic, some of algebra, core pieces of data -- will be really helpful, especially to see the effects of the inevitable changes to Lean 4.

[Rob Lewis]

Three, there's the 20k loc in tactic. Any kind of automated porting here seems hopeless. Many mathlib tactics are basically just linguistic things (obtain, set, etc) that might even be two-line macros in Lean 4. ring, linarith, slim_check, etc will be hard to port. (Leo said he plans to implement a version of linarith himself at some point.) The current omega is almost certainly dead. For a native Lean 4 mathlib, we need versions of most of this. Porting tactics isn't completely independent of the second approach, but I think it can be started independently. And as before, we should experiment with metaprogramming before committing to porting the big stuff.

[Rob Lewis]

So I'd like to see three experiments done in parallel and independently. These can help us in the future but none is expected to be the future. Lean 3 mathlib development can continue in Lean 3, albeit likely at a slower pace if people are directing their time to the porting effort. After some iteration on these experiments, we'll have a better idea how to approach a full port. In particular we'll have more accurate numbers for Daniel's time estimate.

[Rob Lewis]

(Sorry for the essay!)

[Patrick Massot]

Don't forget to add experimentation with rebuilding the basic algebraic hierarchy (without proving any lemma) using the structure command provided by Lean4 or a new new structure command somewhat simulating the old structure command using the new one. Or even try to rebuild it using unification hints!

[Gabriel Ebner]

I mostly agree with Rob, except that the critique of Frankenlean's monster maybe misses the point a bit. The motivation behind a hybrid Lean 3 / Lean 4 mathlib is as a viable temporary transition strategy. Porting mathlib is gonna take a few months. We know from linting sprints that we can organize incremental library cleanups. I am not sure we can pull off having two separate repositories.

[Rob Lewis]

I don't see how we achieve a full port top-down, but I'd be happy to be proven wrong.

[Eric Wieser]

I fear the rate at which mathlib is ported will be slower that the rate at which the lean3 version grows - so a multiple repository approach seems like it wouldn't work, and a hybrid approach is the only option.

[Eric Wieser]

Can we strive for a bottom-up port instead?

[Alex J. Best]

Eric Wieser said:

I fear the rate at which mathlib is ported will be slower that the rate at which the lean3 version grows - so a multiple repository approach seems like it wouldn't work

I wonder if there are some areas of interest to mathlib that are not well represented in mathlib so far (and so have few serious dependecies). People could start working on some of these from almost nothing in a mathlib 4, such projects might be a fun way for the community to learn lean 4 that isn't just porting existing work.

[Johan Commelin]

numerical analysis?

[Johan Commelin]

see the undergrad page, there are several sections that are just empty

[Mario Carneiro]

Eric Wieser said:

I fear the rate at which mathlib is ported will be slower that the rate at which the lean3 version grows - so a multiple repository approach seems like it wouldn't work, and a hybrid approach is the only option.

Once the porting gets far enough, it will be stable enough that people can feel comfortable writing new things in lean 4 mathlib, so the rate of lean 3 mathlib contributions will plateau and eventually dwindle

[Mario Carneiro]

But I definitely think that porting will take far too long for a global freeze to be viable

[Mario Carneiro]

Freezing at a file level is maybe doable, although I don't think it's particularly necessary, since the changes that happen to a given file are usually pretty low frequency. We have done lint sprints and other refactorings at about this level of disruptiveness already in the past

[Sebastien Gouezel]

Mario Carneiro said:

But I definitely think that porting will take far too long for a global freeze to be viable

Once all tactic files and all basic algebra files are ported, I wouldn't be surprised if the port were essentially mechanical. Maybe I'm too optimistic, but I guess we will stumble all the time on the same issues, so once we know how to fix these I don't see why it wouldn't be pretty smooth.

[Mario Carneiro]

I think it is definitely worth the time to set up the means to make it as mechanical as possible, but I don't think we will be able to reduce the manual part of the porting to zero. A few files a day seems like an upper limit on the amount of work one person could get done if it's all going smoothly, so together with the PRs and coordination I think a few months sounds about right

[Simon Hudon]

In terms of new designs for mathlib, after the port, it would be valuable to move tactics into a separate packages so that we can run them in mathlib in compiled form. (unless Leo implements just-in-time compilation) That will likely be a big change.

[Kevin Lacker]

in my experience with porting projects, they fail not when there is too much overall work, but when there are 2 or 3 critical things that are so hard to port, the people working on it eventually give up and nobody wants to try any more. so I am curious what are the hardest parts of mathlib to port, that are critical for mathlib. is it complex but commonly used tactics like ring, omega, simp, linarith, etc?

[Joe Hendrix]

I haven't thought through the implementation, but it seems like it should be possible to compile tactics in one module and use the compiled version in other modules without a JIT. I think this would result in using the compiled versions in most cases.

[Bryan Gin-ge Chen]

Lean 4 has a simplifier, but all the other tactics you mentioned will have to be ported.

[Mario Carneiro]

For most tactics, I expect that we can port them just like we port other things. That said I would bet that we want to make more significant changes to some of them: omega needs to be rewritten, simp will be rewritten, linarith might be rewritten

[Yakov Pechersky]

Should mathlib porting guidelines make a firm statement about set_option autoBoundImplicitLocal false?

[Mario Carneiro]

What's it mean?

[Yakov Pechersky]

Consider the following: https://gist.github.com/shingtaklam1324/7451d7e329aa32efd42dd49d784ac8a5#file-algebra_groups_defs-lean-L15

[Yakov Pechersky]

The u is coming from the fact that it is a lowercase letter, and can be inferred, so it is.

[Mario Carneiro]

I would say use it freely

[Yakov Pechersky]

As remarked on here https://leanprover.github.io/lean4/doc/autobound.html?highlight=lower#auto-bound-implict-arguments

[Mario Carneiro]

If it's possible, I want to bring back Sort* via notation

[Mario Carneiro]

I think, as long as it's still basically making the right guesses, we should use Sort* or Type* wherever possible, because it makes universe errors less likely

[Yakov Pechersky]

The bottom snippet in https://leanprover.github.io/lean4/doc/typeobjs.html?highlight=type%20_#types-as-objects is about Type* or Sort*

[Mario Carneiro]

Right, we're going to need a mathlib prelude anyway and this should go in it

[Mario Carneiro]

For times when it's necessary to use explicit universes, it's marginally more convenient to use implicit universe arguments than universes u v which is mostly noise

[Kenny Lau]

https://github.com/kckennylau/mathlib4/blob/master/src/logic/basic.lean

[Kevin Buzzard]

Is that the official mathlib port repo? :D

[Kenny Lau]

it’s my unofficial mathlib port repo

[Kevin Buzzard]

You'd better document your instances or the linter will complain

[Kevin Buzzard]

In fact @Jesse Michael Han was telling me that we should document all theorems too, because then AI will be able to learn better about mathematical natural language

[Eric Wieser]

Maybe then we can train gpt to insert a comment explaining in natural language why it rewrote add_comm repeatedly

[Kevin Buzzard]

"Because it's there"

[Eric Wieser]

More seriously though, that knowledge would definitely help build a more powerful method for searching theorems in the docs

[Jesse Michael Han]

Kevin Buzzard said:

In fact Jesse Michael Han was telling me that we should document all theorems too, because then AI will be able to learn better about mathematical natural language

yes, this would be extremely useful as training data for informal-to-formal machine translation

[Eric Wieser]

Perhaps vice versa too, given the discussion in the teaching panel about transitioning to paper from lean

[Mohamed Al-Fahim]

(deleted)

[Alena Gusakov]

I wonder if there are some areas of interest to mathlib that are not well represented in mathlib so far (and so have few serious dependecies).

graph theory and combinatorics!

[Kenny Lau]

@Alena Gusakov so are you going to work on graph theory in Lean 4

[Alena Gusakov]

I might

[Alena Gusakov]

I've just barely started wrapping my head around how Lean 3 works but it might be worth it for me to start experimenting w/ Lean 4 since we're planning to port anyway

[Kenny Lau]

let's go

[Nasos Evangelou-Oost]

@Huỳnh Trần Khanh thank you. i am interested in experimenting with some category theory stuff in lean. is anything available yet for lean4? how long would you expect for mathlib to be upgraded for lean4? as someone who has never uesd lean before, would you suggest i stick to lean3 for now or to try to port myself the relevant bits from mathlib to lean4?

[Huỳnh Trần Khanh]

@Nasos Evangelou-Oost I'd say stick with Lean 3 for now. Lean 4 is still unstable.

[Huỳnh Trần Khanh]

There was a recent soundness bug. Already fixed, but who knows if there are still other bugs lurking somewhere.

[Mario Carneiro]

more importantly, it doesn't have many of the features of lean 3 yet, only the ability to eventually write them. This is going to take a while

[Nasos Evangelou-Oost]

@Huỳnh Trần Khanh i see. actually what i'm more interested is in computational category theory and general purpose programming. i recently was surprised to learn that lean4 is actually quite capable of this. i'm currently working on a project in F# but the lack of dependent types is limiting. i also considered idris2 as a general-purpose dependently typed language but it is in prerelease and its development seems slow (idris 1 seems too slow to be able to do anything useful).

[SnowFox]

Is there a roadmap until port : Lean3 -> Lean4 port mathlib?

[Sayantan Majumdar]

lean4 seems significantly different. Does this mean mathlib has to be written again?

[Kevin Buzzard]

Lean 4 is very similar to lean 3, but sufficiently different to make porting the maths library a nontrivial problem. Right now we're letting the experts think about this but it's still early days.