7 mai 2019

Patrick Massot (LMO)
Introduction aux mathématiques formalisées

Plus d'infos...

Lieu : 0D10

Résumé : Dans cet exposé-TP, j’essaierai de répondre à quelques questions qui
m’ont été posées durant des pauses café récentes : que signifie « expliquer
une définition ou une démonstration mathématique à un ordinateur » ?
Est-ce faisable sans formation en logique ou informatique ?
Cela pourrait-il être utile aux mathématiciens ? Peut-on l’utiliser pour
enseigner ?
Dans un premier temps, je ferai un exposé sur ces questions, en
m’appuyant sur l’exemple de la définition des espaces perfectoïdes,
expliquée très récemment aux ordinateurs, et sur des exemples
de cours en L1 utilisant la vérification de démonstrations par
ordinateur, à Londres et à Orsay. Il n’est pas nécessaire de savoir ce
qu’est un espace perfectoïde ou un étudiant de L1, je ferai des rappels.
Dans un deuxième temps, je guiderai l’auditoire pour écrire ses
premières définitions et démonstrations formalisées.
Note : La partie TP requiert de se connecter aux machines des salles
informatique de notre bâtiment.
=============

Introduction aux mathématiques formalisées  Version PDF

Cyril Demarche (IMJ-PRG)
Le théorème de dualité d’Artin-Mazur-Milne et quelques applications

Plus d'infos...

Lieu : salle 3L15 bâtiment 307

Résumé : Le théorème de dualité globale pour la cohomologie fppf des schémas en groupes finis et plats sur un ouvert d’une courbe sur un corps fini (ou du spectre de l’anneau des entiers d’un corps de nombres) est dû à Artin et Mazur. Il est notamment important pour la compréhension de la cohomologie fppf des schémas en groupes finis sur les corps globaux, et il possède de nombreuses applications arithmétiques. Le théorème est démontré par Milne dans son livre sur les théorèmes de dualité arithmétique, mais cette preuve est incomplète sur plusieurs points. Nous proposons, dans un travail en commun avec David Harari, une preuve détaillée de ce théorème, assortie de quelques compléments. Si le temps le permet, on évoquera quelques applications au principe de Hasse et à l’approximation faible pour les espaces homogènes de groupes algébriques sur un corps global.

Le théorème de dualité d’Artin-Mazur-Milne et quelques applications  Version PDF