Πώς να μάθεις το Lean

Το Lean είναι ταυτόχρονα μια συναρτησιακή γλώσσα προγραμματισμού γενικού σκοπού και ένας βοηθός απόδειξης. Υπάρχουν πολλοί διαθέσιμοι πόροι για να μάθεις το Lean, με κάποιους να εστιάζουν στις πτυχές προγραμματισμού του και άλλους στη χρήση του ως αποδεικτή θεωρημάτων.

Το βιβλίο Functional Programming in Lean είναι μια εισαγωγή στο παράδειγμα του συναρτησιακού προγραμματισμού με τη χρήση του Lean. Απευθύνεται σε προγραμματιστές που θέλουν να μάθουν το Lean, ακόμη και αν δεν έχουν προηγούμενη εμπειρία με συναρτησιακές γλώσσες προγραμματισμού.

Για μια πιο εμβριθή ματιά στην απόδειξη θεωρημάτων στο Lean, το βιβλίο Theorem Proving in Lean 4 αναφέρεται ως επίσημος πόρος.

The Lean Language Reference είναι η έγκυρη πηγή για λεπτομερείς πληροφορίες σχετικά με τη γλώσσα.

Πολλοί επιπλέον πόροι για την εκμάθηση του Lean διατίθενται από την Lean Community.