Visual Lean

An experimental graphical user interface for writing Lean code.

Lean verification runs locally on both desktop and mobile through WASM.

Start here: The Visual Natural Numbers GameProve the fundamental properties of arithmetic from scratch! → Elevator PitchTake a brief tour of Visual Lean's three modes. → The Natural Numbers Game ClassicPlay the Natural Numbers Game as it was originally designed, typing Lean code yourself. →

Credits

Visual Lean was designed and orchestrated by Autumn Mapes under the advisement of Timothy Gowers, Miles Cranmer, and Matthew Colbrook. It was coded with the help of Codex and Claude Code.

Visual Lean is built on a WASM port of Lean 4, Lean4.js, by Cauli Ziani.

The Natural Numbers Game was originally designed by Kevin Buzzard and Mohammad Pedramfar for Lean 3, then later ported to Lean 4 with the help of Jon Eugster. Alexander Bentkamp helped with the game engine, and Sian Carey, Ivan Farabella, and Archie Browne all helped add additional levels.

Special thanks to Joseph Claver for playtesting Visual Lean!

All source code is available publically on Github at the following repositories: Lean4.js and Github Pages hosting Lean4Game frontend engine Annotated NNG4 content Elevator pitch demo All are licensed with a GPL-3.0 license.