Lean3 or Lean4?

Stream: Lean for teaching

[Assaf Kfoury]

I plan to use Lean in teaching a course on theorem proving and formal methods, starting in September 2023. If Lean4 is close to being fully operational, is there any reason to keep on using Lean3? What about pedagogical accessories (I have the Nat Number Game and mathlib in mind), are these being transferred/translated from Lean3 to Lean4, and how close are they ready to be used?

[Kevin Buzzard]

Mathlib is in the process of being ported; we are 60% of the way through. You can see if the mathlib3 files you want are ported by e.g. looking at the file on master and seeing if it says "this file has been ported to lean 4" at the top. The natural number game is also being ported, but I hope to rewrite some chunks of it and add some new stuff, and it's a case of finding the time.

[Johan Commelin]

@Assaf Kfoury Do you plan to use advanced bits of mathlib? Are you targetting bachelor or master students?

[Johan Commelin]

For a bachelor's course, I suppose that we should have a mathlib by September that is pretty usable.

[Jon Eugster]

The natural numbers game exists and is playable in lean4. Watch tomorrow for the announcement here on zulip:smiley: (also regarding creating new games)

[Assaf Kfoury]

Johan Commelin said:

For a bachelor's course, I suppose that we should have a mathlib by September that is pretty usable.

Many thanks to Kevin, Johan, and Jon, for their hopeful replies! Really glad that the transfer to Lean4 is moving ahead and moving fast. My intended audience in September will be, in the American university system, mostly seniors and first-year graduate students. So, I don't think I will need advanced bits of mathlib. And I'm really glad the Nat Number Game will be playable in Lean4 (really tomorrow already?). In Sept, I will ask my students to take time to play NNG on their own, perhaps in the first one-two weeks of the semester, after which I hope they will be able to solve homework assignments for which they will need no more more than the features of Lean already introduced in the NNG.

[Andrés Goens]

Assaf Kfoury said:

I plan to use Lean in teaching a course on theorem proving and formal methods, starting in September 2023. If Lean4 is close to being fully operational, is there any reason to keep on using Lean3? What about pedagogical accessories (I have the Nat Number Game and mathlib in mind), are these being transferred/translated from Lean3 to Lean4, and how close are they ready to be used?

"theorem proving and formal methods" sounds like a CS course? I think for CS applications the argument for Lean 4 over 3 is probably even stronger (as per the mathlib arguments above, mathlib and the math community around it being the main argument for Lean 3)

[Assaf Kfoury]

Andrés Goens said:

Assaf Kfoury said:

I plan to use Lean in teaching a course on theorem proving and formal methods, starting in September 2023. If Lean4 is close to being fully operational, is there any reason to keep on using Lean3? What about pedagogical accessories (I have the Nat Number Game and mathlib in mind), are these being transferred/translated from Lean3 to Lean4, and how close are they ready to be used?

"theorem proving and formal methods" sounds like a CS course? I think for CS applications the argument for Lean 4 over 3 is probably even stronger (as per the mathlib arguments above, mathlib and the math community around it being the main argument for Lean 3)

Yes, it will be a CS course, with several double-major students in Math and CS, and a few who were Math undergrads and then transferred to CS as graduate students. (I already have a partial list of students who signed up for the course.)

[Marcus Rossel]

@Assaf Kfoury I was involved in a CS course on theorem proving (more heavy on the underlying theory) last year and we used Coq and Lean 4 and it worked out just fine. We didn't need Mathlib and Lean 4 didn't cause any problems (I do recommend to tell students to always set_option autoImplicit false though).