Orateur
Filippo Nuccio
(Institut Camille Jordan)
Description
Dans la première partie de mon exposé je vais faire un petit
survol de comment l'assistant de preuve Lean est capable de
"comprendre" des définition d'objets mathématiques, des énoncés de
théorèmes, et des preuves. Je parlerai ensuite d'un travail commun
avec A. Baanen, S. Daamen et Ashvni N., où on a formalisé une preuve
de la finitude du groupe de classes d'idéaux pour un corps global en
Lean.
