Using Lean Live for a tutorial session

Stream: general

[Jineon Baek]

We (me with @Kyu-Hwan Lee, @Byung-Hak Hwang, etc.) plan to host a Lean tutorial session for Korean mathematicians. There are around 30~40 people in the session and we plan to use https://live.lean-lang.org/ for them to easily access the Lean interface. The session will hold for 1.5 hours afternoon in Korea time. In your time, it is:

https://www.timeanddate.com/worldclock/fixedtime.html?iso=20241217T15&p1=235&ah=1&am=30

1. Will the Live Lean server be able to handle this workload?
2. Is such a usage discouraged? I understand if so, as the server is meant for general use. In such a case we are willing to set up a local server.

[Henrik Böving]

Thanks for telling us! We had previously seen load and couldn't tell where it was coming from.

CC @Sebastian Ullrich

[Sebastian Ullrich]

@Jineon Baek Thanks for reaching out! Yes, we are happy to provide this infrastructure not only for individual experimentation but small-medium size classes as well. While we've heard good things about holding classes there for up to 50 people, we have just doubled the RAM of the server to make extra sure!

[Jineon Baek]

Thank you so much for your generosity and extra help!! Much appreciated :) @Sebastian Ullrich

[Yee-Jian Tan]

@Henrik Böving do you know roughly how much resource (memory, CPU, storage) would be enough if I want to set up a local server for a peak usage of about 150 people for 2h?