update lean-lang.org

Stream: general

[Bulhwi Cha]

From https://lean-lang.org/download/:

There is also an online version providing recent versions of Lean 4, std4, and mathlib4.

Should we change "std4" to "batteries"? It links to Batteries anyway.

[Johan Commelin]

cc @David Thrane Christiansen

[Joachim Breitner]

Fixed

[David Thrane Christiansen]

Thanks for the report, @Bulhwi Cha, and @Joachim Breitner for taking care of it on the weekend :)

[Niels Voss]

I just visited Chapter 6 of Theorem Proving in Lean 4, under "Using the Library", and it also links to std4, but this time it gives a 404:
https://leanprover.github.io/theorem_proving_in_lean4/interacting_with_lean.html#using-the-library

[Michael Rothgang]

Speaking of which: the "next steps" section of FPIL is outdated, as it

• refers to std4 (which should now be batteries, and std should be mentioned)
• does not know the mathlib port was finished

[Bulhwi Cha]

I guess the FRO will revise these documents in the future.