SICSA mcp day

We would like to invite you to apply to participate in a maths and computer proof discussion day. The goal of the event is to bring together a small number of leading mathematicians, and experts in computer proof, for a day of informal discussion, to consider the broad question of how present and future research efforts in computer proof can best serve mathematical advance. The idea is to think "big picture" thoughts about the future of mathematics, and the possible role of formal proof within it, rather than to discuss technical questions - expertise in computer proof is not required.

Participants so far include Dr Georges Gonthier of Microsoft Research, who has produced a formal proof of the four colour theorem, and is well advanced on a formal proof of the odd-order theorem; Dr John Harrison of Intel, who works on formalising mathematics needed to ensure correctness of hardware; and mathematicians Dr Tara Brendle (Glasgow), Sir Michael Atiyah (Edinburgh); Professor Andrew Ranicki (Edinburgh), and Professor Geoff Robinson (Aberdeen). The event is chaired by Professor Ursula Martin CBE (QMUL/Edinburgh).

The day will run from 10am - 5pm on 15th April, in the Informatics Forum, and lunch and refreshments will be provided. In the evening of 15th April you are invited to join members and visitors at a reception celebrating 25 years of Edinburgh's Laboratory for Foundations of Computer Science. Funding is being provided by SICSA.

The event is co-located with the Milner Symposium, celebrating the life and work of computer scientist and Turing Award winner Robin Milner.

This is a small focussed workshop, and the number of places is strictly limited. A small number of places are available to researchers in SICSA universities. To apply to attend, please send the following information to Magdalena Mazurczak level4admin@inf.ed.ac.uk BY 5PM ON MONDAY 19TH MARCH. You will be notified a few days later. We need to know your name, your department, your status (PhD student, RA etc), and a statement of up to 100 words explaining your reason for wanting to attend the event.

Over the past 25 years there have been remarkable developments in software that produces formal proofs, such as

• Gonthier's formal proof of the four colour theorem [1], and his plans for a formal proof of the classification of finite simple groups [2]
• Hales's work in progress on a formal proof of Kepler's conjecture [3]

The AMS devoted an issue of the Notices to these matters recently [4], and in 2005 the Royal Society held a discussion meeting [5] on "The nature of mathematical proof" bringing together many of the major actors. The development and use of such systems involves major and sustained efforts and commitment. This spans the mathematics underlying them (deep connections are emerging between the logic developed for these systems and other parts of mathematics); developing the software (the leading systems, for example Isabelle, have a 20 year history); and deploying it (Hales estimates his Kepler proof will take ten years). Thus, while there are already specialised meetings already devoted to these issues, the goal of this event is novel. Rather than concentrate on details of the technologies, we want to focus on how we can develop and use them to best advance mathematics, with input from leading mathematicians who are already shaping the discipline. We expect wide-ranging discussion, and do not wish to pre-judge the outcomes, but we might consider questions like:

• Are these technologies changing the nature of mathematical advance? Does mathematics need to respond to this, and if so how?
• How can the development of these systems best support mathematical advance?
• Should matters proceed organically (an approach which has, after all, served mathematics well throughout history) or should there be a more planned approach?
• What should the balance be between useful tools and attacks on major conjectures?
• Are there ways to make the burden of work more tractable and speed up progress?
• What's missing - are there some "quick-win" software tools that would be useful?
• How do we best inform mathematicians as to the power and limits of these systems?