feedback on early prototype for Lean for Mathematicians

Stream: general

[Alex Kontorovich]

I got some encouragement at the ICERM meeting on this prototype:

https://sites.math.rutgers.edu/~alexk/TestRealAnalysis.html

and wanted to stress test it / get some more feedback from the experts on here. The idea is to allow people to hop right on (no installation, no papercuts, just web app) and experiment with nonzero (but easy) math content, in an environment where they have the full freedom to type whatever they want (unlike Natural Number Game which carefully controls what's allowed).

The user is meant to read each exercise, and click on the "Open Lean Editor" button, which pops up a bottom frame preloaded with the desired content for that exercise, running live.lean-lang.org. When they're satisfied with playing with that exercise, they click the same button to "Close Lean Editor", then move on to the next exercise. [This might be interesting to implement also with Mathematics in Lean...]

Any comments/suggestions would be very welcome! (Perhaps it's better for such to be sent by DM to me, so as not to clog the general discussion?) Thanks!

[Aaron Hill]

A couple of minor suggestions:

• Clicking one of the 'Open Lean Editor' buttons currently changes all of the buttons to 'Close Lean Editor', instead of just the one you opened
• In Exercise 1, there's no by in the sorried theorem and example

[Frederick Pu]

I think this might overlap with verso. Mb there could be an excercise mode for verso

[Quang Dao]

Minor style issue: the sidebar doesn’t resize / can’t be minimized, so it takes up almost the whole screen on mobile

[Frederick Pu]

mb we could have notebook style format with a bunch of code blocks and single infoview on the side

[Frederick Pu]

that way you can also be able to export a single lean file at the end too