Comment by dsksddfhsf

Previously: A real nice similar project using Coq: https://news.ycombinator.com/item?id=4014646

That's very polished, visually or at least typographically, which might not please everyone. But the idea of "proof by pointing" is solid.

OTOH the 'UX' of this Lean system is all over the place: being told to remove the word 'sorry' is a bizarre way to start. With my browser and reasonable font sizes, it's just not possible to make the column wide enough to get all the text on the same page. So the following paragraph refers to something that's not visible (because it's at the end of the text).

"At the bottom of the text in this box, there's a lemma, which says that if x, y and z are natural numbers then xy + z = xy + z. Locate this lemma (if you can't see the lemma and these instructions at the same time, make this box wider by dragging the sides). Let's supply the proof. Click on the word sorry and then delete it. When the system finishes being busy, you'll be able to see your goal -- the objective of this level -- in the box on the top right. [NB if your system never finishes being busy, then your computer is not running the javascript Lean which powers everything behind the scenes. Try Chrome? Try not using private browsing?]"

This paragraph is also bad because it's all jumbled up. There's advice on resizing the UI, there's a casual/vague comment on browser compatibility, and there's the random placeholder word "sorry" which appears to have no pedagogical purpose. All this as well as the fact that the lemma isn't yet visible.

From a UX, accessibility, and teaching aspect, there's a lot of room for improvement. The current state of this app really comes across as idiosyncratic rather than straightforward. The experience has got a complicated, intrusive, handmade personality rather than being a lucid exposition. Logitext has a particular personality as well but it's a slicker one. It hides the incidental complexity better (though the implementation isn't necessarily as simple as it should be).