teaching early US ugrads f'22

Stream: lean4

[Matthew Ballard]

I am teaching an intro to proofs for math majors this fall (2022). This is my second time. The previous time I incorporated Lean 3 following @Jeremy Avigad 's course at CMU Logic and proof. I wanted to get a communal sense of moving to Lean 4 for this. (Perhaps mainly for those already familiar with Logic and Proof) What are the main gaps I would need to fill in at the moment?

[Patrick Massot]

I don't see what could be missing. If I remember correctly this book doesn't use mathlib at all. However you probably won't gain much by switching to Lean 4. Students won't have to remember to use commas but they will fail because of whitespace sensitivity.

[Matthew Ballard]

There is a lot of have, assume, suffices, show from. Are these implemented?

[Patrick Massot]

Of course!

[Patrick Massot]

Why are you following this book for math majors? It's really targetting computer science people.

[Matthew Ballard]

Really? I didn't get that feeling.

[Matthew Ballard]

The student population for this course probably does not exist in Europe. These are usually fresh from high school who really only have seen calculus as math.

[Patrick Massot]

It puts a lot of emphasis on pure logic.

[Matthew Ballard]

That being said, the majority of enrollment is from students that are doing CS for their major and math for a double or minor

[Patrick Massot]

In France the first 10 chapters would never be taught in any form to a math student.

[Matthew Ballard]

The first 10 chapters form the "standard" for an intro to the major course in the US.

[Matthew Ballard]

What you do after that is gravy

[Matthew Ballard]

We get some very talented students but the baseline for knowledge is much lower than elsewhere

[Matthew Ballard]

The other text I supplemented with was Infinite descent which follows a similar structure with less emphasis on natural deduction

[Patrick Massot]

It's not a baseline issue. Math students in France never learn this at all, from birth to death.

[Matthew Ballard]

Sure but they are exposed it to before they meet you, right?

[Patrick Massot]

You mean before being born? No.

[Patrick Massot]

Before I started using Lean I had never heard "natural deduction". I may have heard "first order logic" logic but I'm not sure. I never heard "semantic" in any math-related context.

[Matthew Ballard]

I guess I need to kick the tires a bit.

[Jireh Loreaux]

@Matthew Ballard, just for reference, I teach in the US (and did undergraduate and graduate school here), and I agree with Patrick. The first 10 chapters are full of a bunch of things that are not frequently taught to math undergraduates. For example, most students (nay, I would argue most mathematicians I know) don't understand the distinction between natural deduction and classical reasoning (although they may have some idea that there is a thing called constructivism and maybe they have heard of intuitionist logic). Most students never hear about soundness and completeness (except perhaps in the context of Gödel's theorem, but even then, they probably can't explain what "completeness" means here).

That being said, most intro to proof courses I have seen in the US do spend a few weeks at the beginning of the semester covering the basics of propositional and first-order logic.

[Matthew Ballard]

I should have been more precise. From my experience, the core of such a course is

• propositional and predicate logic
• sets
• functions
• relations

Natural deduction is less common I agree. Classical reasoning vs other logics is generally a comment in passing as is soundness and completeness.

[Matthew Ballard]

Is this fair?

[Kevin Buzzard]

I certainly teach sets, functions and relations to students part of their intro to proof course which they do the moment they walk through the doors. But, like Patrick, I've never learnt or taught natural deduction, and I only heard about the concept of 1st order logic and the word "semantic" because I did the optional 3rd year logic and set theory course.

[Patrick Massot]

Matthew Ballard said:

I should have been more precise. From my experience, the core of such a course is

• propositional and predicate logic
• sets
• functions
• relations

Natural deduction is less common I agree. Classical reasoning vs other logics is generally a comment in passing as is soundness and completeness.

Only the first item is part of the first 10 chapters of Logic and proofs I was talking about.

[Patrick Massot]

Of course the last three items (sets, functions and relations) are taught in math departments in France and UK.

[Patrick Massot]

But this comes after Chapter 10 in that book, hence my initial remark.

[Patrick Massot]

About propositional and predicate logic, my experience is that an abstract treatment of these don't help students at all because it is very hard to transfer to practice in everyday mathematics.

[François G. Dorais]

@Matthew Ballard

distinction between natural deduction and classical reasoning

What distinction do you mean? Classical reasoning makes perfect sense for natural deduction - see 5.1 in Logic and Proof. Natural deduction can be both classical or intuitionistic, the difference is including or excluding one rule.

I think I know what you mean though. Nevertheless, proof-by-contradiction is a standard topic in intro-to-proofs courses in the US. As a backbone, many such courses use (slightly disguised) forms of natural deduction or variants, and very few use Hilbert style proofs.

[Patrick Massot]

In my course I remove abstract logic exercises every year (not sure about next year: maybe I don't have any of them left to remove)

[François G. Dorais]

@Patrick Massot Have you looked at Dan Velleman's How to prove it?

[Matthew Ballard]

François G. Dorais said:

Matthew Ballard

distinction between natural deduction and classical reasoning

I think this is @Jireh Loreaux but you almost convinced me it was me :)

