cloud

Stream: general

[William Stein]

I enjoyed Kevin Buzzard's talk at the VANTAGE seminar recently about the FLT formalization process. Inspired by it, I made a Lean compute server image and corresponding video demo today for https://cocalc.com (a cloud computing platform I started):

https://youtu.be/H1KzvpgUyMU

and tutorial: https://github.com/sagemathinc/cocalc-howto/blob/main/lean.md

This is on CoCalc but is very different than the Lean file editor I wrote a couple of years ago that is integrated into the free version.  This is just a full normal VS Code with the Lean extension and Lake pre-installed, so is probably pretty similar to GitHub CodeSpaces, except much better pricing and more compute options.       In the video I demo using Kevin's FLT repo, so maybe it'll be useful to somebody working on that.

NOTE: There are ways to use LEAN entirely free in the browser, whereas what I've added to CoCalc and demo above is not free to use. It's potentially interesting for people that want easy access to very powerful compute (e.g., lots of CPU or RAM), and a collaborative stateful environment. Also, there are course management tools in cocalc -- there have been some big 200+ student lean courses taught via cocalc in the past.

Thanks, William