Et si on pouvait s’assurer que nos démonstrations mathématiques sont totalement sans erreur, même dans leurs moindres détails ? C’est exactement ce que permettent les assistants de preuve, comme Lean. Ces outils sont conçus pour aider les mathématiciens à formaliser des théorèmes et leurs preuves de manière ultra-rigoureuse, en laissant l’ordinateur vérifier chaque étape. Dans cet exposé, je vous présenterai Lean, un des assistants de preuve les plus populaires aujourd’hui. On verra pourquoi ces outils deviennent incontournables, comment ils fonctionnent, et en quoi ils peuvent changer notre manière de faire des maths. À travers des exemples concrets, on explorera comment utiliser Lean pour prouver des théorèmes tout en découvrant ses limites et ses promesses.