Χρήσιμοι πόροι για το Lean

Μια συλλογή χρήσιμων πόρων που θα σε βοηθήσουν να κατακτήσεις το Lean

  • Ο επίσημος ιστότοπος είναι το κύριο αποθετήριο περιεχομένου για τη γλώσσα. Έχει ένα διαδικτυακό playground όπου μπορείς να δοκιμάσεις τη γλώσσα χωρίς να εγκαταστήσεις τίποτα.
  • Το Reservoir ευρετηριάζει, χτίζει και δοκιμάζει πακέτα στο οικοσύστημα Lean και Lake. Είναι το μέρος όπου θα βρεις πακέτα τρίτων.
  • Η Lean Community είναι ένα συνεργατικό δίκτυο ανοιχτού κώδικα γύρω από το οικοσύστημα Lean. Είναι υπεύθυνη για το mathlib, τη βασική βιβλιοθήκη μαθηματικών για το Lean 4, που τη διαμορφώνει η κοινότητα.
  • Το Lean 4 Zulip Chat είναι το κύριο κανάλι συζήτησης για την Lean Community.