How to prove it in Lean

Stream: Lean for teaching

[Assaf Kfoury]

Dan Velleman said:

How To Prove It can be used as a textbook for a discrete math course as you describe--or for a "transition to advanced math" course. I have used it that way, as have others. It does not mention Lean--it is about writing proofs in English.

How To Prove It with Lean is (or will be, when it's done) a companion to How To Prove It, explaining how to use Lean to write the proofs in How To Prove It. I have not used it with students--I haven't even finished writing it. But I hope it will be useful to students who are trying to learn to write proofs from How To Prove It.

At some point in the near future, as a pilot experiment, I plan to teach an introductory discrete-math course with a proof assistant. This is all part of an on-going conversation in a small group of colleagues at my university (Boston University). Are proof assistants a good way to teach and promote the rigor of mathematical proofs, or do they hinder students' ability to communicate in the language of written mathematics (in plain semi-formal math prose)? Are the syntactic rigor of proof assistants and the overhead of learning them largely independent of -- or an obstacle to -- developing intuition and semantic understanding of math concepts?

[Kevin Buzzard]

There is an entire stream on Lean for teaching, which would be a much better place to have this discussion.

[Notification Bot]

2 messages were moved here from #announce > How to prove it in Lean by Heather Macbeth.

[Heather Macbeth]

Assaf Kfoury said:

Are proof assistants a good way to teach and promote the rigor of mathematical proofs, or do they hinder students' ability to communicate in the language of written mathematics (in plain semi-formal math prose)? Are the syntactic rigor of proof assistants and the overhead of learning them largely independent of -- or an obstacle to -- developing intuition and semantic understanding of math concepts?

These are great questions ... of course, on this discussion board, you are reaching the formal-mathematics enthusiasts, and we all hope the answer is "yes".

One recent forum where these questions were discussed was the Learning Mathematics with Lean workshop organised in April by @Athina and Paola Iannone. I hope that the talks from that workshop will be on YouTube soon.

[Kevin Buzzard]

So yeah this is a great question. Paola Iannone and Athina Thoma recently organised a conference on Lean for teaching where various people discussed what they were doing and what their goals were. Roughly speaking some of us (including me) were just teaching a Lean maths course with the goal of teaching the students how to use Lean, and were not really concerned with how it was changing things like the students' perception of mathematics and in particular whether it was "making them better at maths" or whether it was just making them able to use a theorem prover.

However others (including Heather and Patrick) were teaching more introductory courses with other goals in mind. I'll perhaps let them speak for themselves.

[Heather Macbeth]

Here's a quick version of my own opinions on the subject. I taught a Lean-bilingual intro-to-proof this semester -- here's the book I wrote for it, and here are my slides about the course from the Southampton workshop. The course worked well, but I spent a ton of effort writing my own custom dialect of Lean to support it, with tactics automating exactly the steps I wanted my students to think of as "one chunk of reasoning". I don't think it would be possible to teach a Lean-bilingual course for early-undergrad students with off-the-shelf Lean.

[Heather Macbeth]

@Patrick Massot has also taught a Lean-bilingual course at this level and also spent a lot of effort developing custom automation for that course.

[Matthew Ballard]

I've twice taught our intro to proofs course using Lean. Introducing a theorem prover at the lower level was part of the reason I won our university award for innovative pedagogy so I think it can definitely be a positive for math education.

You will not be able to convince the majority of faculty to completely turn over such a class to an ITP. The expectation is that students will emerge with the ability to communicate as mathematicians do currently: in writing and orally. As such, you will want to gear your use to addressing how learning to Lean can help students achieve these skills.

Lots of translation exercises are essential. Students should be able to understand the mathematics in the written, oral, and digitized form. The ability to pass faithfully between them is a good signal for comprehension.

Students learn in a variety of ways. Lean will be the way some really grok an concept. Others it may not help so much. Providing different incarnations of a mathematical truth in this way provides a better chance at reaching a broader section of the students. With group work, students can gather their strengths and teach each other.

There will always be an extra learning curve, though @Patrick Massot's natural language tactics are the future for education. In general, when you teach such a class, you want to ask yourself if student should walk out of the course able to consume existing code in mathlib. The answer here depends on the time and your goals.

Lean also presents opportunities for gamification not usually present in such courses. I often lead students through a embedding of predicate logic into blockly to help open their mind as to the form of mathematics and proof.

In my experience, using Lean as component in such a class can improve outcomes.

[Assaf Kfoury]

Heather Macbeth said:

Here's a quick version of my own opinions on the subject. I taught a Lean-bilingual intro-to-proof this semester -- here's the book I wrote for it, and here are my slides about the course from the Southampton workshop. The course worked well, but I spent a ton of effort writing my own custom dialect of Lean to support it, with tactics automating exactly the steps I wanted my students to think of as "one chunk of reasoning". I don't think it would be possible to teach a Lean-bilingual course for early-undergrad students with off-the-shelf Lean.

Many thanks, Heather, for referring me to your book and sharing your slides. I already read several parts. Maybe this is the way to go in the future, Lean-bilingual math books. I still have to experiment myself and also compare your presentation with Patrick Massot's Lean-bilingual course. In support of what you did, it seems to me that a little hand-waving and intuitive understanding of concepts will never be divorced from the way we (humans) do mathematics and enjoy doing it, from the earliest baby steps to the most advanced research-level arguments -- and it is nice that we have (and will have) a proof assistant next to us to confirm our semi-formal reasoning.