Try Lean the Easy Way

You can easily run Lean code right in your browser using Lean 4 Web.

A Little More Detail

You don’t need to follow the official guide to install this, set up that, and run those complicated commands.

Just open Lean 4 Web in your browser, and you can run simple Lean code with ease.

For the kind of Lean code I write, Lean 4 Web is more than enough. In fact, it’s what I use almost all the time.

Try it out! Just copy and paste the code below into Lean 4 Web.

theorem one_plus_one_is_two : 1 + 1 = 2 := by
  -- Since 2 is defined as 1 + 1 in the standard library,
  -- the proof is true by definition.
  rfl

below is result