## Stream: Lean for teaching

### Topic: Waterproof: educational software for learning how to writ...

#### Marcello Seri (Jul 13 2023 at 09:07):

With coq there is also this recent paper/tool that makes it much more student-friendly: https://arxiv.org/abs/2211.13513

#### Bulhwi Cha (Jul 13 2023 at 09:11):

Waterproof looks like Lean games.

#### Patrick Massot (Jul 13 2023 at 09:24):

Unfortunately this software seems abandoned. It doesn't build (see https://github.com/impermeable/waterproof/issues/82) and most pages of the website are blank, for instance https://impermeable.github.io/src/guide.html. They also don't answer emails.

#### Marcello Seri (Jul 13 2023 at 09:28):

That is surprising, the were presenting it just a few weeks ago at the netherlands mathematics conference and saying that they actively use it in their classes

#### Eric Wieser (Jul 13 2023 at 10:14):

It looks like they're all supposed to redirect to https://impermeable.github.io/src/default.html, which isn't much better

#### Heather Macbeth (Jul 13 2023 at 13:20):

Interesting, I never saw that paper before. I like their LaTeX-formatted proof environment!

It's nice to see that that paper includes an implementation of an Isabelle/Lean-style calc environment for Coq, I wonder if that will be incorporated into Coq standard libraries. I still think the Lean calc-syntax is nicer, though. Their calcs are one-liners and that would get unwieldy on nontrivial examples -- when I teach I encounter calcs like

  calc d (k + 2) = 3 * d (k + 1) + 5 * d k := by rw [d]
_ ≥ 3 * 4 ^ (k + 1) + 5 * 4 ^ k := by rel [IH1, IH2]
_ = 16 * 4 ^ k + 4 ^ k := by ring
_ ≥ 16 * 4 ^ k := by extra
_ = 4 ^ (k + 2) := by ring


#### Marcello Seri (Jul 13 2023 at 16:02):

Patrick Massot said: