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 | More features of Math Comp (Assia Mahboubi, Cyril Cohen) | Documentation (Patrick Massot, Jeremy Avigad) | 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 | Patrick Massot and Johan Commelin | Simon Hudon | Discussion about Lean 4 (Sebastian Ullrich) Automation / Hammers (Jasmin C. Blanchette) | Lean in Education (Jeremy Avigad, Kevin Buzzard) | Collaboration time | |||

12 | 11:30 AM | Edward Ayers | ||||||||

13 | 12:00 PM | Lunch | Seul Baek | |||||||

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

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

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

17 | 1:45 PM | Mario Carneiro | ||||||||

18 | 2:00 PM | Tom Hales | Analysis (Jeremy Avigad) | Mathlib organization (Johannes Hölzl, Mario Carneiro) | ||||||

19 | 2:15 PM | Jesse Han | ||||||||

20 | 2:30 PM | Kevin Buzzard | ||||||||

21 | 2:45 PM | Sebastian Ullrich | ||||||||

22 | 3:00 PM | Reid Barton | ||||||||

23 | 3:30 PM | Coffee break | Coffee break | Coffee break | Coffee break | |||||

24 | 4:00 PM | Jeremy Avigad | Assia Mahboubi | Unification Hints (Assia Mahboubi, Cyril Cohen) Perfectoid Spaces (Patrick Massot) | Future Mathlib maintainers (Mario Carneiro) | |||||

25 | 4:30 PM | Minchao Wu | Jasmin Blanchette | |||||||

26 | 5:00 PM | Bruno Bentzen | Mario Carneiro (live coding) | |||||||

27 | 5:30 PM | |||||||||

28 | 6:00 PM | |||||||||

29 | 6:30 PM | |||||||||

30 | 7:00 PM | |||||||||

31 | 7:30 PM | Workshop dinner | ||||||||

32 | ||||||||||

33 | NOTES | NOTES | ||||||||

34 | All times are Amsterdam local time (UTC+1). | |||||||||

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

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

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

38 | We will have extra rooms available as working rooms: 11A-33 on Thursday, 10A-20 on Friday morning, and 05A-37 on Friday afternoon. | |||||||||

39 | ||||||||||

40 |

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:30 PM | Welcome and introductions | Johannes Hölzl and Robert Lewis | |

8 | 1:45 PM | The type theory of Lean | Mario Carneiro | |

9 | 2:15 PM | Towards a formalization of the independence of the continuum hypothesis | Jesse Han | We report on the progress of the Flypitch project, which aims to give a formal proof of the independence of the continuum hypothesis from ZFC. In particular, we describe joint work with Floris van Doorn on a completed formalization of the Gödel completeness theorem and the requisite deep embedding of first-order logic in Lean. |

10 | 2:45 PM | Lean 4 | Sebastian Ullrich | The next version of Lean is under heavy development. As a teaser, this talk will give a tour of the biggest user-facing features (and changes) as implemented or planned so far. |

11 | 3:30 PM | Coffee break | ||

12 | 4:00 PM | Quotients of polynomial functors | Jeremy Avigad | I'll discuss an algebraic method of constructing datatypes in Lean, inspired by Isabelle's bounded natural functors. (Joint work with Mario Carneiro and Simon Hudon.) |

13 | 4:30 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. |

14 | 5:00 PM | A Formalization of Henkin-style Completeness Proofs for Classical Propositional Logic and Propositional Modal Logic in Lean | Bruno Bentzen | In this talk, I will present a recent formalization of Henkin-style completeness proofs for classical propositional logic and propositional modal logic in Lean. The proof is constructed for Hilbert-style axiomatic systems with the false and implication as the only primitive logical connectives (and necessity as the only primitive modal operator). The full source code is available online at https://github.com/bbentzen/metalogic/ |

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 | We construct the p-adic numbers Q_p and integers Z_p in Lean, with various associated algebraic properties, and formally prove a strong form of Hensel's lemma. The proof lies at the intersection of algebraic and analytic reasoning and demonstrates how the Lean mathematical library handles such a heterogeneous topic. This is a first step taken toward the goals of the Lean Forward project. |

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

6 | 11:00 AM | The perfectoid project | Patrick Massot and Johan Commelin | A presentation on the perfectoid project, focusing on ring completions and sheaves. |

7 | 12:30 PM | Lunch | ||

8 | 2:00 PM | Formal Abstracts - an update | Tom Hales | I will give a report on the formal abstracts project and on formalization projects in Lean being carried out at the University of Pittsburgh. |

9 | 2:30 PM | Using Lean in undergraduate math education | Kevin Buzzard | I have been teaching mathematics undergraduates at Imperial College London about Lean, both formally (as an optional part of their introduction to proof course) and informally (on Thursday evenings at the Xena project, and last summer as part of a UROP). I will tell the story of how it started, what it has become, and where I want it to go. |

