VScode in the browser

Stream: general

[Johan Commelin]

Has anyone seen https://spiffcode.github.io/ghedit/ before?

[Johan Commelin]

Pretty cool stuff. Now we only need a server farm to run lean in the backend, and then we can have an online workflow that actually works (I hope)

[Johan Commelin]

Maybe this is something the CoCalc is interested in. I might actually send William Stein an email. Then we can have collaborative lean. That would be a lot of fun.

[Kevin Buzzard]

I have spent some time talking to William about Lean, and I have used Lean within cocalc.

[Kevin Buzzard]

But we're not ready

[Kevin Buzzard]

because we are waiting for a stable lean and a stable mathlib

[Kevin Buzzard]

and the moment we have it

[Kevin Buzzard]

we will have multiplayer lean

[Kevin Buzzard]

@Sebastian Ullrich -- are we currently waiting for a new stable Lean? I am unsure what is happening.

[Kevin Buzzard]

Johan, please email William with your ideas.

[Johan Commelin]

Johan, please email William with your ideas.

Done

[Sebastian Ullrich]

@Kevin Buzzard I'm planning to release 3.4.1 today

[Kevin Buzzard]

That is half of the great news I am looking forward to.

[Kevin Buzzard]

The other half being when Mario says that mathlib works fine with it.

[Kevin Buzzard]

@Sebastian Ullrich I stayed up for 24 hours straight yesterday talking on this forum about how to get Lean to accurately model an extremely subtle concept which mathematicians take for granted and which is deeper than they think. Lean is a perfect language for mathematicians and I am continually reminded of this. Thank you to you and @Gabriel Ebner for being the bridge between Lean and mathematicians and I really look forward to working together in the future.

[Kenny Lau]

lol you have a lecture in 2 days and you just messed up your sleeping schedule

[Kevin Buzzard]

A powerful and stable release of Lean and Mathlib makes teaching so much easier, and I feel that we are nearly there.