Lean 3 or 4?

Stream: new members

[Mark Wilhelm]

Hello, for simple hobbyist type uses, should I be using version 3 or 4? Thanks

[Eric Rodriguez]

what do you want to be doing? we'll soon be migrating mathlib to lean4 and most development going forwards, but not yet. lean4 is a far better programming language than lean3, though

[Mark Wilhelm]

I'm going through "seven sketches in compositionality" with a reading group, thought it would be cool if we did some of the exercises in there in something like lean. So i am not wanting to have like a complete library with everything already implemented, but rather we'd do that ourselves as a learning tool. I think like basic sets and arithmetic would be enough for libraries(?)

[Kyle Miller]

I'd suggest using Lean 3 for this. It's nice having mathlib on hand for those things you don't want to reimplement from scratch. There are also more Lean 3 learning resources at the moment.

If you haven't already, I'd also suggest going through some tutorials to get your feet wet before diving into formalizing things from a book. Seven Sketches in Compositionality is fairly formal, but I think there will still be many technical challenges that will be difficult to overcome without some Lean experience.

[Mark Wilhelm]

Great, thank you for the advice. Yes I'll definitely try to go through some tutorials first.

[Eli Mazaheri]

lean 4

[Kevin Buzzard]

Right now the question is the same as "do you want access to a gigantic mathematics library?". Note that there is mathlib4 which is quite like a "hobby" project now, it's being used as an experimental manual port, and basic stuff like sets are there by now, but it's of course nothing compared to mathlib := mathlib3

[Vasily Ilin]

I am co-running a weekly meeting with a group of math undergrads to learn the basics of Lean. We intent to formalize some easy math things. I notice that the installation link only mentions Lean 4 but Kevin Buzzard's 2023 course uses Lean 3. Which one should I prefer?

[Martin Dvořák]

Lean 4 definitely.

[Martin Dvořák]

Kevin Buzzard's 2023 course seems to have been happening before Mathlib was ported to Lean 4.

[Vasily Ilin]

What does "Lean 4 is currently released as milestone releases towards a first official release." mean here? I read it as "Lean 4 is not yet stable, use at your own risk"

[Johan Commelin]

That sentence is outdated. The first official release happened a few weeks ago.

[Johan Commelin]

cc @Sebastian Ullrich

[Vasily Ilin]

Can I still use projects written in Lean 3 if I use Lean 4 myself? Is it backwards compatible? Last year we went through Kevin Buzzard's formalising-mathematics-2022 and I was going to do the same this year but I can't even get the project with leanproject any more

[Johan Commelin]

Nope, there's no backwards compatibility.

[Patrick Massot]

@Vasily Ilin is there any reason why you want to use that source rather than one of the official ones listed at https://leanprover-community.github.io/learn.html?

[Kevin Buzzard]

My next course in Jan 2024 will be a lean 4 version of my course. Until I translate it in December I think #mil is an excellent place to start.

[Vasily Ilin]

I did not know about those official resources because I think they did not exist a couple of years ago when I first started learning Lean. Thank you for pointing them out to me. MIL looks like an excellent start!

[Kevin Buzzard]

(That came out slightly wrong: even after I've translated my course into Lean 4, #mil will still be an excellent place to start!)

[Vasily Ilin]

I miss the party hat in Lean 4! Why is there no more party hat?

[Kevin Buzzard]

Because there is no more begin/end it's apparently now far too confusing to have party hats, because they sometimes appear when you're not done. The issue is with the end, which is no longer there. If you are happy to use a by/tada block like we used to use begin/end blocks then you can use this code written by Mario:

import Lean
open Lean Elab Tactic

elab "tada" : tactic => do
  let gs ← getUnsolvedGoals
  if gs.isEmpty then
    logInfo "Goals accomplished 🎉"
  else
    Term.reportUnsolvedGoals gs
    throwAbortTactic

[Mario Carneiro]

PS: I believe the tada emoji ( :tada: ) is actually a depiction of a party popper, not a hat

[Ming Li]

I encountered the problem message " invalid field 'ltr', the environment does not contain 'Iff.ltr'". Any idea how to fix it?

[Ruben Van de Velde]

Try .mp

[Ruben Van de Velde]

Though I don't know where you got it in lean 3, docs3#iff.ltr doesn't seem to find it

[Ming Li]

Thanks.
I am learning codes from tutorials which used lean 3. But I am using lean 4.

[Patrick Massot]

This is obviously a very bad idea. Why aren't you following a Lean 4 tutorial?

[Ming Li]

I did follow lean4 tutorials but for some interesting mathematical results, I traced back some in lean 3.

[Patrick Massot]

Could you tell more precisely why tutorial you felt you needed to read in Lean 3 and what are those interesting mathematical results?

[Ming Li]

That is quite random. For example, today I tried an example of MIL in Mathlib4 (not alone in MIL). It gave me an error message "ambiguous, possible interpretations _root_.Prime x ". So I have to find a solution on internat, which suggests me to close "open Nat" and use "Nat.Prime" instead. Like this, sometimes, the suggestion leads me to lean3...

By the way, I notice that "theorem .... := by" sometimes ends withoud "by", or with "by {....}", why? This might be a dumb question, sorry.

At this moment, I am interested in "the Schröder-Bernstein Theorem". It seems Lean uses the constructive way to prove the result. I am wondering if it can be done in Lean by non-constructive way as in math.

[Patrick Massot]

ming said:

That is quite random. For example, today I tried an example of MIL in Mathlib4 (not alone in MIL). It gave me an error message "ambiguous, possible interpretations _root_.Prime x ". So I have to find a solution on internat, which suggests me to close "open Nat" and use "Nat.Prime" instead. Like this, sometimes, the suggestion leads me to lean3...

I don't see how that is different in Lean 3 and Lean 4. And I think you truncated the error message, Nat.Prime should be mentioned too.

By the way, I notice that "theorem .... := by" sometimes ends without "by", or with "by {....}", why? This might be a dumb question, sorry.

I you saw := without by in MIL you should try to report it since we always expect a tactic proof, so we should be consistent in always including by in the exercise. In general what goes after := is a proof term that can be either input directly or constructed using a tactic script that begins with by.

At this moment, I am interested in "the Schröder-Bernstein Theorem". It seems Lean uses the constructive way to prove the result. I am wondering if it can be done in Lean by non-constructive way as in math.

I am not sure which proof you have in mind, but the answer is most probably "yes". The reason why your question is confusing it that the proof in MIL is definitely not constructive. I don't think there any constructive proof of this theorem.

[Ming Li]

The proof of SBT in my mind is to use the map on the power set of f-domain constructed by composition of f and g and complement of sets has a fixed point. In this case, the injections of f and g are not needed. In stead of constructing bijection, it only has existence of the fixed point as a set. As you said, both are not constructive in sense of Turing machine..