Fun Exists

Fun ∃ pronounced the same as "fun e" or "funny".

We are a group interested in mathematical programming for fun. This includes, but is not limited to: puns, game development in Lean and talks on Proof Assistants and Dependently Typed Programming.

Projects

RayLean: Lean4 bindings for Raylib
Jessica Can't Swim: a game built using Raylean
Coq Lean Cheatsheet: a Cheatsheet for people transitioning from Coq to Lean

Presentations

The Little Typer reading group (Stellenbosch 2025)
Correct Code by Construction (London 2022)
Advertising Coq (Stellenbosch 2020)