Mathematics Research Beyond the Blackboard
LMS Computer Science Colloquium
Tuesday 29th October 2013 - De Morgan House, 57-58 Russell Square, WC1B 4HS (Nearest tube - Russell Square)
In recent years computer science has made a variety of contributions to the way mathematics research is done. These range from formal proofs of results too complex for humans to do by hand, such as the Kepler conjecture, to sophisticated computational tools such as chebfun for analysis and GAP for algebra and combinatorics, and even the use of social media to "crowdsource" proofs. The colloquium presents introductory talks, aimed at the level of interested graduate students or postdocs, for those who want to know more about these new ways of doing mathematics research, with ample scope for questions and discussion.
11:00 – 12:00 John Harrison (Intel Corporation)
Computer proofs, where we are and where we are going
The capacity of computers to construct and check formal proofs has grown from an esoteric research interest to be now both a practical industrial tool, and a real contributor to mathematics research, with the work by Hales on using computer proof in his proof of the Kepler Conjecture. In this talk we give an overview of present achievements and future directions.
12:00 – 13:00 Nick Trefethen (University of Oxford)
Numerical computation with functions instead of numbers
Symbolic computation with functions of a real variable suffers from combinatorial explosion of memory and computation time. An alternative idea is a kind of floating-point arithmetic in which the rounding operations are applied to Chebyshev representations of functions rather than to individual numbers. These ideas have been realized in the Chebfun software system.
13:00 – 14:00 - LUNCH
14:00 – 15:00 Ursula Martin (Queen Mary, University of London)
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 through experiments such as Gowers' polymath 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 an 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.
15:00 – 16:00 Steve Linton (University of St Andrews)
Experiment and Exploration in Algebra and Combinatorics
In this talk Professor Linton will briefly introduce the GAP (Groups, Algorithms, Programming) system for computing in discrete algebra and combinatorics, and some of its more important extension packages, and then describe my approach to using it in research. Computationally, this approach features the incremental development of small extensions to the system until it is capable enough to explore your area of interest interactively -- a middle ground between purely interactive "desk calculator" use of the existing capabilities of the system and the traditional "write a program and run it" model of scientific computing. Mathematically, the key idea is "undirected exploration". Once you acquire the capability to compute with a new type of mathematical structure, the first thing to do is often to set the computer to creating examples at random and listing their properties. As the output scrolls past, the stream of evidence and counterexamples helps you quickly narrow down to a set of conjectures that is worth investigating.
While this can, of course, be done by hand, the power of computers to create and analyse many non-trivial examples quickly makes it both faster and more rewarding.
Limited funds are available to help with students’ travel costs. Further details are available from Duncan Turton at the Society.
Submitted by Donald Eastwood on