Are you ready for Lean in Hanoi?

This repository contains exercises and supplementary materials for the Hanoi Lean 2019 workshop.

To get started, first make sure that Lean is installed and you have the update-mathlib script (see install instructions here).

Open a terminal and run

git clone https://www.github.com/jesse-michael-han/hanoi-lean-2019

cd hanoi-lean-2019

leanpkg configure

update-mathlib

The exercises are in the /src directory.

Schedule

	DAY 1 (introduction, basics)	DAY 2 (tactics, metaprogramming)	DAY 3 (mathlib, library-building)	DAY 4 (formal abstracts, formal blueprints)
10:00-10:50	Hales	Han	Lewis	Vajjha
	Formal Abstracts - A Vision	Tactics and automation	Typeclass inference in Lean	Documentation for formal abstracts
10:55-11:10	Morning break	Morning break	Morning break	Morning break
11:10-12:00	Lewis	Vajjha	van Doorn	Mark Adams
	Introduction to Lean I	Introduction to metaprogramming	Introduction to mathlib	Organization of formal abstracts
	(Chapters 6 and 1-3 of TPIL)
12:00 - 1:45	Lunch	Lunch	Lunch	Lunch
1:45-2:35	Trung	Baek	van Doorn	Hales
	Introduction to Lean II	Writing tactics	Best practices for library-building	Formal abstracts - the way forward
	(Chapters 5-8 of TPIL)			Suggested projects
2:35-3:25	Trung	Baek	van Doorn	Working groups (suggested projects)
	Group theory in Lean	omega	Exercise session
3:25-3:40	Afternoon break	Afternoon break	Afternoon break	Afternoon break
3:40-4:30	Exercises/working groups	Hanoi Lean Working Group	Exercises/working groups	Working groups (suggested projects)
		TBD