10 | 3:00 PM | Formalizing model categories in Lean | Reid Barton | I'll describe a project to formalize the Quillen model category structure on topological spaces. Part of the construction involves a generic method for carrying out inductive constructions while maintaining consistency invariants. |

11 | 3:30 PM | Coffee break | ||

12 | 4:00 PM | Intro to Coq's Mathematical Components library | Assia Mahboubi | The Mathematical Components Library [*] is a collection of verified mathematical theories, developed using the Coq proof assistant. It forms the bedrock of a verified proof of the Odd Order Theorem [**]. This talk proposes a short guided tour of this library, in terms of content, formalization methodology, issues and perspectives. [*] https://github.com/math-comp/math-comp [**] https://en.wikipedia.org/wiki/Feit-Thompson_theorem |

13 | 4:30 PM | So what are hammers good for? | Jasmin Blanchette | "Hammers" are tools that invoke automatic theorem provers (such as SMT solvers and superposition-based provers) to discharge proof obligations from proof assistants and that certify the externally found proofs. I will explain how they work and what to expect from them, and briefly describe ongoing work on a Lean hammer. I will also use this opportunity to talk about counterexample generators, which can also help boost user productivity, and about preliminary work on integrating them with Lean. |

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

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 | Human-oriented Term Rewriting | Edward Ayers | In this talk I will introduce a new approach for automating term rewriting with a prototype demonstration in Lean. The process works by generating trees of “subtasks” which represent classes of intermediate terms. In this way, the algorithm models how a human would approach a term rewriting problems. This will help to declutter files because it can prove steps in some proofs that humans find ‘obvious’ but existing automation might need prompting on. |

8 | 12:00 PM | A Verified Optimization of Cooper's Algorithm | Seul Baek | In this talk, I present an optimization of Cooper's algorithm using structured B-set extraction, verified in Lean and implemented as a reflected decision procedure. The optimization is a natural generalization of the block quantifier elimination method suggested by Cooper in his 1972 paper, which allows it to work with quantifier alternations. |

9 | 12:30 PM | Lunch | ||

