Show HN: Visual Lean: Learn to write Lean code with an accessible user interface

Category: devtools

Tags: lean4, webassembly, theorem-proving, education, interactive-proofs

Score: 7.8/10 (Innovation: 8, Technical: 9, Documentation: 8, Utility: 6)

Visual Lean is a browser-based Lean 4 playground and game platform that runs the real Lean compiler via WebAssembly in a Web Worker, enabling instant proof checking without a server. It includes ports of the Natural Number Game and Real Analysis Game with kernel-verified exercises, and innovative optimizations like a custom Lean fork, explicit WASM exports, and persistent environments for fast interactive performance.

Target audience: math students, educators, theorem proving enthusiasts, functional programmers

Repository: https://leangame.autumnofautumn.com/ · JavaScript · Apache-2.0 · 21 stars

View on Hacker News