About Us:

TheoryMine is a company dedicated to automated theory exploration: we develop artificial intelligence techniques to discover new mathematical concepts and automate proof. By providing some fun applications of theorem proving (e.g. naming new theorems!), we sponsor more serious applications of automated reasoning technology. In particular, we are working on verification tools to make software more reliable and safe to use, as well as tools to ease the exploration of new mathematical concepts

Our software builds on decades of research by the international community in automated reasoning, notably the work in interactive theorem proving as well as automated deduction. They provide amazing software which deserves to be more widely used and appreciated.

TheoryMine was started by a group of researchers in the School of Informatics at University of Edinburgh, we are:


Alan Bundy

Professor of Automated Reasoning at School of Informatics, University of Edinburgh and Vice President of the British Computing Society. Member of Centre for Intelligent Systems and their Applications.
Flaminia Cavallo

Graduated in Artificial Intelligence and Mathematics from the University of Edinburgh.
Lucas Dixon

Senior Researcher with the Mathematical Reasoning Group, part of the Centre for Intelligent Systems and their Applications, in the School of Informatics, at the University of Edinburgh. Lucas is the lead software developer for TheoryMine.

Moa Johansson

Currently a postdoc researcher in the Departement of Informatics at Universita degli Studi di Verona in Italy. She did her PhD in the Mathematical Reasoning Group at the University of Edinburgh.

Roy McCasland

Senior Research Fellow at the School of Informatics, University of Edinburgh and member of the Centre for Intelligent Systems and their Applications.