Intro to Proofs in US with Lean

Stream: Lean for teaching

[Matthew Ballard]

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.

[Kevin Buzzard]

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

[Matthew Ballard]

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

section
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 :=
sorry

end

/- Question 2 -/
section
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 :=
sorry

end

/- Question 3 -/
section
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 :=
sorry

end

[Matthew Ballard]

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.

[Matthew Ballard]

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.

[Matthew Ballard]

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.

[Apurva Nakade]

Hi @Matthew Ballard , I'm teaching a "foundations of math" course next Jan. I'd love to see your course materials. I'll DM you my email address.

Did you have to explain type theory in your course? Also, could you do anything more than Logic in Lean? One big worry I have with using Lean is that it'll turn the foundations of math course into an intro to logic course.

[Matthew Ballard]

No type theory, alas. I supplemented with Infinite descent but I may reverse the roles this cycle.

[Matthew Ballard]

One thing I took from Logic and Proof that I found very valuable was the different means of presenting the "same" core ideas at least in the logic component.

• Natural language proofs
• Natural deduction
• Lean

I think this diversity of incarnation helped reach the broadest swath of students.

[Matthew Ballard]

I didn't ever feel like it was a logic takeover.

[Matthew Ballard]

While natural deduction may be the obvious thing to cut from the three, it is also the thing which has been gamified

[Sarah Smith]

Hi @Apurva Nakade are you still planning on teaching a Foundations of Math course this Spring using Lean? Are you based at Northwestern?

[Apurva Nakade]

Sarah Smith said:

Hi Apurva Nakade are you still planning on teaching a Foundations of Math course this Spring using Lean? Are you based at Northwestern?

I'm teaching an intro to proofs class at Northwestern but it won't be based on Lean. At best I'll have an optional Lean project at the end. I don't think type theory is essential for doing math :P