Le logiciel Lean permet de parler de maths de tout niveau à son ordinateur. Il peut aussi servir à enseigner le raisonnement mathématique rigoureux, par exemple en L1. Ce TP sera une introduction à l’utilisation de Lean en pratique. Il n’y a aucun pré-requis si ce n’est de venir avec un ordinateur portable.