Zulip Chat Archive

Stream: Lean for teaching

Topic: Intro to Proofs in US with Lean

view this post on Zulip Matthew Ballard (Mar 11 2021 at 19:23):

Last fall, I decided to incorporate Lean into our existing Introduction to Mathematical Reasoning course here at UofSC. The goal of the course was definitely not Lean for Lean's sake. Rather, I wanted to see if Lean could be useful for students whose ultimate outcome is to compose convincing written or oral natural language proofs of basic mathematical statements. In my experience, teaching students to write good proofs requires many detailed feedback cycles per assignment. Better than me, Lean provides immediate feedback as to problems. My main concern was whether including the additional language of Lean would constitute too much inertia for students to realize any pedagogical of Lean.

The majority of students were first-year in our honors program. So the student background was essentially good US high school education which includes seeing calculus/taking calculus concurrently. In particular, students were not expected to have any experience with mathematics at the UG level nor any programming experience. It turned out the majority of students were CS majors that were also thinking about incorporating math into their degree in some way (dual major, minor, or just mathed-up).

For a textbook, I initially leaned on Logic and Proof to structure the flow of material. By midway through, I had incorporated Infinite Descent and authored a good portion of the Lean components of the assignment. We covered logic, sets, functions, and then delved into basics of group theory by focusing on four main classes, cyclic, symmetric, dihedral, and free groups.

The first 2.5 months of the course were structured closer to traditional lecture. I tried to break up me just talking to students with some small group work periodically. After this, we had covered logic, sets, functions, and relations. During this time, students worked on homework in rotating groups. The assignments were about 2/3-3/4 written problems and 1/4-1/3 lean problems. Tactic-based proofs were essentially buried for the majority of course. Forcing students to confront a term-based assume, have, show proof in Lean forced them to rectify their thoughts. As an added benefit, it made identifying whether a problem with a written proof came from poor communication or poor understanding easier. If a student could compose a proof that compiled but I didn't understand their written work, then I knew where to focus the attention.

Each week for the final 4 weeks, I handed out worksheets on the 4 classes of groups above. Students were required to fill in the proofs and present some of their proofs. There was no Lean here. The structure was strongly influenced by this course at JHU.

Finally, in place of a final exam, there was final project chosen from a selection. By far, the most popular option was beating the NNG. I take this as the strongest indication of students' appreciation for Lean overall.

Anecdotal conversations lead me to believe that the individual appreciation was highly variable. Some students loved it and thought it was the best part of the course. Others viewed it as a distraction to the core material though I think they understand why I believed it brought value. I don't think anyone actively detested it partly because you could still earn a good grade without much proficiency in Lean.

I think, overall, it went gang-busters. Ultimately, I'd like to build these into undergraduate major and graduate qualifying courses.

view this post on Zulip Kevin Buzzard (Mar 12 2021 at 06:53):

Many thanks for your report. Are any of your teaching resources eg Lean files available online?

view this post on Zulip Matthew Ballard (Mar 12 2021 at 13:28):

Unfortunately, right now, everything is embedded in Microsoft Teams and often in strange ways to ease workflow. For example, all my lean files have .txt extensions because the file viewer in Teams balked at rendering .lean files in the pop-up window. To get a sense of what a homework assignment looked like, here is the lean component on the week we did relations:

import data.set

parameters {U : Type} {R : U  U  Prop}

#print irreflexive  -- definition of irreflexive
#print transitive -- definition of transitive
#print anti_symmetric -- definition of anti-symmetric

parameter (irreflR : irreflexive R) -- a proof that R is irreflexive
parameter (transR : transitive R) -- a proof that R is transitive

/- Question 1: Prove that an irreflexive and transitive relation is anti-symmetric -/
example: anti_symmetric R :=


/- Question 2 -/
parameters {U : Type} {R : U  U  Prop}
parameter (equivR : equivalence R)

#print equivalence -- take a look at the definition of equivalence in Lean
#print reflexive
#print symmetric
#print transitive

def Rop (x y : U) : Prop := R y x -- the "opposite" relation to R

example : equivalence Rop :=


/- Question 3 -/
open set

variable {U : Type}

def equiv_class (X : set U) (S : U  U  Prop) (x : U) : set U :=
{ y  X | S y x }

variable R : U  U  Prop
variable X : set U
variable a : U

#reduce equiv_class X R a -- see what Lean thinks this is
#check ext_iff

example (x y : U) (h1 : x  X) (h2 : y  X) (equivR : equivalence R) : equiv_class X R x = equiv_class X R y  R x y :=


view this post on Zulip Matthew Ballard (Mar 12 2021 at 13:33):

Additionally, I discovered that having to translate a statement often required some understanding of the statement. For example, if all our calculus homework were turned in Lean, then the instances of search-copy-paste solutions to assignments would approach 0. Currently, we are at nice spot in the development of Lean where it is documented sufficiently so students (and instructors) shouldn't struggle with the basics of the language but, at the same time, you can't toss your question into a google search and pull up a solution.

view this post on Zulip Matthew Ballard (Mar 12 2021 at 13:34):

That being said, I definitely benefited from @Jeremy Avigad sharing his course materials from CMU. So I would be happy to share what I have via email. People should not hesitate to reach out.

view this post on Zulip Matthew Ballard (Mar 12 2021 at 13:36):

For me, the main lesson (I think) was the stark difference between the fears I felt when I began contemplating adding in an ITP to such a course and the actual outcomes.

Last updated: May 06 2021 at 01:57 UTC