Ben Hutchison: exploring Lean programming

​Melbourne Compose is the monthly in-person meetup for functional programmers in Melbourne, every 3rd Thursday of the month in Carlton.

Our January meeting will be 5:30-8pm Nov 20th at our regular venue, Activity Room 2 at Kathleen Syme Center in Carlton. Arrive from 5:30 for chat and socialising, handson session starts 6:30pm. Please RSVP via Luma

This session will be an informal and hands-on exploration of the Lean 4 functional programming language and proof system, led by Ben Hutchison. Lean is having a massive impact on mathematics, revolutionizing the way that mathematics is expressed.

We'll base the session on the course examples from Tyler Josephson's course "Lean for Scientists and Engineers". The idea is to play around in VSCode and try to understand what is going on.

https://github.com/ATOMSLab/LFSE2024/tree/master/Lean%20Code

BYO laptop to get the most out of the session.

There's a series of lecture on youtube for the course at:
https://www.youtube.com/watch?v=s9Dyiu4S4vA
It's probably helpful to look at some of lectures 1 and 2 before the session, but not required. (I find them a bit slow and halting myself, and prefer to skip through on express.) We might watch or refer to parts of the lectures to decipher the examples during the session.

​As always, newcomers welcome. Reach Ben on 407 990094 if you have trouble accessing the venue.

Hope to see you there :)
-Ben Hutchison & John Walker