Flying now to Jerusalem, to give a mini-workshop on Lean for Mathematicians @leanprover at the Einstein Institute @HebrewU.

https://mathematics.huji.ac.il/event/lean-workshop-alex-v-kontorovich

(Unfortunately the workshop is oversubscribed already, with ~80 participants, so they're not taking more.)