10 | 7:30 PM | Workshop dinner | Join us for Indonesian food at Sama Sebo (http://samasebo.nl), P.C. Hoofdstraat 27, near the Rijksmuseum. |

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

2 | Time | Title | Speaker | Abstract |

3 | 9:00 AM | More about Math Comp | Assia Mahboubi and Cyril Cohen | |

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

5 | 11:00 AM | Automation / Hammers / Counter Example Finders | Jasmin C. Blanchette | |

6 | 11:45 AM | Discussion about Lean 4 | Sebastian Ullrich | |

7 | 12:30 PM | Lunch | ||

8 | 2:00 PM | Analysis | Jeremy Avigad | |

9 | 3:30 PM | Coffee break | ||

10 | 4:00 PM | Unification Hints | Assia Mahboubi and Cyril Cohen | |

11 | 4:45 PM | Perfectoid Spaces | Patrick Massot |

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

2 | Time | Title | Speaker | Abstract |

3 | 9:00 AM | Documentation | Patrick Massot, Jeremy Avigad | |

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

5 | 11:00 AM | Lean in Education | Jeremy Avigad, Kevin Buzzard | |

6 | 12:30 PM | Lunch | ||

7 | 2:00 PM | Mathlib organization | Johannes Hölzl and Mario Carneiro | |

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

9 | 4:00 PM | Further Mathlib Maintainers | Mario Carneiro |

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:30 | Welcome and introductions | Johannes Hölzl and Robert Lewis | |

7 | 1 Monday | 13:45 | The type theory of Lean | Mario Carneiro | |

8 | 1 Monday | 14:15 | Towards a formalization of the independence of the continuum hypothesis | Jesse Han | We report on the progress of the Flypitch project, which aims to give a formal proof of the independence of the continuum hypothesis from ZFC. In particular, we describe joint work with Floris van Doorn on a completed formalization of the Gödel completeness theorem and the requisite deep embedding of first-order logic in Lean. |

9 | 1 Monday | 14:45 | Lean 4 | Sebastian Ullrich | The next version of Lean is under heavy development. As a teaser, this talk will give a tour of the biggest user-facing features (and changes) as implemented or planned so far. |

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

11 | 1 Monday | 16:00 | Quotients of polynomial functors | Jeremy Avigad | I'll discuss an algebraic method of constructing datatypes in Lean, inspired by Isabelle's bounded natural functors. (Joint work with Mario Carneiro and Simon Hudon.) |

12 | 1 Monday | 16:30 | 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. |

13 | 1 Monday | 17:00 | A Formalization of Henkin-style Completeness Proofs for Classical Propositional Logic and Propositional Modal Logic in Lean | Bruno Bentzen | In this talk, I will present a recent formalization of Henkin-style completeness proofs for classical propositional logic and propositional modal logic in Lean. The proof is constructed for Hilbert-style axiomatic systems with the false and implication as the only primitive logical connectives (and necessity as the only primitive modal operator). The full source code is available online at https://github.com/bbentzen/metalogic/ |

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

15 | 2 Tuesday | 10:00 | A formal proof of Hensel's Lemma | Robert Y. Lewis | We construct the p-adic numbers Q_p and integers Z_p in Lean, with various associated algebraic properties, and formally prove a strong form of Hensel's lemma. The proof lies at the intersection of algebraic and analytic reasoning and demonstrates how the Lean mathematical library handles such a heterogeneous topic. This is a first step taken toward the goals of the Lean Forward project. |

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

17 | 2 Tuesday | 11:00 | The perfectoid project | Patrick Massot and Johan Commelin | A presentation on the perfectoid project, focusing on ring completions and sheaves. |

18 | 2 Tuesday | 12:30 | Lunch | ||

19 | 2 Tuesday | 14:00 | Formal Abstracts - an update | Tom Hales | I will give a report on the formal abstracts project and on formalization projects in Lean being carried out at the University of Pittsburgh. |

20 | 2 Tuesday | 14:30 | Using Lean in undergraduate math education | Kevin Buzzard | I have been teaching mathematics undergraduates at Imperial College London about Lean, both formally (as an optional part of their introduction to proof course) and informally (on Thursday evenings at the Xena project, and last summer as part of a UROP). I will tell the story of how it started, what it has become, and where I want it to go. |

21 | 2 Tuesday | 15:00 | Formalizing model categories in Lean | Reid Barton | I'll describe a project to formalize the Quillen model category structure on topological spaces. Part of the construction involves a generic method for carrying out inductive constructions while maintaining consistency invariants. |

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

23 | 2 Tuesday | 16:00 | Intro to Coq's Mathematical Components library | Assia Mahboubi | The Mathematical Components Library [*] is a collection of verified mathematical theories, developed using the Coq proof assistant. It forms the bedrock of a verified proof of the Odd Order Theorem [**]. This talk proposes a short guided tour of this library, in terms of content, formalization methodology, issues and perspectives. [*] https://github.com/math-comp/math-comp [**] https://en.wikipedia.org/wiki/Feit-Thompson_theorem |

24 | 2 Tuesday | 16:30 | So what are hammers good for? | Jasmin Blanchette | "Hammers" are tools that invoke automatic theorem provers (such as SMT solvers and superposition-based provers) to discharge proof obligations from proof assistants and that certify the externally found proofs. I will explain how they work and what to expect from them, and briefly describe ongoing work on a Lean hammer. I will also use this opportunity to talk about counterexample generators, which can also help boost user productivity, and about preliminary work on integrating them with Lean. |

25 | 2 Tuesday | 17:00 | Live coding session | Mario Carneiro | |

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

27 | 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. |

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

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

30 | 3 Wednesday | 11:30 | Human-oriented Term Rewriting | Edward Ayers | In this talk I will introduce a new approach for automating term rewriting with a prototype demonstration in Lean. The process works by generating trees of “subtasks” which represent classes of intermediate terms. In this way, the algorithm models how a human would approach a term rewriting problems. This will help to declutter files because it can prove steps in some proofs that humans find ‘obvious’ but existing automation might need prompting on. |

31 | 3 Wednesday | 12:00 | A Verified Optimization of Cooper's Algorithm | Seul Baek | In this talk, I present an optimization of Cooper's algorithm using structured B-set extraction, verified in Lean and implemented as a reflected decision procedure. The optimization is a natural generalization of the block quantifier elimination method suggested by Cooper in his 1972 paper, which allows it to work with quantifier alternations. |

32 | 3 Wednesday | 12:30 | Lunch | ||

33 | 3 Wednesday | 19:30 | Workshop dinner | Join us for Indonesian food at Sama Sebo (http://samasebo.nl), P.C. Hoofdstraat 27, near the Rijksmuseum. | |

34 | 4 Thursday | 9:00 | More about Math Comp | Assia Mahboubi and Cyril Cohen | |

35 | 4 Thursday | 11:45 | Discussion about Lean 4 | Sebastian Ullrich | |

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

37 | 4 Thursday | 11:00 | Automation / Hammers / Counter Example Finders | Jasmin C. Blanchette | |

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

39 | 4 Thursday | 14:00 | Analysis | Jeremy Avigad | |

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

41 | 4 Thursday | 16:00 | Unification Hints | Assia Mahboubi and Cyril Cohen | |

42 | 4 Thursday | 16:45 | Perfectoid Spaces | Patrick Massot | |

43 | 5 Friday | 9:00 | Documentation | Patrick Massot, Jeremy Avigad | |

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

45 | 5 Friday | 11:00 | Lean in Education | Jeremy Avigad, Kevin Buzzard | |

46 | 5 Friday | 12:30 | Lunch | ||

47 | 5 Friday | 14:00 | Mathlib organization | Johannes Hölzl and Mario Carneiro | |

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

49 | 5 Friday | 16:00 | Further Mathlib Maintainers | Mario Carneiro |