Is there a good website that provides a Lean 4 proof assistant service?

There are web-based environments for other languages, eg:

• Prolog has swish https://swish.swi-prolog.org
• Scheme has try.scheme https://try.scheme.org
• p5js has an online environment too https://editor.p5js.org

By “good” I mean: (1) simple and easy to use fro students / teaching, and (2) will likely be around in a few years and therefore safe to create teaching tutorials around.

Doing an internet search only located this one: https://live.lean-lang.org I am new to Lean so I don’t know if this the “official” preferred one.