-
AG : Riccardo Brasca (IMJ-PRG) : Formalisation des mathématiques et l’assistant de preuve Lean
AG : Riccardo Brasca (IMJ-PRG) : Formalisation des mathématiques et l’assistant de preuve Lean
Résumé : Je vais parler dans cet exposé de formalisation des mathématiques, le processus "d'expliquer" des théorèmes à un ordinateur. J'expliquerais comment fonctionnent les assistants de preuve et pourquoi ils peuvent être utiles pour les mathématiciens. Je raconterai aussi l'histoire