1 | Lean Together program | |||||||||
---|---|---|---|---|---|---|---|---|---|---|

2 | Week of: | January 7 | ||||||||

3 | 1/7 | 1/8 | 1/9 | 1/10 | 1/11 | |||||

4 | MONDAY | TUESDAY | WEDNESDAY | THURSDAY | FRIDAY | |||||

5 | 8:00 AM | |||||||||

6 | 8:30 AM | |||||||||

7 | 9:00 AM | Intro to Lean | Intro to mathlib | Tactic programming | Suggestion: Perfectoid Spaces? | Talk | ||||

8 | 9:30 AM | |||||||||

9 | 10:00 AM | Rob Lewis? | Karl Palmskog? | Tutorial | ||||||

10 | 10:30 AM | Coffee break | Coffee break | Coffee break | Coffee break | Coffee break | ||||

11 | 11:00 AM | Intro to Lean, ctd | Tom Hales? | Simon Hudon? | Suggestion: Analysis (esp. Derivatives)? | Collaboration time | ||||

12 | 11:30 AM | Patrick Massot? | Edward Ayers? | |||||||

13 | 12:00 PM | Lunch | Johan Commelin? | Seul Baek? | ||||||

14 | 12:30 PM | Lunch | Lunch | Lunch | Lunch | |||||

15 | 1:00 PM | |||||||||

16 | 1:30 PM | Welcome + intros | ||||||||

17 | 2:00 PM | Johannes Hölzl? | Assia Mahboubi? | Suggestion: Lean in Education? | Suggestion: Further Mathlib Maintainers? | |||||

18 | 2:30 PM | Sebastian Ullrich? | Kevin Buzzard? | |||||||

19 | 3:00 PM | Mario Carneiro? | ||||||||

20 | 3:30 PM | Coffee break | Coffee break | Coffee break | Coffee break | |||||

21 | 4:00 PM | Jasmin Blanchette? | Jeremy Avigad? | Suggestion: Automation / Hammers / Counter Example Finders? | Suggestion: Documentation? | |||||

22 | 4:30 PM | Reid Barton? | Bruno Bentzen? | |||||||

23 | 5:00 PM | Mario Carneiro (Live coding)? | Minchao Wu? | |||||||

24 | 5:30 PM | |||||||||

25 | 6:00 PM | Workshop dinner | ||||||||

26 | 6:30 PM | |||||||||

27 | ||||||||||

28 | NOTES | TO DO | ||||||||

29 | Talk times and order are tentative, and may change before the event! | |||||||||

30 | All events are located in the Hoofdgebouw (main building) of the Vrije Universiteit Amsterdam. | |||||||||

31 | Events on Monday, Tuesday, and Wednesday will take place in room Agora 1 (floor 3). | |||||||||

32 | Scheduled events on Thursday and Friday will take place in room 08A-33 (floor 8). | |||||||||

33 | We will also use room 11A-33 (floor 11) as a working room. | |||||||||

34 | ||||||||||

35 |

1 | Monday schedule | |||
---|---|---|---|---|

2 | Time | Title | Speaker | Abstract |

3 | 9:00 AM | Introduction to Lean (tutorial) | Kevin Buzzard and Gabriel Ebner | An introductory tutorial about theorem proving in Lean. No background using Lean is expected, but participants should install Lean beforehand and bring a laptop. |

4 | 10:30 AM | Coffee break | ||

5 | 11:00 AM | Introduction to Lean, continued (tutorial) | Kevin Buzzard and Gabriel Ebner | An introductory tutorial about theorem proving in Lean. No background using Lean is expected, but participants should install Lean beforehand and bring a laptop. |

6 | 12:00 PM | Lunch | ||

7 | 1:00 PM | Welcome and introductions | Johannes Hölzl and Robert Lewis | |

8 | 2:00 PM | Johannes Hölzl | ||

9 | 2:30 PM | Lean 4: Reimplementing Lean in Lean | Sebastian Ullrich | |

10 | 3:30 PM | Coffee break | ||

11 | 4:00 PM | So what are hammers good for? | Jasmin Blanchette | what to expect and not to expect from different kinds of proof automation |

12 | 4:30 PM | Reid Barton | ||

13 | 5:00 PM | Live coding session | Mario Carneiro |

1 | Tuesday schedule | |||
---|---|---|---|---|

2 | Time | Title | Speaker | Abstract |

3 | 9:00 AM | Introduction to mathlib (tutorial) | Johannes Hölzl | A tour through the contents of Lean's mathematical library. |

4 | 10:00 AM | A formal proof of Hensel's Lemma | Robert Y. Lewis | |

5 | 10:30 AM | Coffee break | ||

6 | 11:00 AM | Formal Abstracts - an update | Tom Hales | |

7 | 11:30 AM | Patrick Massot | The perfectoid project | |

8 | 12:00 PM | Johan Commelin | ||

9 | 12:30 PM | Lunch | ||

10 | 2:00 PM | Assia Mahboubi | intro to Mathematical Components | |

