Hello World

Stream: new members

[David Spies]

Hey, I'm trying to get started with Lean and mathlib, but I can't seem to get "Hello, World" working. I think it's some sort of 403 error when it attempts to download the dependency, but I don't know how to tell because all the set-up resources say to use the VSCode UI which doesn't give obvious feedback rather than command-line tools (Despite being a fan and regular user of VSCode, I'm a bit perplexed by the decision to bake it into the main setting-up tutorial)

[David Spies]

Oof, thanks
Is there somewhere I can check the current status/for updates?

[Matt Diamond]

also, https://live.lean-lang.org is functional if you just want something to play around with

[Adam Millar]

Hello,
I'm Adam Millar.
I did a little bit of LEAN ~5 years ago with Mario and Jeremy as a masters' student at CMU.
I am .... very ... rusty, but I am trying to return to the world of LEAN, most likely from a pedagogical perspective to help undergraduate math and computer science students see the connections between Logic, Proof-Based Math, and Computer Science.
.... does anyone have a suggestion on where to begin?

[Patrick Massot]

https://leanprover-community.github.io/teaching/index.html

[Damiano Testa]

Depending on how rusty you are, you may or may not notice that now (almost) everyone is using Lean 4, instead of Lean 3.