Lean Together 2019

Lean Together is a meeting for users (both current and future) and developers of the Lean proof assistant and its libraries, focusing on the formalization of mathematics. The 2019 meeting will also serve to kick off the Lean Forward project.

Many people have expressed interest in uniting the interactive theorem proving and mathematics communities. Indeed, one goal of Lean Forward is to gather mathematicians, formalizers, and tool developers together as a group. Participants from all areas are welcome at the Lean Together workshop, including those with little or no experience using proof assistants. We hope to establish cross-disciplinary connections and learn what each community needs from the other.

The workshop will include introductory tutorials, scientific talks, and collaboration time for developers and users. Tutorials will be aimed at a mathematically experienced audience with little background in formal methods. Presentation topics may include (but are not limited to) the development of formal theories and libraries, tools and automation for formalization, the use of proof assistants in mathematics and computer science education, translating between formal and informal mathematics, and theoretical aspects of proof assistants. We welcome relevant work in proof assistants other than Lean. Participants who are interested in giving a talk or running a tutorial or discussion are asked to contact the organizers.

Videos of the talks will be streamed and recorded.

Monday morning will have an introductory tutorial aimed at new and inexperienced Lean users.

Monday afternoon, Tuesday, and Wednesday morning will have a mix of scientific talks and tutorials. The tutorials will introduce audiences to mathlib and tactic programming.

Wednesday afternoon will be unscheduled time. There will be a workshop dinner Wednesday evening, 7:30pm at Sama Sebo (Pieter Cornelisz Hooftstraat 27, 1071BL Amsterdam).

Thursday, and Friday will have time for discussions and collaborations. Time will loosely be organized into sessions focusing on particular topics, but we also encourage people to work on projects. Lean experts will be available to advise beginners. Discussion topics will include proof assistants in education, the Formal Abstracts project, hammers for type theory, and managing mathlib.

Hotels in Amsterdam can be very expensive (although less so in January). There are more reasonably priced options in the neighboring city of Amstelveen. There is no official workshop hotel, but some participants have confirmed that they will stay at the Amsterdam Forest Hotel in Amstelveen. Alternatively, it is reasonable to stay farther from the VU campus and commute via tram (line 5 or 24), metro (line 51), or bicycle. The VU is also easily accessible from the Amsterdam Zuid train station.

We want to thank Mojca Lovencak and Caroline Waij for helping with the organization. This workshop is partially supported by the ERC Starting Grant 2016 Matryoshka (grant agreement No. 713999) and the NWO Talent Scheme Vidi 2017 Lean Forward (File No. 016.Vidi.189.037). We kindly ask participants to mention the support from the ERC and NWO in publications or in other kinds of scientific output that directly follows from the workshop.