11 | 2:30 PM | Kevin Buzzard | Using Lean in undergrad math education | |

12 | 3:00 PM | The type theory of Lean | Mario Carneiro | |

13 | 3:30 PM | Coffee break | ||

14 | 4:00 PM | Very Formal Logic | Jeremy Avigad | about implementing a logic toolbox in Lean (i.e. deep embedding logics, using them as a programming library, and proving things about them). |

15 | 4:30 PM | A Formalization of Henkin-style Completeness Proofs for Classical Propositional Logic and Propositional Modal Logic in Lean | Bruno Bentzen | |

16 | 5:00 PM | Verified decision procedures for modal logics in Lean | Minchao Wu | I'll be talking about a formalization of a tableau-based decision procedure for modal logic K in Lean. The formalization comes with conflict-driven backjumping as an optimization so the prover is algortihmically efficient. The verification includes termination, soundness and completeness of the algorithm with respect to the Kripke semantics, as well as the correctness of backjumping. The prover returns a Kripke model if a formula is satisfiable, or a proof of its being unsatisfiable if the formula is not satisfiable. When Lean 4 comes with vm_compute, this formalization can be turned into an automation by computational reflection. |

1 | Wednesday schedule | |||
---|---|---|---|---|

2 | Time | Title | Speaker | Abstract |

3 | 9:00 AM | Introduction to tactic programming (tutorial) | Simon Hudon | A tutorial on writing tactics and automation for Lean. |

4 | 10:00 AM | Regression Proving with Dependent Types: Theory and Practice | Karl Palmskog | Large-scale verification projects using proof assistants typically contain many proofs that must be checked at each new project revision. This process of regression proving can be time-consuming, lasting anywhere from tens of minutes up to several days, which negatively impacts user productivity. In recent work, we have explored techniques for speeding up regression proving in the Coq proof assistant, based on both proof-checking parallelization (via multi-core hardware) and proof selection (checking only proofs affected by a change). We have evaluated our techniques on the version histories of several large-scale Coq projects in program verification and mathematics. For example, we found that in continuous integration environments, fine-grained parallel checking with proof selection can be up to 28 times faster than sequential checking from scratch. We have also proposed a formal model in Coq of change impact analysis, validated against practical testing tools and build systems. We believe this model can be used to formally verify tools for incremental regression proving, increasing user confidence. In this talk, I will give an overview of our techniques, models, and empirical findings, and suggest how they can be leveraged in practice, both using Coq and other systems such as Lean. |

5 | 10:30 AM | Coffee break | ||

6 | 11:00 AM | Writing Temporal Logic Proofs in Lean: an exercise in embedding specialized proof languages | Simon Hudon | |

7 | 11:30 AM | Edward Ayers | human-like automation of proving simple equalities (in Lean) | |

8 | 12:00 PM | Seul Baek | ||

9 | 12:30 PM | Lunch | ||

10 | 6:00 PM | Workshop dinner |

1 | Thursday schedule | |||
---|---|---|---|---|

2 | Time | Title | Speaker | Abstract |

3 | 9:00 AM | Suggested discussion topic: perfectoid spaces | ||

4 | 10:30 AM | Coffee break | ||

5 | 11:00 AM | Suggested discussion topic: analysis | ||

6 | 12:30 PM | Lunch | ||

7 | 2:00 PM | Suggested discussion topic: Lean in education | ||

8 | 3:30 PM | Coffee break | ||

9 | 4:00 PM | Suggested discussion topic: hammers and automation |

1 | Friday schedule | |||
---|---|---|---|---|

2 | Time | Title | Speaker | Abstract |

3 | 10:30 AM | Coffee break | ||

4 | 12:30 PM | Lunch | ||

5 | 2:00 PM | Suggested discussion topic: social organization of mathlib | ||

6 | 3:30 PM | Coffee break | ||

7 | 4:00 PM | Suggested discussion topic: documentation |

1 | Day | Time | Title | Speaker | Abstract |
---|---|---|---|---|---|

2 | 1 Monday | 9:00 | Introduction to Lean (tutorial) | Kevin Buzzard and Gabriel Ebner | An introductory tutorial about theorem proving in Lean. No background using Lean is expected, but participants should install Lean beforehand and bring a laptop. |

3 | 1 Monday | 10:30 | Coffee break | ||

4 | 1 Monday | 11:00 | Introduction to Lean, continued (tutorial) | Kevin Buzzard and Gabriel Ebner | |

5 | 1 Monday | 12:00 | Lunch | ||

6 | 1 Monday | 13:00 | Welcome and introductions | Johannes Hölzl and Robert Lewis | |

7 | 1 Monday | 14:00 | Johannes Hölzl | ||

8 | 1 Monday | 14:30 | Lean 4: Reimplementing Lean in Lean | Sebastian Ullrich | |

9 | 1 Monday | 15:30 | Coffee break | ||

