Often when one wants to find out whether a mathematical definition or statement is already known, searching for it in the literature is a haphazard process because one does not know the name of what one is searching for. This project is to develop a system that will search for the concepts themselves. The first goal would be a system that can search the literature once that literature has been appropriately tagged. One of the challenges will be to give the system enough theorem-proving ability to recognise when two formulations of a theorem are obviously equivalent: this will involve a certain amount of automatic theorem proving. A more ambitious long-term goal would be to create a system that can trawl through the literature on its own and do the tagging for itself.
Professor Gowers is not currently accepting students in this area.