Cover Image for Ben Hutchison: exploring Lean programming

Presented by

Melbourne Compose is a monthly meetup for practitioners of typed functional programming, including the Haskell & Scala languages

Hosted By

8 Went

Tech

Ben Hutchison: exploring Lean programming

Name: Ben Hutchison: exploring Lean programming
Start: 2026-01-15T17:30:00.000+11:00
End: 2026-01-15T20:00:00.000+11:00
Location: Kathleen Syme Library and Community Centre

Melbourne Compose Group

Kathleen Syme Library and Community Centre

Carlton, Victoria

Past Event

Welcome! To join the event, please register below.

You will be asked to verify token ownership with your wallet.

About Event

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, 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 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

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

Location