ITP class

Stream: general

[Jeremy Avigad]

This is a follow-up to Mario's remark on "having existential statements", but I changed the thread title.

Here are the assignments Mario and I have assigned so far: https://www.dropbox.com/sh/m8r6bhu8m0zv012/AABOy6lv93pViN1-eZvHrmMpa?dl=0. Most of it derives from things already in TPIL. Once I have survived the semester, I will work the material back in there.

Another update: I finally moved PIL to Sphinx, though I have not yet changed the contents at all (so everything is outdated and broken). It's here: https://avigad.github.io/programming_in_lean/. Simon and I will try to get it into better shape. I hope to use it with the class in a few weeks.

Within the next couple of weeks, Mario and I need to start showing the class mathlib and showing them how to formalize "real" theorems. (Some will be more interested in writing little programs and proving things about their behavior.) I am a little anxious about that. We haven't yet figured out what to do, and I don't have good materials prepared. But we'll come up with something.

itp_assignments

[Joseph Corneli]

Glad to hear that PIL is moving - I hope I can share comments in a useful fashion. Feel free to use me as a guinnea pig prior to sharing the material with your class.