To Create a Semantic Search Engine for Mathematical Literature

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.

Who's involved


There's still time to register to attend the CCIMI Connecting with Industry Day tomorrow, starting at 12:45pm (GMT)… View on Twitter