Learning to do Math with Vampires and Spiders
The Project
This project harnesses the power of large language models (LLMs) to facilitate translation of statements and proofs between different interactive theorem provers (ITPs), such as Lean and the Rocq Prover, as well as between different versions of the same prover, e.g., Lean 3 vs Lean 4. By enabling the conversion of proofs and libraries across these platforms, the initiative aims to create a unified library of formalized knowledge, enhancing collaboration and resource sharing within the formal methods community. This effort would not only bridge significant resources like MathLib and Mathematical Components but would also support smoother transitions during future major updates, e.g., Lean 5.
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.