Invited Talks

Ursula Martin

Mathematical practice, crowdsourcing, and social machines.

For centuries, the highest level of mathematics has been seen as an isolated creative activity, to produce a proof for review and acceptance by research peers. Mathematics is now at a remarkable inflexion point, with new technology radically extending the power and limits of individuals. Crowdsourcing pulls together diverse experts to solve problems; symbolic computation tackles huge routine calculations; and computers, using programs designed to verify hardware, check proofs that are just too long and complicated for any human to comprehend.

Mathematical practice is am emerging interdisciplinary field which draws on philosophy, social science and ethnography, and the input of mathematicians themselves, to understand how mathematics is produced. Online mathematical activity provides a rich source of data for empirical investigation of mathematical practice - for example the community question answering system mathoverflow contains around 40,000 mathematical conversations, and polymath collaborations provide transcripts of the process of discovering proofs. Such investigations show the importance of "soft" aspects such as analogy and creativity, alongside formal deduction, in the production of mathematics, and give us new ways to think about the possible complementary roles of people and machines in creating new mathematical knowledge

Social machines are new paradigm, identified by Berners-Lee, for viewing a combination of people and computers as a single problem-solving entity, and the subject of major international research endeavours. We outline a research agenda for mathematics social machines, a combination of people, computers, and mathematical archives to create and apply mathematics, with the potential to change the way people do mathematics, and to transform the reach, pace, and impact of mathematics research.

Assia Mahboubi

A Machine-checked Proof of the Odd Order Theorem

The Odd Order Theorem due to Feit and Thompson is a major result of finite group theory which is a cornerstone of the classification of finite simple groups. Originally published in 1963, this was considered at its time as a demonstration of an uncommon length and intricacy, whose 255 pages filled an entire volume of the Pacific Journal of Mathematics. Later simplified and improved by a collective revision effort, it remains a long and difficult proof, combining a broad panel of algebraic theories. In September 2012, the Mathematical Components team, lead by Georges Gonthier, completed a formalization of this result using the Coq proof assistant. In this talk we will comment on the techniques and methodologies that emerged from this six year collaborative work and on the perspectives it opens on the use of a computer to do mathematics.

Patrick Ion

Mathematics and the World Wide Web.

Mathematics is an ancient and honorable study. It's been called The Queen and The Language of Science. The World Wide Web is something brand-new that started only about a quarter of a century ago. But the World Wide Web is having a considerable effect on the practice of mathematics, is modifying its image and role in society, and can be said to have changed some of its content. There are forces at work in the web that may be changing our world not necessarily for the better. I'll be exploring some of the issues this raises.