Workgroup to learn Lean 4 @ IMT/LPT Toulouse
Hi everyone!
We have started a workgroup to learn Lean language to learn the basics of formalising mathematics, and we invite anyone interested in Toulouse to join this group. This website will be a repository of all the material covered in the workgroup, notes, videos, and lectures. We will also try to make the lean files available for reference. We hope that this will be a weekly thing, and people try to get a hands-on experience with the software. Hope to see you at the next meeting.
Aabhas Gulati and Ion Nechita
Thanks to Francois for providing all these proofs.
Homework was to formalise your favourite theorem in Group Theory. The lean file for theorems discussed in this session are available here. Thanks to Francois!
There are a few helpful resources, Groups and Lean and Formalisation of basic group theory in Lean.
We discussed the homework and we have updated the file with the proof.
We also discussed proofs of a basic theorem in group theory
If there is a group G such that for all $x \in G$, we have $x^2 = 1$, then it implies that the group is Abelian.
The lean file for this theorem can be found here
We went line by line through some simple proofs involving even numbers.
We decided on a homework for next time, following the lemma from this video.
Introductions and set-up. The main webpage for Lean 4
Installation instructions:
The Natural Number Game is a good place to start when learning the basics of Lean.
We briefly saw the proof of: composition of two surjective functions is surjective lean file