Copilots for Isabelle
Learning Logical Structure for a Better Proving Experience
The Project
Isabelle is one of the most popular proof assistants which has hosted landmark verification results in both mathematics and computer science. As a team that puts together experienced Isabelle designers, developers and users with AI experts, we will extend the system with intelligent copilots that will take advantage of the substantial amount of highly structured information that is acquired through human interaction. Isabelle will “pay more attention” to data coming from its highly intelligent users and developers and will herself become more intelligent. This will lead to the formulation of new AI problems relevant for theorem proving beyond Isabelle.
The Team
Andrei Popescu is a senior lecturer (associate professor) in computer science at the University of Sheffield. Previously, he worked as a Lecturer at Middlesex University and as a postdoctoral researcher at TU Munich. He has a PhD in computer science from the University of Illinois at Urbana-Champaign and one in mathematics from the University of Bucharest. He is an enthusiastic seeker of ever better logical foundations and specification mechanisms for proof assistants, and much of his work informs the development of inductive and coinductive reasoning infrastructure for a wonderful proof assistant called Isabelle/HOL. He is also involved in formal verification developments using Isabelle, ranging from fundamentals such as Gödel’s incompleteness theorems to applied information flow security.
Dmitriy Traytel is an associate professor at the University of Copenhagen, Department of Computer Science (DIKU). He completed his PhD at TU München in 2015 under Tobias Nipkow’s supervision and has been a postdoctoral researcher in David Basin’s group at ETH Zürich until 2020. Dmitriy is both a user and a developer of the Isabelle proof assistant and serves as an editor for Isabelle’s Archive of Formal Proofs. As a user, Dmitriy’s current focus is the verification of scalable data stream processing algorithms. As a developer, Dmitriy has been a major contributor to the design and implementation of Isabelle’s modular inductive and coinductive datatypes (including binding-aware variants) along with the accompanying definitional and reasoning infrastructure.
Jan Jakubův is a senior researcher at CIIRC, Czech Technical University in Prague, with expertise in automated reasoning and formal verification. He received his PhD from Heriot-Watt University, where he studied process calculi and type systems. His recent work emphasizes machine learning techniques for theorem proving, and he is the principal developer of ENIGMA.