Lean 4 in the browser

This is Lean 4 running in your browser. Edit the theorem, press Run and play with the code without installing Lean or setting up a local project.

One that passes

rfl is short for reflexivity. Equality is a reflexive relation, meaning x = x for every value x, and Lean accepts rfl when both sides reduce to the same expression. Press Run.

One that fails

This one says 2 + 2 = 5, so Lean rejects it. Change the numbers, edit the proof or type your own theorem.

Equality from scratch

If a = b and b = c, then a = c; this is transitivity, the property proved here. The two cases steps substitute equal values. After those substitutions, the goal is a = a. This final goal uses a different property, reflexivity (rfl), which says every value is equal to itself.