## Lecture 8

## On Families of Filtered phi Modules and Crystalline Representations

We study families of filtered phi-modules associated to families of p-adic Galois representations as considered by Berger and Colmez. We show that the weakly admissible locus in a family of filtered phi-modules is open and that the groupoid of weakly admissible modules is in fact an Artin stack. Working in the category of adic spaces instead of the category of rigid analytic spaces one can show that there is an open substack of the weakly admissible locus over which the filtered phi-modules is induced from a family of crystalline representations.

## Introduction to the Coq Proof Assistant

A "proof assistant" is a software package comprising a validity checker for proofs in a particular logic, accompanied by semi-decision procedures called "tactics" that assist the mathematician in filling in the easy parts of the proofs. I will demonstrate the use of the Coq proof assistant in doing simple proofs about inductive structures such as natural numbers, sequences, and trees.

## Entropy, Algebraic Integers and Moduli of Surfaces

## Nonlinear Dvoretzky Theory

The classical Dvoretzky theorem asserts that for every integer k>1 and every target distortion D>1 there exists an integer n=n(k,D) such that any

## Shimura Varieties and the Bernstein Center

## INTRODUCTION TO THE UNIVALENT FOUNDATIONS OF MATHEMATICS

## Constructive Type Theory and Homotopy

In recent research it has become clear that there are fascinating connections between constructive mathematics, especially as formulated in the type theory of Martin-Löf, and homotopy theory, especially in the modern treatment in terms of Quillen model categories and higher-dimensional categories. This talk will survey some of these developments.

## Localization and Thermalization in Highly-Excited Many-Body Quantum Systems

**ANALYSIS/MATHEMATICAL PHYSICS SEMINAR**