Melbourne Compose returns Thursday 15th Jan 2026: Ben Hutchison on "Exploring Lean Programming"
Ben Hutchison
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, Thurs 15th Jan, at our regular venue, Activity Room 2 at Kathleen Syme Center in Carlton. Arrive from 5:30 for chat and socialising, hands-on session starts 6:30pm. Please RSVP via Luma: https://luma.com/event/manage/evt-OS02c0amIeTIPVD
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 course exercises from "The Mechanics of Proof" by Heather Macbeth, which focuses on Lean's role as a mathematical proof assistant.
Textbook: https://hrmacbeth.github.io/math2001/index.html
Code: https://github.com/hrmacbeth/math2001
Lean Language, including tooling: https://lean-lang.org/
BYO laptop to get the most out of 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