Fields Institute Mathematics Education Forum March Meeting

Stream: Lean for teaching

[Kitty Yan]

We are pleased to invite you to a Zoom session on AI and automated reasoning, sponsored by the Fields Institute in Toronto as part of the mathematics education forum’s activities.

Date: March 26, 2022, from 10am to 1:15pm, Toronto time.

You will be able to see the program: http://www.fields.utoronto.ca/activities/21-22/meforum-Mar

If you are planning to attend the session, please register via https://www.fields.utoronto.ca/cgi-bin/register?form_selection=meforum You will then get an email with a Zoom link.

Kindly please forward this invitation to your colleagues who may be interested in attending. Registration is free.
Gila and Kitty

[Kevin Buzzard]

Heather is about to announce the conference date/time in funky Zulip time zone format (because I failed ;-) )

[Heather Macbeth]

@Kevin Buzzard Indeed you seem to be off by 2 hours :)

[Heather Macbeth]

2022-03-26T10:00:00-04:00 to 2022-03-26T13:15:00-04:00

[Johan Commelin]

That's the same times as Kevin posted... :face_palm:

[Filippo A. E. Nuccio]

(they look identical to me...)

[Jeremy Avigad]

Heather and I are going to be speaking at this meeting on Saturday. In my talk, I'd like to show a list of courses/people who are using (or have used) Lean to teach mathematics. In addition to Heather and me I know of @Kevin Buzzard , @Patrick Massot , @Gihan Marasingha , @Matthew Ballard, and @Sina. Are there others? I'll put the slides on my web page with links to the courses.

[Sina]

Jeremy Avigad said:

Heather and I are going to be speaking at this meeting on Saturday. In my talk, I'd like to show a list of courses/people who are using (or have used) Lean to teach mathematics. In addition to Heather and me I know of Kevin Buzzard , Patrick Massot , Gihan Marasingha , Matthew Ballard, and Sina. Are there others? I'll put the slides on my web page with links to the courses.

Here's the link to the course I'm teaching at Johns Hopkins:
Introduction to Proofs: https://introproofs.github.io/s22/

(This course is for Spring 2022. Once the course is done, I'll post here a no-too-short report on my experiment of teaching intro to proofs entirely with Lean.)

[Heather Macbeth]

I think @Kalle Kytölä has?

[Patrick Massot]

Resources for my course can be found at https://www.imo.universite-paris-saclay.fr/~pmassot/enseignement/

[Patrick Massot]

Exercises can also be done in gitpod

[Patrick Massot]

And if people are interested in controlled natural language then the link to a rough English version is https://github.com/PatrickMassot/lean-verbose

[Rob Lewis]

Is this forum being recorded? I'm very interested in it, but won't be available on Saturday to watch

[Jeremy Avigad]

I can't tell whether the talks will be recorded, but I will let you know if they are.

[Kalle Kytölä]

Heather Macbeth said:

I think Kalle Kytölä has?

I don't think my course counts here.

In a 2nd year course I did very limited experiments, only in a handful of lectures (maybe 10-20% of total lecture time, and given that recorded more standard lectures existed, even this was an obviously optional and experimental component). In particular I did not teach the students any Lean syntax or give them any Lean problems. My main point was that the infoview is a way to follow what is going on in a proof, since this was one of their first exposures to proofs. The students participated, however, by suggesting proof steps in natural language, which I then "translated" to Lean on the spot (at least if they were reasonable), and we saw how the tactic state changed. The following was an example actually done in a lecture towards the end of the course (I was using my custom preliminary lemmas numbered as in my lecture notes, so this will not compile in mathlib, but should give an idea):

/-- Theorem XI.6 (Compactness implies completeness) -/
theorem compact_implies_complete
  {X : Type*} [metric_space X] :
  is_seq_compact_space X → is_complete_space X :=
begin
  -- Assume that X is compact.
  assume X_cpt,

  -- Let xs be a sequence, and assume it is Cauchy.
  intro xs, assume xs_Cauchy,

  -- Since X is compact, the sequence xs has a convergent subsequence xsub.
  rcases X_cpt xs with ⟨xsub, ⟨xsub_subseq, xsub_conv⟩⟩,

  -- By Lemma X.5 the Cauchy sequence xs with a convergent subsequence xsub is itself convergent.
  apply Cauchy_with_convergent_subseq_implies_convergent,
  refine ⟨xs_Cauchy, ⟨xsub, ⟨xsub_subseq, xsub_conv⟩⟩⟩,

  -- QED.
end

In the course feedback questionnaire I asked about the helpfulness of Lean. Very few people had any opinions (very few attended the experimental lectures). The handful who had opinions were polarized: a few said it was very helpful (which probably just meant they enjoyed seeing a new game) and a few said it was very unhelpful. Don't worry, I am stubborn and I have not given up yet... I think the success is very much dependent on the implementation, and mine was a first experiment only.

One implementation issue that I tried but abandoned at the students' request was Observable notebooks such as this. They were very slow for using Lean, and typing even ordinary text and math was slow (so I switched to a virtual blackboard). But I think notebooks of this flavor could work very well, with better preparation. I loved @Bryan Gin-ge Chen's Lean tools for Observable in principle, although I abandoned this format after two lectures, and later only showed Lean in a shared VS Code window.

[Heather Macbeth]

Kalle Kytölä said:

The students participated, however, by suggesting steps in natural language, which I then "translated" to Lean on the spot (at least if they were reasonable), and we saw how the tactic state changed.

I love this idea!

[Kalle Kytölä]

That's maybe the only idea which worked quite well. Otherwise my implementation requires more than a bit of polishing... (But remote lectures with previous years' lectures recorded did give me freedom to experiment more than usually! I don't think I could have done this if we hadn't been again forced to remote mode by the Omicron surge.)

[Kalle Kytölä]

I also really think the Observable notebooks have potential, because the students can browse them without installing Lean. And they could contain problems. (This time I had other issues.)

[Jireh Loreaux]

@Jeremy Avigad in case it's relevant: I haven't used Lean in teaching just yet, but I will be offering a Lean course this summer as a topics course jointly for our math and CS students. I don't have a repo that I'm ready to share publicly though.

[Kitty Yan]

Jeremy Avigad said:

I can't tell whether the talks will be recorded, but I will let you know if they are.

The session will be recorded. I will ask for a link to the recording and share it with the community.

[Kitty Yan]

The video recording of the March Meeting is available now http://www.fields.utoronto.ca/activities/21-22/meforum-Mar

[Kevin Buzzard]

Thank you Kitty! BTW the link just sits there on "Waiting for www.fields.utoronto.ca" on Firefox for me -- is anyone else having the same problem? Chrome working fine.

[Damiano Testa]

For me, it hangs on both Firefox and Chrome.

[Arthur Paulino]

It works for me now. The server was unreachable

[Damiano Testa]

Indeed, now it works for me as well.