Learning to do Math with Vampires and Spiders
The Project
This project aims to enhance the capabilities of the fully automated theorem prover, Vampire, by integrating specific mathematical constructs such as infinite series and transcendental functions into its reasoning routines. This work seeks to improve Vampire's performance on standard mathematics through innovative machine learning approaches and the development of strategy portfolios tailored to specific mathematical theories. The project will also establish a web service to facilitate the use of automatic theorem provers and create open datasets to support global automatic theorem proving efforts.
The Team
Andrei Voronkov was crazy about proving theorems from the age of 7 and equally crazy about writing computer programs from the age of 15, when he first got his hands on a punchcard. It is not surprising that his first non-toy computer program was a program for proving theorems.
His passion for computer theorem proving resulted in the design and initial development of the theorem prover Vampire, which won 70 world championship titles in first-order theorem proving since 1999.
He made contributions to many areas of automated reasoning, including theory, implementation techniques, and applications. He developed the first ever machine-learning based strategy scheduler Spider for Vampire in 2007. In his spare time he also developed the conference management system EasyChair used by over 4 million researchers.
He thinks that the world will be a better place to live when working mathematicians and computer programs teach each other how to do math and learn from each other. He believes that recently developed techniques in automated reasoning, such as theory reasoning and induction, can lead us to a revolution in computer-assisted math in the next 20 to 50 years.
Michael Rawson thinks that computers ought to be able to reason and learn from their past experiences. He is particularly interested in automated theorem proving: computer systems that make watertight logical arguments. He is one of the Antique Vampires: the team overlooking and directing the design and development of the world leading theorem prover Vampire.