search

leanprover-community / leanprover-community.github.io

Hosts the website for mathlib and other Lean community infrastructure.
https://leanprover-community.github.io/
MIT License
53 stars 123 forks source link

Modification to "Book" paragraph in Learning Lean 4 page #439

Closed motib closed 3 months ago

motib commented 9 months ago

Add link to my tutorial "A Gentel Introduction to Lean" Rewrote the paragraph "Books" for consitency and clarity, also changing the name to "Documents".

turibe commented 6 months ago

I believe that "How to prove it with Lean" still uses Lean 3?

PatrickMassot commented 6 months ago

@turibe, thanks for your help, but actually that project was ported to Lean 4, see https://github.com/djvelleman/HTPILeanPackage/tree/master.

However this project is pretty different from the ones that are already mentioned and the maintainer team already decided not to include it in this specific list. We will think about the other document and report back.

turibe commented 6 months ago

Thanks, I was hastily judging by https://djvelleman.github.io/HTPIwL/IntroLean.html, which does not mention a version. (All such pages should ideally mention which version of Lean they refer to / were tested on, but many don't... it gets confusing.) p.s. Looking closer, I do see one version hint there : "“Lean 4: Infoview: Toggle” :-) , so that's Lean 4 too.

jcommelin commented 3 months ago

@motib Yesterday we had a triage meeting for pull requests to the website. We decided that we want to use this list for resources that have an established track record in the community of being a good resource for beginners.

We are happy that you wrote your introduction to Lean, but we do not think that it should be included in this list.