[Patrick Massot]

I think I did but I don't remember what I thought about it. However I've looked at many such books and I couldn't find anything that helped for my course.

[Patrick Massot]

And now I should go to bed.

[Jeremy Avigad]

@Matthew Ballard This fall, I'll be focused on working on two other textbooks -- Logic and Mechanized Reasoning and Mathematics in Lean, but I'd love to see Logic and Proof ported to Lean 4 and updated to be more useful for teaching.

My co-authors (@Rob Lewis and @Floris van Doorn) might have other views, but I am not wedded to the prominence of logic. I think seeing some logic is generally helpful: if helps students understand formalism and what is going on under the hood, it helps them think about the way the form of the hypotheses and goal structure a proof, and it is generally useful for applications to CS -- programming and using database queries and so on. But I would not be sorry to see natural deduction go or the focus of logic cut back. It's no fun grading natural deduction proofs, and Lean does a better job at teaching formal deduction.

In any case, whatever the role of logic, Rob and Floris and I (and @Marcus Rossel) have come to the conclusion that it would be more useful to move from term mode to tactic mode, because (1) the latter are easier to learn, (2) it's easier to build more advanced proofs on that, and (3) it's the norm for mathlib. I don't think it would make a huge difference to the exposition -- instead of telling students to write or.elim h ... we'd tell them to write cases h and instead of writing or.inl they would write left, etc.

One issue that arises is that it was really helpful in the past that students didn't have to install Lean to do the homework assignments, since they could use the browser version of Lean. There currently is no version of Lean 4 that runs in the browser, though we have had success in having students use Lean using Gitpod.

Anyhow, I'll be free from teaching in the spring and I can invest effort in porting L&P to Lean 4 then. If there is anything I can do in the meanwhile that would be helpful, let me know.

[François G. Dorais]

@Matthew Ballard Yes, you're right! Sorry about the confusion!

[Matthew Ballard]

Jeremy Avigad said:

In any case, whatever the role of logic, Rob and Floris and I (and Marcus Rossel) have come to the conclusion that it would be more useful to move from term mode to tactic mode, because (1) the latter are easier to learn, (2) it's easier to build more advanced proofs on that, and (3) it's the norm for mathlib. I don't think it would make a huge difference to the exposition -- instead of telling students to write or.elim h ... we'd tell them to write cases h and instead of writing or.inl they would write left, etc.

Interesting. To my eye, sugaring the syntax to resemble natural language would have the most benefit at this level.

[François G. Dorais]

@Patrick Massot Dan's book is great and much closer to what I've seen in your course notes than you might think. Another important difference is that @Dan Velleman is very strongly interested in Lean and can be found here on Zulip from time to time. (Sorry for putting you on the spot Dan!)

[Matthew Ballard]

Jeremy Avigad said:

One issue that arises is that it was really helpful in the past that students didn't have to install Lean to do the homework assignments, since they could use the browser version of Lean. There currently is no version of Lean 4 that runs in the browser, though we have had success in having students use Lean using Gitpod.

Yes I cannot assume that students have acquired great technical sophistication. The in-browser version of Lean is almost perfect for the level of use in the course. This is the main hold up in my mind right now

[Patrick Massot]

In my experience natural language syntax is slightly harder to learn but much better to transfer to paper. You know about lean-verbose right?

[Matthew Ballard]

Yes and :in_love:

[Patrick Massot]

About installing Lean: do you really expect such young students to work at home? If they work only in a computer room in your university then everything becomes simpler.

[Jireh Loreaux]

@François G. Dorais yes, sorry, I mixed up the terminology myself! :laughing:

[Marcus Rossel]

@Matthew Ballard If you're still interested in using Logic and Proof, my plan is to have updated the first 10 chapters to Lean 4 by early October. And once the update process gets going, subsequent chapter may not take too long.

[Matthew Ballard]

@Marcus Rossel Awesome! My semester starts in two weeks though. :face_palm:

[Matthew Ballard]

Patrick Massot said:

About installing Lean: do you really expect such young students to work at home? If they work only in a computer room in your university then everything becomes simpler.

The plan is for group work in class with them finishing outside of the course if necessary.

[Matthew Ballard]

I am fortunate to have a small course.

[Jeremy Avigad]

To my eye, sugaring the syntax to resemble natural language would have the most benefit at this level.

Well, cases is reasonably close to "There are two cases to consider. Case one: ... Case two: ..." In general, you want to overall structure of a formal proof to be similar to the structure of an informal proof, and it's not clear to me that it is any harder to approximate it with a tactic proof than with a term proof.

@Marcus Rossel Thanks for doing this! What type of online textbook format would be most useful, given that there is no web-browser version of Lean 4 yet?

[Marcus Rossel]

Jeremy Avigad said:

What type of online textbook format would be most useful, given that there is no web-browser version of Lean 4 yet?

