In this course, we will learn how to work with the Lean 4 language. Please note that Lean 3 is very different.
Learning goals:
- Learn to read and write code in a functional style.
- Learn to work with Lean as a programming language.
- Learn to reason about your code in Lean.
Materials:
There is no Teams for this course. There is a Telegram chat; ask another course participant to add you, or ask me for an invite link via email.
If you do not want to use Telegram, just keep an eye on this repository and you should see everything as well.
If you would like to reach me, I recommend using the email komi.golov@jetbrains.com or using Telegram.
The course consists of weekly lectures, tutorial sessions, and homework assignments.
The lectures are at 9:45 on Friday. They are usually online, but exceptions will be announced occasionally.
The tutorial sessions are at 11:15 on Friday, and are on campus.
See Campus Net for up-to-date information on the rooms.
Homework assignments are available through GitHub Classrooms and must be handed in by 9:30 on Fridays (15 minutes before the lecture starts).
Your homework and exam contribute 50% of your grade each. You need at least 45% on both to pass.
The homework submission is organised via GitHub Classroom, see below.
There are no individual extensions, replacement exercises, or anything else of the sort possible for the homework.
The exam will be on paper. The date will be announced later.
There are some practice problems that you can do during the tutorial session. These do not need to be handed in and do not contribute to your grade.
Overview of lectures:
- Introduction to Lean.
- Function types and inductive types
- Programming in a functional style (no slides)
Homework links:
- https://classroom.github.com/a/QHKUQ38i
- https://classroom.github.com/a/24wWmmb_
- https://classroom.github.com/a/j-GTRfjs
Homework solutions are available in this GitHub
organisation soon after the deadline, look for the repo hwNN
and check for a solutions branch.