Really cool idea. I've been curious about theorem provers but never tried one out. I had a quick look at this on my phone (so, maybe not representative UI).
Some things that I think could be improved:
It tells you to click on "Tutorial world", but there is no such button. You have to click "Start" before you see it.
It doesn't tell you what "rfl" stands for.
It doesn't tell you where the "two_eq_succ_one" etc. come from. Are these axioms? Are there infinitely many of them? Are they always available in Lean or are they part of the tutorial world? Why refer to numbers with names instead of digits?
The thing where you have to type "\l" when you want a unicode arrow feels pointlessly obtuse. Why not make it "<-" or something? If humans are going to type it, it should be made out of characters typically found on keyboards.
And I stopped because I got annoyed with typing on my phone. Might try again when I get to a real computer.
EDIT: I just looked it up. "rfl" stands for "reflexivity". Also "rw" is meant to automatically do "rfl" but I think I found that I had to manually do "rfl" after "rw" in the tutorial. https://lovettsoftware.com/NaturalNumbers/Tactics.lean.html
And "two_eq_succ_one" is part of the tutorial world but there are only a small handful of them. In my opinion it is important to distinguish for newbies what is actually part of the system they're learning to use and what is merely part of their learning environment.
Theorem providers should be treated as interactive. I don't know how Lean works but I know how Isabelle works. Reading Isabelle proofs in plain text (e.g. in the seL4 verification repository on GitHub) is completely useless. However, when you open one in Isabelle's IDE, you can click on any point in the proof and show the internal state of the verifier - what the current statement being proved is, so you can see how the last tactic modified it. You can also search for names of theorems and axioms by matching templates (e.g. "?a*(?b+?c)=?d" will match the law of distributivity and maybe some other stuff)
Some things that I think could be improved:
It tells you to click on "Tutorial world", but there is no such button. You have to click "Start" before you see it.
It doesn't tell you what "rfl" stands for.
It doesn't tell you where the "two_eq_succ_one" etc. come from. Are these axioms? Are there infinitely many of them? Are they always available in Lean or are they part of the tutorial world? Why refer to numbers with names instead of digits?
The thing where you have to type "\l" when you want a unicode arrow feels pointlessly obtuse. Why not make it "<-" or something? If humans are going to type it, it should be made out of characters typically found on keyboards.
And I stopped because I got annoyed with typing on my phone. Might try again when I get to a real computer.
EDIT: I just looked it up. "rfl" stands for "reflexivity". Also "rw" is meant to automatically do "rfl" but I think I found that I had to manually do "rfl" after "rw" in the tutorial. https://lovettsoftware.com/NaturalNumbers/Tactics.lean.html
And "two_eq_succ_one" is part of the tutorial world but there are only a small handful of them. In my opinion it is important to distinguish for newbies what is actually part of the system they're learning to use and what is merely part of their learning environment.