Skip to content

Latest commit

 

History

History
87 lines (63 loc) · 4.66 KB

README.md

File metadata and controls

87 lines (63 loc) · 4.66 KB
Raw

Atelier Lean 2023

Day 1, Tuesday May 2nd, 2023

Time Speaker Title
9.30-10.15 Riccardo

What does it mean to formalise and why do it
10.20-11.05 Filippo

Formalising Math 1
11.05-11.35

Coffee Break
11.35-12.20 Damiano

Generalizations, automation

library_search, simp, tactics
12.25-13.10 Filippo

Formalising Math 2
Lunch
15-??

Hacking session

Day 2, Wednesday May 3rd, 2023

Time Speaker Title
9.30-10.15 Damiano

Overview of Type Theory
10.20 -11.05 Filippo

Formalising some basic Number Theory 1
11.05 -11.35

Coffee Break
11.35-12.20 Riccardo

Lean Type Theory
12.25 -13.10 Filippo

Formalising some basic Number Theory 2
Lunch
15-??

Hacking session

Formalisation Talks

Three talks (Tue 10.30-11.15 and 12.30-13.15; Wed 10.30-12.00) are devoted to getting our hands dirty trying to formalise some mathematics. During the afternoon hacking sessions, participants will try to solve exercices that are similar to the ones seen in class. The files used both in the lectures and for the hacking sessions can be tested online without installing Lean locally.

For each exercise session, click on the corresponding link below. You might have to wait for a minute or so until "Lean is busy..." becomes "Lean is ready!". Then, you can type exactly as I did in class. The only difference is that, instead of the nice "goals accomplished 🎉" you will see a more modest "no goals".

Part A: Logic. The Class and the Tutorial

Part B: Functions. The Class and the Tutorial

  • Some Exercises on limits of real valued-functions.

Part C: Rings and Ideals. The Class and the Tutorial

Part D: some Number Theory

Links

  1. The Natural Number Game
  2. Lean community webpage
  3. Lean Zulip chat
  4. Damiano's slides on computers and maths
  5. Atelier PARI/GP, 2019

Cloning instructions

To clone this entire GitHub repository and install mathlib as a dependency, use

leanproject get https://github.com/adomani/Atelier_Lean_2023.git

This creates in the current directory a new directory called Atelier_Lean_2023, containing this repository and also a copy of mathlib.

Of course, the previous command assumes that you already have leanproject successfully installed on your computer.