A deeply interactive "user interface" for a slimmed down version of Lean4.