Lean Together 2019
Published:
From the 7th to the 11th of January, 2019, we hosted a workshop Lean Together in Amsterdam. This workshop was meant to serve a few purposes. First, it was a meeting for Lean developers and users who have been working remotely on the system and mathematics libraries. Second, it was a kickoff party for Jasmin Blanchette’s Lean Forward NWO project. A key part of this project is “mathematical outreach”; we want to put proof assistants in the hands of mathematicians, and through collaboration with computer scientists, advance the world of formal mathematics.
The workshop was an incredible success on both fronts. When we started planning in July, we expected to have around 30 participants; we ended up with 68 people registered. Amazingly, 29 self-identified their primary discipline as mathematics, and 29 as computer science. (Nine chose the “multidisciplinary” option and one wrote in “logic.”) It was great to meet more of the Lean crowd in person, and equally great to see the crowd eager novice formalizers.
We’re still feeling the momentum from this meeting and we hope to keep things rolling. Watch out for an announcement about Lean Together 2020: this time, it’s in Pittsburgh.