Le LMV organise un colloquium grand public le mardi 10 octobre de 15h à 16h en amphi Bertin.
Nous aurons le plaisir d’accueillir Riccardo Brasca (IMJ-PRG) dont l’exposé s’intitule : « Autour de la formalisation : pourquoi et comment expliquer des mathématiques à l’ordinateur ».
Résumé : La formalisation est un processus qui consiste à utiliser l’ordinateur non pas pour calculer mais pour raisonner. Il est en train de devenir un outil puissant pour aider les mathématiciens et mathématiciennes dans leur travail de recherche. En effet, il est aujourd’hui possible de formaliser un résultat récent en un temps raisonnable, et les choses ne peuvent que s’améliorer dans les années à venir. Dans cet exposé, je vais décrire le processus de formalisation, avec des nombreux exemples, et je vais expliquer pourquoi ça peut être utile en mathématiques, dans le sens usuel du terme.
L’ensemble des membres du laboratoire est cordialement invité.
Groupe de travail
Plusieurs personnes de l’équipe AG sont intéressées par apprendre Lean (un assistant de preuve dont va nous parler Riccardo Brasca lors de son exposé). Nous souhaiterions réaliser un groupe de travail sur ce sujet qui se fera probablement sous la forme d’un projet commun à réaliser. La formalisation mathématique touche à tous les domaines, donc tout le monde motivé est convié.
Si vous souhaitez essayer Lean et apprendre les bases vous pouvez essayer le jeu en ligne « The Natural Number Game ».
Si vous êtes motivé par ce groupe de travail, il serait souhaitable d’avoir fait ce jeu au paravant.