TheoryMine

TheoryMine was a company dedicated to automated theory exploration: it developed artificial intelligence techniques to discover new mathematical concepts and automate proof.

By providing a fun application of theorem proving - naming new theorems as a novelty gift - it aimed to sponsor more serious applications of automated reasoning technology, such as verification tools to make software more reliable and safe to use, and tools to ease the exploration of new mathematical concepts.

TheoryMine was started in 2009 and operated until the end of 2019. After 10 years the founders decided to close the company and give the (sadly not very large) profits to charity (codeyourfuture.io) and open-source the code.

On this site, we'll be adding links to the software and adding a little more description of the project and some of the crazier ideas we had but never really had time to do.

Whether you named a theorem from TheoryMine or not, we wish you happy mathematical discoveries, and hope you enjoyed the robotic discoveries, or at least the concept of it.

Who developed TheoryMine?

The founders were a group of researchers in the School of Informatics at University of Edinburgh:

Alan Bundy - was Managing Director of TheoryMine and Professor of Automated Reasoning in the School of Informatics, University of Edinburgh, CBE, FRS, FREng, FACM.

Flaminia Cavallo - graduated in Artificial Intelligence and Mathematics from the University of Edinburgh.

Lucas Dixon - was CTO of TheoryMine and a senior researcher at, and former PhD graduate of, the Mathematical Reasoning Group at the University of Edinburgh. Lucas is now a research scientist at Google.

Moa Johansson - did her PhD in the Mathematical Reasoning Group at the University of Edinburgh, and then became Assistant professor at Chalmers University of Technology in Gothenburg, Sweden.

The Software

The software built on decades of research by the international community in automated reasoning, notably in interactive theorem proving and automated deduction. We'll be uploading the source code in a little while, and adding links to it here.