Title: Managing Sparsity in Formal Mathematics with User Tags and Network Models
Speaker: James Vaughan
Abstract:

Proof assistants are used for interactive development and verification of mathematical proofs with the assistance of automated tools. These proofs are highly modular and are frequently reused, but the quantity that are available makes it difficult to find those that are relevant during interactive proofs. In this presentation, I will discuss how we use network science to understand the structure of the dependency network that emerges between proofs in the Isabelle proof assistant. In particular, we use stochastic block models and side-information in the form of user tags to combat the sparsity of the network and improve the prediction of new dependencies. In so doing we aim to improve the level of automation in Isabelle, thereby enabling the user to tackle more complex proofs.