This is the course webpage for the Lean learning group, a participant-led crash course in the Lean programming language, a functional programming language that can be used as a proof verification system. The course is running in Spring 2023 under the auspices of the Glasgow-Maxwell School. Organizational and logistical support is being delivered by David Jordan, Patrick Kinnear and Adrián Doña Mateo.
When: Tuesdays 12:00 - 13:30.
Where: Bayes 1.35, Bayes Centre, Edinburgh; location tbc in Glasgow; online on Zoom, details circulated by email.
Chat: we have a private chat stream for the course on the Lean Zulip server. To join the chat, you should join this server, and send an email to Patrick to be added to the stream.
|Introducing Lean (slides). Natural number game. Zoom recording will be posted on Zulip.
|1. Join Zulip by clicking the link and following Sign Up in the top right hand corner. You will be added to the priovate course stream when you do that. 2. Install Lean and VSCode. 3. (Optional) finish as much of the natural number game as you want.
|Introduced Lean in VSCode, and how to get a project with
leanproject. Worked on sheet 01 of the tutorials project, rewriting equations. Introduced paired programming.
|Complete the installation, and ask on Zulip if any problems. Finish tutorials project sheet 01 if you didn't already.
|Worked on sheet 02 of the tutorials project, covering rewriting equivalences, implications and conjunction.
|Finish tutorials project sheet 02 if you didn't already.
|Logic crash course. Overview of the key tactics to work with first order logic. See demo code and selected exercises (all drawn from the tutorials project) in the following files: demo.lean, week4.lean. Remember to put these files in the
src folder of a lean project (e.g. the tutorials project) to work with them.
|Finish the selected exercises in week4.lean. Work on as much of the rest of sheets 01 - 08 of the tutorials project as interests you (see sheets 02 - 04 and 07 for more logic practice, some exercises already covered in week4.lean).
|Putting it together. Quick review of how to work with logical connectives and common tactics. Worked on sheet 09 of the tutorials project, on basic real analysis results. You can use the (updated) file cheatsheet.lean as a reference. Place it inside the
src folder in your project directory.
|In file 09 of the tutorials project, finish lemma 0071
le_lim if you haven't already, and try to fill as many
sorry as you can in lemma 0072
is_sup_iff. Don't worry too much if you get stuck.
|Reviewed and improved two solutions to last weeks problems. Learned about inductive types, structures and typeclasses, in preparation for mathlib. Files for this week: 09_collab.lean, week6.lean.
|Fill in the two sorries at the end of the week6.lean file to show that the product of two monoids is a monoid.
|Discussed type classes and class inference (week7.lean). Began exploring some algebra in mathlib using the sheet
thursday/groups_rings_fields.lean of Lean for the Curious Mathematician 2020. To get this lean project, run
leanproject get lftcm2020 in the terminal.
|Think about possible topics you would be interested in exploring in a group project, and contribute to the Zulip discussion on this. As a starting point, see the community pages here, here and here.
|Introducing git. Setting up and using git, making a pull request.
|Finish setting up and trying out git.
|Resolving merge conflicts in git. Discussion of group projects and setting goals for a hackathon.
|1. Participate in the Zulip poll to join a project group, and the date poll to inform a choice of date. 2. Start the process of making a docstring PR by: 2a Asking on the new members stream of Zulip to have access to the mathlib github; 2b Finding part of mathlib where you think you could write a documentation comment, or improve an existing one (it might help to look at areas you're thinking of working on a project on; 2c making your change and submit a PR on github. See this page for details, in particular the video tutorial linked at the start of the page explains the whole process. Please at least go through items 1 and 2a before the next class.
|Discussed and refined ideas for the upcoming hackathon group projects. Example of interacting with ChatGPT to begin formalising something in Lean.
|Participate in the poll to inform a choice of date.
We held a hackathon across two days on 25 April and 11 May. We worked on some group projects to formalise simplicial homology, the diamond lemma and PBW theorem, and Coxeter groups from various perspectives.