[TYPES/announce] A talk by Tim Gowers at IHP, May 26, 5 pm

[Pierre-Louis Curien]

We are glad to announce that, as part of the IHP trimester

Semantics of proofs and certified mathematics,

there will be a talk by 

Timothy Gowers (Cambridge University)

on May 26, 5 pm, Amphithéâtre Hermite (IHP, 11 rue P. et M. Curie)

Title: Fully automatic problem solving with human-style output.

Abstract: I shall describe a program that Mohan Ganesalingam and I created that proves simple statements in elementary abstract analysis. I shall also discuss the broader project of which this is intended to be just a preliminary step. Briefly, the aim is to write a series of programs that solve problems in a "fully human" way, meaning that they do not undertake any search that a human mathematician would not consider undertaking. At first, this seems to be sacrificing everything that makes a computer worth using. However, I shall attempt to explain why we regard this view as mistaken.

The organisers:  Pierre-Louis Curien, Hugo Herbelin, Paul-André Melliès