Intro to Proofs at Johns Hopkins

Stream: Lean for teaching

[Sina]

This semester I am teaching an Intro to Proofs course at Johns Hopkins to a mix of first and second year undergraduates and senior high school students. Today we had our install party, and we did some very basic rewrite exercises.

This course takes great inspiration from Mathematics in Lean and will be a lot like it, except that in our course functions appear before logic and we do a good deal more abstract algebra, including categories and functors.

If you are or know somebody who is interested in joining this course remotely, there is a Zulip server for this course at https://introproofs.zulipchat.com/. All the course materials can be found on the Zulip server of the course (including link to recorded lectures). If interested, you can DM me and I can send an invite link to this server.