Queen Mary, University of London
My research area is in mathematical logic, or, more precisely, the logical structure of proofs in mathematics. I study proofs in Mathematics because proofs are very similar to computer programs (as in Computer Science). Just as complex computer systems are normally built in a modular fashion, out of smaller subcomponents; so are complex proofs in mathematics. When proving a new theorem, a mathematician is allowed to freely use other theorems already proven
by other mathematicians, just like software engineers are encouraged to reuse computer code, and build systems using standard libraries. From this perspective,
Mathematics can be thought of as a big open source project, very similar to the project that led to the development of the Linux operating system.
The problem is that Mathematics is a different form of programming language, which is not directly comprehensible to a standard computer. And moreover, it is
not an easy task to tell what a given proof in Mathematics will turn out to be once you convert it into a computer program. In order to be able to understand what a
proof does, and ultimately to “run” it just like to we with everyday computer software, we need a translator from the language of Mathematics to the language
of computers. I work both on such translation mechanisms but also on the particular meaning of the programs one obtains from some standard proof in
The impact of my research lies on the potential to turn complex and clever proofs in Mathematics into sophisticated computer programs that we might not be able to come up with, or build, directly. We have some concrete examples of this. For instance, a 50-year old proof in approximation theory has been shown to solve an
algorithmic task no one had been able to solve otherwise. In this particular case, the proof had hidden in its logical structure a computational procedure to
approximate any continuous function by a polynomial.