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

[Rado Kirov]

This is great, thanks for sharing! I was just looking for more exercises after the natural number games and this proved a great next step (https://gist.github.com/rkirov/acea4b8d478a581cbd58190a864bf541 almost got the first problem solved, but there is an error still). The format is right, embed the VS code editor directly, no need for the extra hand-holding from the natural games.

I wonder if it would be better to provide some guidance on which mathlib theorems to use or finding the right ones is part of the challenge ( I used heavily claude, lean explore and apply?). A basic addition can be some way to save the editor state (in local storage or in the url directly).

One can imagine growing this style of exercises to something like the online programming challenges sites - https://www.codewars.com/kata, https://leetcode.com, https://www.codeabbey.com/ etc, but for short undergrad math proofs.

[metakuntyyy]

I've tried it out, it seems pretty good. Honestly the only thing I'm really missing is more games, not from you specifically but in general. The natural number game was very fun to play as it was an excellent introduction into lean.

[Kevin Buzzard]

It's hard to find topics for games which turn out as fun as NNG. Believe me I've tried.

[suhr]

Believe me I've tried.

It's hard to, since there's a lot of things that can be decomposed into cool little problems.

Honestly the only thing I'm really missing is more games, not from you specifically but in general.

I have quite a few exercises in the making, but it takes a lot of time to refine and organize them. By the way, NNG skips subtraction and division, while my book has exercises for them.

[Shreyas Srinivas]

One issue : I tried to change the settings of the lean editor to autocomplete upon enter and as usual I also asked the embedded editor to save my settings locally. This didn't work. So every time I open this book, I have to change this extremely inconvenient setting over and over.