[asdftemp]

that is a neat demo with a lot of useful links! In fact, it seems that the Lean developers/community are very interested in new methods of achieving readability, and providing users with tools to build interfaces that scale up to the complexity of real workflows.

For example, Lean in vscode supports interactive html "widgets": https://youtu.be/8NUBQEZYuis?t=453

(at that timestamp, there's a quick introduction to their typical use at the moment).

lean4 is committed to all sorts of extensibility; here's a demonstration of the new macros: https://twitter.com/derKha/status/1354082976456441861. There have also been several instances of users implementing old lean3 features (for example, the `calc` tactic mode, which has unique syntax for proving (in)equalities) by simply defining new type classes and short macros.