Skip to content
Research Fellows Directory

Paulo Oliva

Dr Paulo Oliva PhD

Research Fellow

Organisation

Queen Mary, University of London

Research summary

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

Mathematics.

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.

Grants awarded

Selection functions in proof theory

Scheme: University Research Fellowship

Dates: Oct 2011 - Sep 2014

Value: £262,387.74

Functional interpretations and the nature of computing

Scheme: University Research Fellowship

Dates: Oct 2006 - Sep 2011

Value: £394,464.80