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.
Mohammad Abdulaziz is a lecturer (equiv. to assistant professor) at the Department of Informatics at King's College London. Before that, he was a postdoctoral researcher at the Chair for Logic and Verification at Technische Universität München until 2022. He was awarded his PhD from the Australian National University in 2018. Mohammad’s research is in two areas: applications of theorem proving to formal verification, and to the formalisation of mathematics; and designing algorithms for AI planning. His work on formalising mathematics includes formalisations in theoretical computer science, semantics of planning languages, and multi-variate calculus. He also designed new AI planning algorithms, and verified AI planning software covering a large number of for settings ranging from simple, deterministic, finite systems to large, real-world stochastic systems.