Marmite

Stream: Lean for teaching

[Angela Li]

I think it was mentioned often that some students really did not like Lean in the courses, even when it was stated to be part of the course ahead of time. Were there any surveys on why students did not like Lean?

[Johan Commelin]

What's the difference between Lean and Marmite?

A: Lean is yummy, and Marmite is yuck.

[Simon Hudon]

I like how nuanced your answer is @Johan Commelin

[Johan Commelin]

/me experienced unvoluntary exposure to Marmite on a boarding school where one couldn't always choose which sandwich you got for lunch...

[Kevin Buzzard]

Marmite is yummy!

[Kevin Buzzard]

@Angela Li some maths students are just "not into computers"

[Angela Li]

Weren't some of the courses joint math/computer science though? At least that's what I thought with Patrick's course.

[Kevin Buzzard]

My course had about 230 maths students and 40 joint-maths-computing students

[Sarah Smith]

I thought this might be a good location to place my question :smile:. Has anyone using Lean in their classrooms noticed patterns to what groups of students respond well to the use of Lean and what groups it does not resonate with? And what does that response look like? How do you know if it works well in your classrooms or does not?

[Sina]

Hi Sarah,

Not exactly an answer to your questions, but I thought I'd share my teaching workflow, since this semester has, at least so far, worked much better than the same period of the last semester.

Here's my workflow: I usually spend about twenty to thirty minutes lecturing about the key concepts of each lesson, often sketching some informal and non-rigorous figures, say a figure for how to get a partition from an equivalence relation. We then spend the rest of class time (roughly about 45-55 minutes) to make these ideas precise and rigorous by writing our proofs in Lean.

I have only eight students, and I make them into 4 teams (rotating teams each lecture). For every line of code, I wait until the team whose turn it is to suggest a solution to the current Lean goal, and then I type their solution. If Lean gives us an error, I explain the error, and then I go to the next team and ask them if they have a solution. If no team at all gives a solution to the current goal, and this happened very rarely so far, I write my own solution, and we move on to the next lemma/theorem.

In Spring 2022 semester, a little less than half of my students responded well to the use of Lean and and the rest followed without much enthusiasm and in some cases with apathy.

This semester, so far, everyone seems to be enthusiastic, and we usually end up proving some statement in multiple ways, since different students/teams like to propose their own distinct solutions with their own favorite tactic. For instance, some students love apply, some others are addicted to have, and two students who use calc whenever possible. You can also tell this from their homework solutions.

I am writing a report (a collection of mistakes I did last semester, and how i fixed them this time) about the main factors responsible for the increased enthusiasm/participation from Spring 2022 to Fall 2022. I'll post it here when I'm done with it. I think the main factor is to instill in students a (mild) obsession with Lean, and having a Zulip server for my course, so that my TAs and I could help and debug in real-time, has been very helpful in this regard. We did not have a Zulip server in Spring 2022, and I think this was one of the mistakes.

[Mac]

Sina said:

I am writing a report (a collection of mistakes I did last semester, and how i fixed them this time) about the main factors responsible for the increased enthusiasm/participation from Spring 2022 to Fall 2022.

Are you thinking of turning that into a formal paper? As a person who has published in computer science and related conferences before, this kind of experience report seems right in line with the usual publications of such conferences. I think such a paper would be a great addition to the field! :smile:

[Sina]

Mac said:

Sina said:

I am writing a report (a collection of mistakes I did last semester, and how i fixed them this time) about the main factors responsible for the increased enthusiasm/participation from Spring 2022 to Fall 2022.

Are you thinking of turning that into a formal paper? As a person who has published in computer science and related conferences before, this kind of experience report seems right in line with the usual publications of such conferences. I think such a paper would be a great addition to the field! :smile:

Thanks for the encouragement. I actually have no experience of writing such a paper (reporting on teaching with Lean) for a conference publications. What are some of related CS conferences that would accept such a report?

[Mac]

