This is just to illustrate how LEAN files can be shared publicly.
This is at https://share.cocalc.com/share/32a71772-8761-49d1-9134-6eb7f3fca4f5/public/?viewer=share/
Obviously, it would be nice if somehow information about that output were shared, but it isn't yet.