An­nounc­ing Lean­ing In! 2025

I'm hap­py to an­nounce the first edi­tion of Lean­ing In!, a one-day work­shop ded­i­cat­ed to the Lean pro­gram­ming lan­guage and the­o­rem prover. The kick­off edi­tion will be Thurs­day, March 13, 2025 in Berlin, Ger­many.

For a few years, I've had my eye on Lean but didn't do any­thing with it. Re­cent­ly, it seems that Lean has achieved launch sta­tus. As a prac­ti­tion­er in the the­o­rem prov­ing com­mu­ni­ty, I'd been aware of Lean for some time (go­ing back to v1, when it came out), but wasn't work­ing quite in that area, so I lost track of Lean un­til it popped up on my radar again be­cause of the many good things I kept hear­ing. The lan­guage it­self, the tool­ing around it, the com­mu­ni­ty, its won­der­ful (and won­der­ful­ly large and grow­ing) li­brary of math­e­mat­ics…all signs are look­ing up. I've been play­ing around with it for about a year now in earnest, and am hav­ing a lot of fun. Or­ga­niz­ing Lean­ing In! is my way of con­tribut­ing back to the com­mu­ni­ty.

To sub­mit a talk, just go here. To reg­is­ter for the con­fer­ence, just fill out the same form, leav­ing the talk ti­tle & ab­stract bit blank.

See you in Berlin!