View: session overviewtalk overview
09:00  LargeScale Formal Proof for the Working Mathematician – Lessons Learnt from the ALEXANDRIA Project ABSTRACT. ALEXANDRIA is an ERCfunded project that started in 2017, with the aim of bringing formal verification to mathematics. The past six years have seen great strides in the formalisation of mathematics and also in some relevant technologies, above all machine learning. Six years of intensive formalisation activity seem to show that even the most advanced results, drawing on multiple fields of mathematics, can be formalised using the tools available today.

10:00  CoProver: A Recommender System for Proof Construction PRESENTER: Natarajan Shankar ABSTRACT. Interactive Theorem Provers (ITPs) are an indispensable tool in the arsenal of formal method experts as a platform for construction and (formal) verification of proofs. The complexity of the proofs in conjunction with the level of expertise typically required for the process to succeed can often hinder the adoption of ITPs. A recent strain of work has investigated methods to incorporate machine learning models trained on ITP user activity traces as a viable path towards full automation. While a valuable line of investigation, many problems still require human supervision to be completed fully, thus applying learning methods to assist the user with useful recommendations can prove more fruitful. Following the vein of user assistance, we introduce CoProver, a proof recommender system based on transformers, capable of learning from past actions during proof construction, all while exploring knowledge stored in the ITP concerning previous proofs. CoProver employs a neurally learnt sequencebased encoding of sequents, capturing long distance relationships between terms and hidden cues therein. We couple CoProver with the Prototype Verification System (PVS) and evaluate its performance on two key areas, namely: (1) Next Proof Action Recommendation, and (2) Relevant Lemma Retrieval given a library of theories. We first describe PVS and its key differences with other frameworks that make full automation difficult. We evaluate CoProver on a series of wellestablished metrics originating from the recommender system and information retrieval communities, respectively. We show that CoProver successfully outperforms prior state of the art applied to recommendation in the context of PVS and detail some initial observations about these recommendations from experienced users. We conclude by discussing future directions viable for CoProver (and similar approaches) such as argument prediction, proof summarization, and more. 
10:30  An Augmented MetiTarski Dataset for Real Quantifier Elimination using Machine Learning PRESENTER: Grant Passmore ABSTRACT. In this paper, we contribute a new dataset composed of more than 41K MetiTarski challenges that can be used to investigate applications of machine learning (ML) in determining efficient variable ordering. The proposed dataset aims to address inadvertent bias issues present in prior benchmarks, paving the way to development of robust, easytogeneralize ML models. 
11:30  Isabelle Formalisation of Original Representation Theorems ABSTRACT. In a recent paper, new theorems linking apparently unrelated mathematical objects (event structures from concurrency theory and full graphs arising in computational biology) were discovered by crosssite data mining on huge databases, and building on existing Isabelleverified event structures enumeration algorithms. Given the origin and newness of such theorems, their formal certification is particularly desirable. This paper presents such a certification via Isabelle/HOL definitions and theorems, and exposes the technical challenges found in the process. The introduced formalisation completes the certification of Isabelleverified event structure enumeration algorithms into a fully verified framework to link event structures to full graphs. 
12:00  Formalization Quality in Isabelle PRESENTER: Fabian Huch ABSTRACT. Little is known about the quality of formalizations in interactive theorem proving. In this work, we analyze the relationship between static analysis warnings (lints) and maintenance effort for 6470 Isabelle theories, create models to predict lints based on structural features, and compare the results to a small groundtruth dataset collected with the help of domain experts. We find that for the majority of lints, there is a significant but lowstrength correlation between frequency of occurrence and churn in maintenance changesets. In particular, for proofs using tactic methods (which can be brittle), the Spearman correlation is highest with a strength of 0.16, p<0.005. Furthermore, when classifying theories as lintprone based on their formal entity graphs (which capture the dependencies between underlying logical entities), random forests outperform even deep learning models on our data, achieving 58% precision and 21% recall. Finally, in our groundtruth dataset of 35 good and problematic theories each, our predefined criterion that identifies theories with more than one lint every 100 lines achieves 95% precision and 51% recall. Surprisingly, this is very close to the optimal criterion of one lint every 109 lines (54% recall at the 95% precision). Moreover, the random forest model trained for lintproneness even achieves perfect accuracy at 43%, providing additional evidence of its effectiveness. 
12:30  Formalizing Free Groups in Isabelle/HOL: The Nielsen Schreier Theorem and the Conjugacy Problem PRESENTER: T.V.H. Prathamesh ABSTRACT. Free groups are central to group theory, and are ubiquitous across many branches of mathematics, including algebra, topology and geometry. An important result in the theory of free groups is the NielsenSchreier Theorem, which states that any subgroup of a free group is free. In this paper, we present a formalisation, in Isabelle/HOL, of a combinatorial proof of the NielsenSchreier theorem. In particular, our formalisation applies to arbitrary subgroups of free groups, without any restriction on the index of the subgroup or the cardinality of its generating sets. We also present a formalisation of an algorithm which determines whether two group words represent conjugate elements in a free group. To the best of our knowledge, this is the first formalisation, in any proof assistant, of the NielsenSchreier theorem in its full generality. In addition, to the best of our knowledge, this is the first formalisation, in any proof assistant, of a decision procedure for the conjugacy problem in free groups. 
14:00  Proving Results About OEIS Sequences with Walnut ABSTRACT. We show how to “automatically” prove results about sequences in the OnLine Encyclopedia of Integer Sequences (OEIS) using a free software tool called Walnut, and illustrate it with a number of examples chosen from the OEIS. 
14:30  Nominal ACMatching (Best Paper) PRESENTER: Daniele NantesSobrinho ABSTRACT. The nominal syntax is an extension of the firstorder syntax that smoothly represents languages with variable bindings. Nominal matching is firstorder matching modulo alphaequivalence. This work extends a certified firstorder ACunification algorithm to solve nominal ACmatching problems. To our knowledge, this is the first mechanicallyverified nominal ACmatching algorithm. Its soundness and completeness were verified using the proof assistant PVS. The formalisation enriches the firstorder ACunification algorithm providing structures and mechanisms to deal with the combinatorial aspects of nominal atoms, permutations and abstractions. Furthermore, by adding a parameter for “protected variables” that cannot be instantiated during the execution, it enables nominal matching. Such a general treatment of protected variables also gives rise to a verified nominal ACequality checker as a byproduct. 
15:00  True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers PRESENTER: Simone Heisinger ABSTRACT. As the application of quantified Boolean formulas (QBF) continues to expand in various scientific and industrial domains, the development of efficient QBF solvers and their underlying proving strategies is of growing importance. To understand and to compare different solving approaches, techniques of proof complexity are applied. To this end, formula families have been crafted that exhibit certain properties of proof systems. These formulas are valuable to test and compare specific solver implementations. Current approaches consider false formulas only. In this work, we propose to consider true formulas as well in order to obtain challenging benchmarks. Therefore, we modified two popular formula families in such a way that (1) the formulas become true, (2) interesting structural properties are preserved, and (3) the formulas are in prenex conjunctive normal form. 
15:20  Extending Numeric Automation for Number Theory Formalizations in Mizar ABSTRACT. In this paper we present an experimental version of the Mizar proof checker equipped with new builtin routines for automating common numeric computations. This implementation has been directly motivated by recent formalizations of selected number theory topics that required extensive numeric calculations and proving numerical properties of specific numbers. The potential of automating parts of such proofs has been evaluated and, consequently, the Mizar checker has been extended with code that enabled refactoring the current contents of the Mizar Mathematical Library. 
15:40  Extracting Theory Graphs from the Aldor Library PRESENTER: Florian Rabe ABSTRACT. Aldor is a programming language for computer algebra that allows natural expression of algebraic objects while also allowing compilation to efficient code. Its language primitives, however, do not correspond exactly to those of modern proof assistants nor to those of data formats used in mathematical knowledge management. We discuss these difficulties and export the Aldor library as a theory graph, using a simplified model of the Aldor language that retains its essential expressivity. This allows us to capture a rich set of expertdesigned interfaces for use in mathematical knowledge management settings. 
The open session is an opportunity for people to show their system developments on their laptops. In this session, people could also present other things, such as preliminary work, research proposals, offers of collaboration ...