Séminaire N. Bourbaki

Samedi 21 juin 2014

Le Séminaire a lieu à l'Institut Henri Poincaré (amphithéâtre Hermite), 11 rue Pierre et Marie Curie, Paris 5^e.

Liens vers l'affiche et les résumés (PDF)

10h00

Alain VALETTE — Le problème de Kadison-Singer [PDF] [YouTube]
En 1959, R.V. Kadison et I.M. Singer demandaient si tout état pur de l'algèbre des matrices diagonales sur $\ell^2$, s'étend en un unique état pur sur $B(\ell^2)$. La solution affirmative a été obtenue en juin 2013 par A. Marcus, S. Spielman et N. Srivastava, suite à des traductions du problème en algèbre linéaire dues à J. Anderson, C. Akemann, N. Weaver,... Les résultats principaux concernent le plus grand zéro de l'espérance du polynôme caractéristique d'une somme de variables aléatoires indépendantes, à valeurs dans les matrices positives de rang 1.

11h30

Jacques SMULEVICI — La conjecture de courbure $L^2$ [d'après S. Klainerman, I. Rodnianski et J. Szeftel] [PDF] [YouTube]
La relativité générale est l'un des piliers de la physique théorique moderne. Mathématiquement, il s'agit de l'étude des variétés lorentziennes satisfaisant aux équations d'Einstein, un système d'équations aux dérivées partielles déterminant l'évolution de la géométrie de la variété. La « conjecture de courbure $L^2$ », proposée par Klainerman en 1999, affirme que le problème aux données initiales est bien posé dans la classe des métriques telles que le tenseur de courbure est localement dans $L^2$. Après une brève introduction à  l'étude des équations d'Einstein, nous présenterons les travaux récents de Klainerman, Rodnianski et Szeftel démontrant cette conjecture. Ce résultat fondamental est le point d'orgue d'une longue série de travaux dédiés aux équations d'ondes quasi-linéaires à faible régularité.

14h30

Thomas C. HALES — Developments in formal proofs [PDF] [YouTube]
A formal proof is a proof that can be read and verified by computer, directly from the fundamental rules of logic and the foundational axioms of mathematics. The technology behind formal proofs has been under development for decades and grew out of efforts in the early twentieth century to place mathematics on secure foundations. In recent years, this technology has made remarkable advances. Notably, a project led by Georges Gonthier has produced a complete formal verification of the odd-order theorem of Feit and Thompson. This presentation will describe major recent developments in this field.

16h00

Thierry COQUAND — Théorie des types dépendants et axiome d'univalence [PDF] [YouTube]
Cet exposé sera une introduction à la théorie des types dépendants et à l'axiome d'univalence. Cette théorie est une alternative à la théorie  des ensembles comme fondement des mathématiques. Guidé par une interprétation d'un type comme un espace topologique « à  homotopie près » (type d'homotopie), V. Voevoedsky a introduit une stratification des types suivant la complexité  de leur égalité, qui fait apparaître la théorie  des types comme une généralisation de la théorie des ensembles. Il a aussi formulé l'axiome d'univalence qui est une forme très forte du principe d'extensionalité. On discutera en particulier de quelques conséquences de cet axiome pour la représentation formelle de la notion de catégorie.

Sessions antérieures :

Session de mars 2014

Sessions ultérieures

Session de novembre 2014

Brochure

Des brochures contenant les quatre exposés de ce Séminaire seront distribués au début de chaque séance ; 300 exemplaires seront disponibles au cours de cette session.

Pour recevoir à l'avance le programme et les résumés de chaque séminaire, veuillez vous abonner en envoyant un mail à sympa@lists.ens.fr, en indiquant :
subscribe bourbaki-public <Prénom> <Nom>
<Prénom> et <Nom> devant, bien entendu, être remplacés par vos prénom et nom.

Remerciements

Une subvention du CNRS couvre une partie des frais d'organisation de ce Séminaire.