@Sina of the conferences I know, ACM SIGCSE, ITiCSE, ICER, APSE ICCE, and IEEE FIE are big hitters. They are well ranked (though I generally think of SIGCSE as the flagship conference and FIE's ranking fell from B to C in the 2021 CORE rankings). On the deadline front, SIGCSE's has already past (it was in August), ITiCSE is in January, ICER is in March, ICCE is in May, and FIE has its abstracts due February but papers due April/May.

While your topic is technically mathematics, your specific application is computing-focused enough that I would be surprised if any of them reject you on that grounds. Though, if you are worried, ICCE (International Conference on Computers in Education) or FIE (Frontiers in Education) are broader on their face as neither is directly focused on Computer Science Education (CSE) - ICCE is pretty generally and FIE covers "all disciplines relating to engineering and computing education" -- so they may be better bets. For instance, the ICCE 2022 subconference on Computer-Supported Collaborative Learning (CSCL) and Learning Sciences might have been up your alley from your description of the class.

[Sarah Smith]

Sina said:

I am writing a report (a collection of mistakes I did last semester, and how i fixed them this time) about the main factors responsible for the increased enthusiasm/participation from Spring 2022 to Fall 2022. I'll post it here when I'm done with it.

Sina, this is a wonderful answer and thank you so much for the details. I would love to read the report when complete!

[Patrick Massot]

Sarah Smith said:

I thought this might be a good location to place my question :smile:. Has anyone using Lean in their classrooms noticed patterns to what groups of students respond well to the use of Lean and what groups it does not resonate with? And what does that response look like? How do you know if it works well in your classrooms or does not?

This is a tricky question. For a long time I thought that really bad students could not benefit from Lean. But last year I got one who really kept trying and actually ended up making very unexpected progress. Some people are not patient enough with the syntax requirement, they find it irritating to think they understand everything but can't convince Lean. Most of the time it comes from inadequate understanding but sometimes it indeed comes from purely technological difficulties. However it is very hard to predict who will be blocked by those technological issues.

[Patrick Massot]

However the global picture for me is still that most students respond well.

[Kevin Buzzard]

I don't really have anything to report because in my introductory course it's all optional and typically only some of the smart ones get involved, and for my final year course the people who choose to do it are selecting Lean as an option and hence are naturally going to be interested. I guess one observation is that last year everyone who was interested in my final year course did manage to write hundreds of lines of Lean code.

[Matthew Ballard]

No hard data but some observations mainly derived from a body of students that are seeing any math beyond single variable calculus (US style) for the first time.

• NNG was overwhelmingly the favorite for the final project of the course I taught in fall 20, like 90%
• students seem most confused at the beginning by how to structure a proof. Assumptions vs conclusions. What is allowed. The English language is not structured tightly enough for this even in the stilted vernacular that mathematicians often use. A student can follow a proof in tactic mode both locally at each step and globally better than natural language one at the start.

[Matthew Ballard]

Feedback via the info view is also something that is impossible to match in paper. It is instantaneous and constant. Success in lean helps build confidence in one’s abilities.

[Matthew Ballard]

On the other hand, when Lean was discussed in my graduate class one student was very dismissive. With an attitude of “I can provide a proof. If lean didn’t like, then it’s lean’s problem not mine”.

[Matthew Ballard]

Generality once people get stuck in their views, it becomes more difficult to move them then if they come to something fresh.

[Kevin Buzzard]

Re: it's Lean's problem not mine: Oh that's interesting, Patrick just made the same point. I didn't have that sort of problem in my class, but I suspect the difference was that people in my class had specifically signed up to it to learn Lean, and they had to write Lean code to pass the exam, so if Lean didn't like their proofs then it really was their problem, not Lean's.

[Matthew Ballard]

So far my students have not self selected for Lean affinity. That changes next semester

[Matthew Ballard]

One more anecdote: the intro to proofs students really really dislike premature “🎉 goals accomplished”

[Kevin Buzzard]

you mean "rw randomly closed the goal because it unexpectedly tried refl"? This surprised people to the extent that I disabled this functionality in NNG.

[Matthew Ballard]

No. I move cursor focus and it fires. Less worse is when it happens in a sub proof, like have block.

[Matthew Ballard]

We just saw rw calls rfl today and it was hard to gauge their response

[Matthew Ballard]

I should also mention I’m using Lean 4 this semester.

[Johan Commelin]

You mean when you get ":tada: goals accomplished" but there is still a sorry somewhere?

[Matthew Ballard]

In the middle of a proof. It seems different than Lean 3. I will try to reproduce the behavior and update.

[Assaf Kfoury]

Matthew Ballard said:

I should also mention I’m using Lean 4 this semester.

I am one who is slowly switching from Coq to Lean 3 in my teaching. I would be interested in the reasons some are choosing to use Lean 4, given that the latter still seems a little unstable.

[Matthew Ballard]

I think right now this is dependent on the specific course. For an intro to proofs course that covers topics like sets, functions, and relations then everything except sets perhaps has been stable for a while in Lean 4. This is the course for which I am currently using Lean 4. Lean 3 would look the same to the students. With Lean 4, I can more easily automate grading/feedback though.

I am also teaching an introduction to cryptography course where most of the programming components only use what I would view as "basic" features of a language. I choose Go in advance for its small syntactic surface area, its general focus on readability, and portability. It is a math/CS cross-listed course so I have broad range of students in terms of familiarity with programming and I wanted something user-friendly. So far Lean 4 would have been totally appropriate. Lean 3 would have been a stretch. I would trade some of simplicity for the ability to reason about the algorithms. If I do this course again, I will probably use Lean 4.

Next, semester I am teaching an undergrad course modeled on the logical verification course at VU and a graduate course. I know some people are thinking about porting the VU course to Lean 4. If that happens or if I have enough time to fill in the gaps over winter break, I would use Lean 4 for this. The graduate course is only feasible in Lean 4 after we pass through mathport.

[Assaf Kfoury]

Matthew Ballard said:

I think right now this is dependent on the specific course. For an intro to proofs course that covers topics like sets, functions, and relations then everything except sets perhaps has been stable for a while in Lean 4. This is the course for which I am currently using Lean 4. Lean 3 would look the same to the students. With Lean 4, I can more easily automate grading/feedback though.

I am also teaching an introduction to cryptography course where most of the programming components only use what I would view as "basic" features of a language. I choose Go in advance for its small syntactic surface area, its general focus on readability, and portability. It is a math/CS cross-listed course so I have broad range of students in terms of familiarity with programming and I wanted something user-friendly. So far Lean 4 would have been totally appropriate. Lean 3 would have been a stretch. I would trade some of simplicity for the ability to reason about the algorithms. If I do this course again, I will probably use Lean 4.

Next, semester I am teaching an undergrad course modeled on the logical verification course at VU and a graduate course. I know some people are thinking about porting the VU course to Lean 4. If that happens or if I have enough time to fill in the gaps over winter break, I would use Lean 4 for this. The graduate course is only feasible in Lean 4 after we pass through mathport.

Many thanks for the comments. Very useful!