Try it out here. You need a Google account cause the public playground last time ended up attracting low effort crypto miners. Also picked very basic compute instances to keep costs low (this also means startup times are slow). Lean naturally integrated into the execution model since their repl is mean to be used for machine to machine communication. Sadly the Lean integration is extremely slow from a cold start (Mathlib is HUUUGGGEE) but after you warm some tea and everything is loaded it should be fine.
Changes have been baking since this comment Sabela. Project is on github if you wanna contribute or follow updates.
