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 are asked to contact the organizers.
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.