Starting new people on Lean3 or Lean4?

Stream: new members

[Daniel Packer]

Hi folks!
I haven't been actively engaged in the community since the summer, so I'm a bit out of the know. Some folks here in the math department at Ohio State are interested in forming a lean learning/working group. Would it be worthwhile to try to start new learners out on Lean4 or should we stick to Lean3 until Lean4 is more stable?
Thanks!

[Martin Dvořák]

Lean 4 is probably better.

[Patrick Massot]

Martin, Daniel wrote "math" in his question.

[Patrick Massot]

Daniel, Lean 4 is not yet ready for mathematicians but you can safely start learning Lean 3 and switching to Lean 4 will be much easier than learning Lean in the first place.

[Patrick Massot]

See https://leanprover-community.github.io/learn.html for learning resources, especially https://leanprover-community.github.io/mathematics_in_lean/ for mathematicians.

[Martin Dvořák]

Patrick Massot said:

Martin, Daniel wrote "math" in his question.

I noticed it, yes. I was just stating my opinion.

In the (hopefully not very distant) future, Lean 4 should be better for both mathematicians and computer scientists.

I don't have this opinion because I like Lean 4 better, not at all! I have been using only Lean 3 so far. I have not written a single line in Lean 4 yet. Nevertheless, I think that, for (a group of) new people, jumping right in Lean 4 will be a better use of their time (even though they cannot do as much math with Lean 4 as they could do with Lean 3 now).

I will soon have to switch to Lean 4 in order to keep up with the new development. I don't expect the switch to be easy.

[Martin Dvořák]

It might be good to spare new people from having to undergo this change.

[Patrick Massot]

They are at a math department, they want to do math, so they don't have a choice.

[Martin Dvořák]

Didn't @Kevin Buzzard say that Lean 3 will be abandoned in a few months?

[Johan Commelin]

Basically all learning material is currently written in Lean 3. And I think you'll find transition from Lean 3 to Lean 4 easier than you are expecting.

[Heather Macbeth]

We are working very hard on the port, but 130,000 lines in, mathlib4 is still mathematically almost content-free.

[Martin Dvořák]

I don't want to rush you, but can you provide a rough estimation of when mathlib4 will get so advanced that it will start adding mathematical theorems that mathlib3 doesn't have?

[Martin Dvořák]

I guess it will be the point when we can officially say "Lean 3 is not worth learning anymore".

[Jireh Loreaux]

When the port is (close to) finished? My ballpark estimate based roughly on how quickly the port has progressed so far: 6-ish months.

[Yaël Dillies]

When you get finsets in, I might actually start writing Lean 4 code.

[Heather Macbeth]

@Yaël Dillies what's this "you"? Join the port! :-)

[Yaël Dillies]

My Lean 3 addiction is bad enough already! I cannot take on any more.

[Yaël Dillies]

"What's worse than a lean? Two leans"

[Heather Macbeth]

Seriously, porting isn't fun but we all need to work together on this.

[Yaël Dillies]

I tried to get time for it, and I couldn't. I rarely refuse to take up work but here I genuinely can't.

[Martin Dvořák]

I would have time for it, but I wouldn't have energy for it. I might do a lemma or two with the spare energy I currently have, but I don't think it is worth joining the porting.

[Ruben Van de Velde]

If you aren't able to help with the porting itself, maybe you can help by not adding more content to mathlib 3 that others will need to port?

[Martin Dvořák]

Are you criticizing me for having added stuff into mathlib3 last year?

[Martin Dvořák]

Oh, sorry, I also helped someone to PR their lemma to mathlib3 this year.

[Yaël Dillies]

Empirically, most of the content I'm adding is ported by myself :grinning_face_with_smiling_eyes:

[Martin Dvořák]

I think someone should decide and announce whether adding more code to mathlib3 is desirable (in case of files that haven't been ported to mathlib4 yet).

[David Loeffler]

I think someone should decide and announce whether adding more code to mathlib3 is desirable

I made a similar request on this zulip a few days ago here : https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/No.20more.20PRs.3F (resurrecting a thread from a month back). The verdict seemed to be that PR's to mathlib3 which add substantial new mathematics are still being accepted, as long as they reasonably self-contained changes and definitely don't touch files which are already ported.

[Martin Dvořák]

Yes, I always check whether a file has already been ported.

[Martin Dvořák]

Having read now what Kevin Buzzard wrote, I will not add any more PR into mathlib3.

[David Loeffler]

Having read now what Kevin Buzzard wrote, I will not add any more PR into mathlib3.

(You might want to read that thread to the end, rather than just reading the quote from Kevin at the start of it; Kevin's quote doesn't necessarily represent the community consensus.)

[Ruben Van de Velde]

Speaking purely for myself - I don't think there's a need to stop contributing new mathematics to mathlib 3 at this point, it's just what sounds like a flat out refusal to also assist with the port that rubs me the wrong way. I hope I'm just misunderstanding what people are saying, though

[Martin Dvořák]

Unpopular opinion: I don't think that the only way how to be a good Lean user is to be helping with a port to Lean 4.

[Arthur Paulino]

It's not an unpopular opinion. Experimenting with the system in various ways is good for its development. We can find a wider range of bugs if we don't narrow our interactions with it

[Kevin Buzzard]

@Daniel Packer sorry that your question got derailed. If you want to do maths then use lean 3 or wait for the maths library to be ported to lean 4 which won't happen until at least the summer