Events

10:00am Henk Barendregt (Radboud University, Nijmegen)
Progress in Computer MathematicsProgress in the foundations of mathematics has made it possible to formulate all thinkable mathematical concepts, algorithms and proofs in one language and in an impeccable way. This not in spite of, but partially based on the famous results of Gödel and Turing. In this way statements are about mathematical objects andalgorithms, proofs show the correctness of statements and computations, and computations are dealing with objects and proofs. Interactive computer systems for a full integration of defining, computing and proving are based on this. The human defines concepts, constructs algorithms and provides proofs, while the machine checks that the definitions are well-formed and the proofs and computations are correct. Results formalized so far demonstrate the feasibility of computer mathematics. There are very good applications. The challenge is to make the systems more mathematician-friendly, by building libraries and tools. The eventual goal is to help humans to learn, develop, communicate, referee and apply mathematics.

Henk Barendregt did in 1971 his PhD in mathematical logic at Utrecht University with Georg Kreisel and Dirk van Dalen on topics in lambda calculus. Currently he is professor of Foundations of mathematics and computer science at Radboud University Nijmegen. He is member of Academia Europaea and the Royal Dutch Academy of Sciences. In 2002 he was awarded the Spinoza prize, the highest scientific distinction in the Netherlands.

11:00am Georges Gonthier (MSR Cambridge)
From proof by computation to computing proofs: reflection in action

In the context of mechanical theorem proving, reflection means using theorems about symbolic representations. Despite its trivial logical underpinnings, the generalised use of reflection has a deep impact on the practice of computer proofs. Proof scripts, while not readable in the traditional sense, become more stylised and organised. Paradoxically, while the average size of individual proofs grows sharply, the global size of theories shrinks considerably. We will describe the design principles of the scritpting language that supports this new style of proof, and illustrate its use through examples drawn from the Four Colour Theorem and the PoplMark benchmark.

Georges Gonthier received his Doctorat in 1988 from Université Paris XI for work on the Esterel reactive programming language. After two years at AT&T Bell Labs, he returned to France at Inria in 1990. His work includes the optimal computation of functional programs, the formal verification of a concurrent memory management algorithm, and concurrency analysis of the Ariane 5 flight software. Dr. Gonthier joined Microsoft Research Cambridge in 2003, where he completed the first fully computer-checked proof of the famous Four Colour Theorem.

11:45am Coffee break,

12:00am Sean McLaughlin (Carnegie-Mellon University)
The Mathematics of the Kepler Conjecture

The Flyspeck project is an attempt to formalize a recent proof of the Kepler Conjecture. Unlike other major results such as Fermat’s Last Theorem or the Classification of Finite Simple Groups, Hales’ proof of the Kepler Conjecture requires comparatively little mathematical infrastructure. The proof is also highly computational in nature. This makes it a particularly attractive target for formalization by computer. In this talk I’ll give an overview of the essential theorems and algorithms used in the Kepler Conjecture.

Sean McLaughlin is a graduate student in computer science at Carnegie Mellon University. His interests include proof assistants, automated theorem proving and programming languages. As an undergraduate, he worked closely with Tom Hales on a related sphere packing problem while Hales was completing his proof of the Kepler Conjecture. Sean is presently an intern of Georges Gonthier at the joint Inria-MSR lab.