Lean for Algorithms

Hi all,

As you might recall, I mentioned that the Array.get functions appear to have changed as I got stuck there for a moment. 

Previously there were three functions: Array.get (a[i]) , Array.get! (a[i]!), and Array.getD (a[i]?). These have respectively become Array.getInternal, Array.get!Internal, and Array.getD

Nevertheless they retain the previous type signatures and you can see from the docstring of get!Internal that it accepts only the Nat index i and if the index is out of bounds, it "panics". In lean terms, this means the function returns the `default` value from the `Inhabited` typeclass.

Best Regards,

Shreyas

As some of you have pointed out, the description of Exercise 3 doesn't match the file provided; it has an unnamed example instead of a theorem called Foo2, and is missing the #check for the CommSemiring instance.
I have updated the file Ex3.lean on the exercise repository; you can submit your assignment using either version since this doesn't affect the overall objective of the exercise.

The file for Assignment 2 has been updated to have the correct induction syntax in exercise 2.

 

You can find the challenge from today's exercise class at codeberg.org/Chipi/lfa2026-challenges; let me remind you here that these challenges are completely optional and meant to be solved with every tool at your disposal, including working in groups. I will publish a solution to Challenge 1 on the same repository in two weeks; if any individual or group solves it and wants to show off their solution, they can email it to me and it will be published at the same time. Include a group name or you will be assigned a random bird name.

 

Best regards, Chiara

Good morning!

The first assignment, the lecture slides and the lecture demo are available both here at CMS Materials folder and in our exercise repository that you need for solving the exercises: https://codeberg.org/Henkkuli/lfa2026/

During the lecture, I forgot to mention the following regarding about assignments: to attend the exam, you need to get 50% of the overall assignment points, divided such that you get at least 40% of the assignment points in each of the three modules (weeks 1–4, 5–9 and 10–14).

We also have our first exercise session today at 14:00. Normally, in the exercise sessions, we will be providing model solutions for the previous week's exercises, answering questions, and also handing out extra exercises for practice. This week, instead, we will be providing help with setting up the Lean environment and understanding how to turn in the assignments. The exercise sessions can also function as reserved time slots in your calendars when you can work on the exercises.

Best,
The course personnel

Welcome on the Lean for Algorithms course!

The first course activity will be our first lecture on Tuesday October 13 at 14:15 – 16:00, and then the exercise class on Thursday October 15 at 14:00 – 17:00; we have decided to extend the exercise session by an hour for those who have scheduling conflicts before 16. All of our course activities will be held E9 1, 0.05 (CISPA building, lecture hall on ground floor).

Before the first class, we recommend everyone to install the Lean tool chain, including VS Code, following the official instructions.

Best,
The course personnel