Vidéo de l'IREM de Paris - Le Maths Club. Utiliser l'ordinateur pour faire des démonstrations mathématiques : une introduction aux assistants de preuve.

Résumé

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é, l'auteur présente 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 explore comment utiliser Lean pour prouver des théorèmes tout en découvrant ses limites et ses promesses.

Notes

Conférence donnée le 03 février 2025 dans le cadre de la chaine "Le Maths Club" des vidéos de l'IREMS de Paris.

Le Maths Club propose depuis 2008 un séminaire à l'intention des étudiants en mathématiques et informatique de niveau L et M, mais les séances sont ouvertes à tous ! Le sous-titre du séminaire est "Les Maths, à quoi ça sert ?". Les conférenciers sont par exemple des chercheurs, des enseignants, des industriels.
Ce séminaire est organisé conjointement par l'UFR de Mathématiques de l'Université Paris Diderot et par l'IREM de Paris.

Cette ressource est en ligne sur le site Vidéo de l'IREM de Paris

Données de publication

Éditeur IREM de Paris , Paris , France , 2025 Format 1h

Public visé élève ou étudiant, enseignant Niveau licence, lycée, terminale Âge 17, 18, 19, 20

Type Film, vidéo Langue français Support internet