# Zulip Chat Archive

## Stream: Lean for teaching

### Topic: Lean3 or Lean4?

#### Assaf Kfoury (May 03 2023 at 17:51):

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 (May 03 2023 at 17:53):

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 (May 03 2023 at 18:07):

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

#### Johan Commelin (May 03 2023 at 18:07):

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

#### Jon Eugster (May 03 2023 at 20:16):

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 (May 03 2023 at 20:35):

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 (May 04 2023 at 08:09):

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 (May 04 2023 at 13:34):

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 (May 05 2023 at 14:09):

@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).

Last updated: Dec 20 2023 at 11:08 UTC