Un aperçu de la façon de débuter avec Lean à partir de zéro
Lean est à la fois un langage de programmation fonctionnel polyvalent et un assistant de preuve. Il existe de nombreuses ressources pour apprendre Lean, certaines portant sur ses aspects de programmation, d'autres sur son utilisation comme démonstrateur de théorèmes.
Le livre Functional Programming in Lean est une introduction au paradigme de la programmation fonctionnelle avec Lean. Il s'adresse aux programmeurs qui veulent apprendre Lean, même s'ils n'ont aucune expérience préalable des langages de programmation fonctionnels.
Pour un examen plus approfondi de la démonstration de théorèmes avec Lean, le livre Theorem Proving in Lean 4 est répertorié comme ressource officielle.
The Lean Language Reference est la source faisant autorité pour obtenir des informations détaillées sur le langage.
De nombreuses ressources supplémentaires pour apprendre Lean sont mises à disposition par la Lean Community.