Kick-off afternoon

The trimester will begin with a kick-off afternoon on April 22, intended for a large audience of mathematicians and computer scientists. It will consist of 4 talks:

• Georges Gonthier (Microsoft Research, Cambridge, and Microsoft INRIA Joint Center, Palaiseau): Digitizing the Group Theory of the Odd Order Theorem
• Thomas Hales (University of Pittsburgh): Formalizing the proof of the Kepler Conjecture
• Xavier Leroy (INRIA Paris-Rocquencourt): Proof assistants in computer science research
• Vladimir Voevodsky (Institute for Advanced Study, Princeton): Univalent Foundations - new type-theoretic foundations of mathematics