10 | 1 Monday | 16:00 | So what are hammers good for? | Jasmin Blanchette | what to expect and not to expect from different kinds of proof automation |

11 | 1 Monday | 16:30 | Reid Barton | ||

12 | 1 Monday | 17:00 | Live coding session | Mario Carneiro | |

13 | 2 Tuesday | 9:00 | Introduction to mathlib (tutorial) | Johannes Hölzl | A tour through the contents of Lean's mathematical library. |

14 | 2 Tuesday | 10:00 | A formal proof of Hensel's Lemma | Robert Y. Lewis | |

15 | 2 Tuesday | 10:30 | Coffee break | ||

16 | 2 Tuesday | 11:00 | Formal Abstracts - an update | Tom Hales | |

17 | 2 Tuesday | 11:30 | Patrick Massot | The perfectoid project | |

18 | 2 Tuesday | 12:00 | Johan Commelin | ||

19 | 2 Tuesday | 12:30 | Lunch | ||

20 | 2 Tuesday | 14:00 | Assia Mahboubi | intro to Mathematical Components | |

21 | 2 Tuesday | 14:30 | Kevin Buzzard | Using Lean in undergrad math education | |

22 | 2 Tuesday | 15:00 | The type theory of Lean | Mario Carneiro | |

23 | 2 Tuesday | 15:30 | Coffee break | ||

24 | 2 Tuesday | 16:00 | Very Formal Logic | Jeremy Avigad | about implementing a logic toolbox in Lean (i.e. deep embedding logics, using them as a programming library, and proving things about them). |

25 | 2 Tuesday | 16:30 | A Formalization of Henkin-style Completeness Proofs for Classical Propositional Logic and Propositional Modal Logic in Lean | Bruno Bentzen | |

26 | 2 Tuesday | 17:00 | Verified decision procedures for modal logics in Lean | Minchao Wu | I'll be talking about a formalization of a tableau-based decision procedure for modal logic K in Lean. The formalization comes with conflict-driven backjumping as an optimization so the prover is algortihmically efficient. The verification includes termination, soundness and completeness of the algorithm with respect to the Kripke semantics, as well as the correctness of backjumping. The prover returns a Kripke model if a formula is satisfiable, or a proof of its being unsatisfiable if the formula is not satisfiable. When Lean 4 comes with vm_compute, this formalization can be turned into an automation by computational reflection. |

27 | 3 Wednesday | 9:00 | Introduction to tactic programming (tutorial) | Simon Hudon | A tutorial on writing tactics and automation for Lean. |

28 | 3 Wednesday | 10:00 | Regression Proving with Dependent Types: Theory and Practice | Karl Palmskog | Large-scale verification projects using proof assistants typically contain many proofs that must be checked at each new project revision. This process of regression proving can be time-consuming, lasting anywhere from tens of minutes up to several days, which negatively impacts user productivity. In recent work, we have explored techniques for speeding up regression proving in the Coq proof assistant, based on both proof-checking parallelization (via multi-core hardware) and proof selection (checking only proofs affected by a change). We have evaluated our techniques on the version histories of several large-scale Coq projects in program verification and mathematics. For example, we found that in continuous integration environments, fine-grained parallel checking with proof selection can be up to 28 times faster than sequential checking from scratch. We have also proposed a formal model in Coq of change impact analysis, validated against practical testing tools and build systems. We believe this model can be used to formally verify tools for incremental regression proving, increasing user confidence. In this talk, I will give an overview of our techniques, models, and empirical findings, and suggest how they can be leveraged in practice, both using Coq and other systems such as Lean. |

29 | 3 Wednesday | 10:30 | Coffee break | ||

30 | 3 Wednesday | 11:00 | Writing Temporal Logic Proofs in Lean: an exercise in embedding specialized proof languages | Simon Hudon | |

31 | 3 Wednesday | 11:30 | Edward Ayers | human-like automation of proving simple equalities (in Lean) | |

32 | 3 Wednesday | 12:00 | Seul Baek | ||

33 | 3 Wednesday | 12:30 | Lunch | ||

34 | 3 Wednesday | 18:00 | Workshop dinner | ||

35 | 4 Thursday | 9:00 | Suggested discussion topic: perfectoid spaces | ||

36 | 4 Thursday | 10:30 | Coffee break | ||

37 | 4 Thursday | 11:00 | Suggested discussion topic: analysis | ||

38 | 4 Thursday | 12:30 | Lunch | ||

39 | 4 Thursday | 14:00 | Suggested discussion topic: Lean in education | ||

40 | 4 Thursday | 15:30 | Coffee break | ||

41 | 4 Thursday | 16:00 | Suggested discussion topic: hammers and automation | ||

42 | 5 Friday | 10:30 | Coffee break | ||

43 | 5 Friday | 12:30 | Lunch | ||

44 | 5 Friday | 14:00 | Suggested discussion topic: social organization of mathlib | ||

45 | 5 Friday | 15:30 | Coffee break | ||

46 | 5 Friday | 16:00 | Suggested discussion topic: documentation |