Zulip Chat Archive

Stream: general

Topic: Using Lean Live for a tutorial session


Jineon Baek (Nov 11 2024 at 03:58):

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 (Nov 11 2024 at 07:07):

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

CC @Sebastian Ullrich

Sebastian Ullrich (Nov 11 2024 at 14:01):

@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 (Nov 11 2024 at 21:17):

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


Last updated: May 02 2025 at 03:31 UTC