I was just going to go for the readthedocs sphinx template that you've mentioned before. I'll be using the book for a computer science course, so I'll just tell the students to install Lean.

[Yakov Pechersky]

What is the challenge for making Gitpod work with Lean4?

[Sebastian Ullrich]

There is no challenge, it worked for us without issues for two years in a row https://github.com/IPDSnelting/tba-2022

[Matthew Ballard]

I just want to summarize my understanding to make it easier to locate in the future.

From this dicussion, it seems that if

1. you are willing to teach your students git /assume they know it and
2. you won't go over 50 hours/month (most likely accidentally)

then there are really no technical obstructions to using Lean 4 in an intro to proofs course for undergrads.

[James Gallicchio]

(and that you don't want to teach with/about mathlib)

[Matthew Ballard]

Everything I needed last time I ran this course with Lean 3 were in core.

[Patrick Massot]

I don't understand the link between your summary and the previous conversation.

[Patrick Massot]

Are you talking about gitpod? GitPod doesn't require Git and can use any library. Or are you commenting on the absence of mathlib in Lean4?

[Matthew Ballard]

Fair. This was in my mind but was not emphasized. I want to control the environment , as much as possible, students are using so I don't have to deal with setup issues. The web browser version only requires a modern browser to use Lean.

Without it the best option seems to currently be Gitpod. I guess students don't need to know basic git to use it but at this point I would want to tie into a workflow for automatically grading the assignment. For that they need git.

[Jeremy Avigad]

I can confirm that Gitpod is easy with any flavor of Lean. Students get 50 hours free each month, which should be more than enough.

[Matthew Ballard]

The student developer pack on Github also provides 6 months free of the personal plan (100 hr/month).

[Dan Velleman]

Can you do elementary set theory in Lean 4? It looks to me like the definitions from Lean 3 in core/init.data.set are not there in Lean 4. Or am I missing something? I would think you'd want to do some basic set theory in a proofs course.

[Henrik Böving]

They are not there but implementing basic set theory in Lean is quite straight fowrard (and translating the Lean 3 file to Lean 4 by hand would be easy as well)

Basically the only non trivial thing about is is, what is a set and the answer to that is:

def Set (a : Type u) := a -> Prop

and from here you can build everything, e.g.

def Set.inter (A B : Set a) : Set a := fun x => A x ∧ B x

and so on, you of course may want to define additional notation stuff etc. for this as well and also basic API lemmas etc. but all of that is doable right now and doesn't have any dependencies really. Hence we also already have lots of this stuff in mathlib4, specifically here: docs4#Set

[Matthew Ballard]

For my class, I took a quick run at assembling an autograding setup for my class. The purpose is not so much to catch/deter anything but rather have something I can look at quickly. The output of lean on the file below gets compared with an allowed set of axioms.

import Hw
import Lean.Elab.Print
import Lean.Elab.Command

open Lean
open Lean.Elab.Command

def collectAxiomsOf (constName : Name) : MetaM (List String) := do
  let env ← getEnv
  let (_, s) := ((CollectAxioms.collect constName).run env).run {}
  let a := s.axioms.toList.map toString
  return a

#eval collectAxiomsOf ``problem1

Where Hw.lean contains problem1.

[Matthew Ballard]

Since GitHub classroom autograding is done purely over stdout, this is enough for me (for this week). But for something like gradescope you want to generate a json and write that.

I can also imagine it being done via a lake script or using lspec.

I welcome people's thoughts.

[Mario Carneiro]

In IO, you don't have access to the environment, and a default-created one isn't going to have anything in it, which makes it impossible to find axioms or indeed your student's proof. If you want to run this at compile time, then the #eval approach you have now is fine, but if you want to do it at run time (producing a binary) then you need to call the lean frontend to parse your student's file and query the resulting environment.

[Kevin Cheung]

Marcus Rossel said:

Matthew Ballard If you're still interested in using Logic and Proof, my plan is to have updated the first 10 chapters to Lean 4 by early October. And once the update process gets going, subsequent chapter may not take too long.

How is the progress in porting "Logic and Proof" to Lean 4? Is there a repository for the source? I wasn't able to find it on the Lean home page.

[Benedikt Ahrens]

@Marcus Rossel : I would also be very interested in having the first 10 chapters of Logic and Proof updated to Lean 4. Are you still considering working on this update?

[Marcus Rossel]

Benedikt Ahrens said:

Marcus Rossel : I would also be very interested in having the first 10 chapters of Logic and Proof updated to Lean 4. Are you still considering working on this update?

The update ended up being less straightforward than I had hoped, so I abandoned the effort at some point. The main point being that term-based proofs didn't feel suitable anymore in Lean 4. Thus, tactics would need to be introduced, which would entail some rewriting of the chapters which I wouldn't feel confident doing. Also, @Jeremy Avigad was considering potentially splitting off the first 10 chapters into a document of its own, which would presumably require additional edits. But FWIW you can find the intermediate state here: https://github.com/marcusrossel/foundations-of-logic-and-proof