ABSTRACT. ALEXANDRIA is an ERC-funded 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.

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 sequence-based 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 well-established 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.

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, easy-to-generalize ML models.

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 cross-site data mining on huge databases, and building on existing Isabelle-verified 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 Isabelle-verified event structure enumeration algorithms into a fully verified framework to link event structures to full graphs.

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 ground-truth dataset collected with the help of domain experts. We find that for the majority of lints, there is a significant but low-strength correlation between frequency of occurrence and churn in maintenance change-sets. 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 lint-prone 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 ground-truth dataset of 35 good and problematic theories each, our pre-defined 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 lint-proneness even achieves perfect accuracy at 43%, providing additional evidence of its effectiveness.

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 Nielsen-Schreier 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 Nielsen-Schreier 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 Nielsen-Schreier 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.

ABSTRACT. We show how to “automatically” prove results about sequences in the On-Line Encyclopedia of Integer Sequences (OEIS) using a free software tool called Walnut, and illustrate it with a number of examples chosen from the OEIS.

ABSTRACT. The nominal syntax is an extension of the first-order syntax that smoothly represents languages with variable bindings. Nominal matching is first-order matching modulo alpha-equivalence. This work extends a certified first-order AC-unification algorithm to solve nominal AC-matching problems. To our knowledge, this is the first mechanically-verified nominal AC-matching algorithm. Its soundness and completeness were verified using the proof assistant PVS. The formalisation enriches the first-order AC-unification 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 AC-equality checker as a byproduct.

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.

ABSTRACT. In this paper we present an experimental version of the Mizar proof checker equipped with new built-in 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.

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 expert-designed interfaces for use in mathematical knowledge management settings.

ABSTRACT. Abstract algebra provides a large hierarchy of properties that a collection of objects can satisfy, such as forming an abelian group or a semiring. These classifications can arranged into a broad and typically acyclic directed graph. This graph perspective encodes naturally in the typeclass system of theorem provers such as Lean, where each can be represented as structures (or records) containing the requisite axioms. This design inevitably needs some form of multiple inheritance; a ring is both a semiring and an abelian group.

In the presence of dependently-typed typeclasses that themselves consume typeclasses, such a vector space typeclass which assumes the presence of an existing additive structure, the implementation details of structure multiple inheritance matter. The type of the applied outer typeclass is influenced by the path taken to resolve the typeclasses it consumes. Unless these paths are all considered judgmentally equal, this is a recipe for disaster.

This paper provide a concrete explanation of how these situations arise (reduced from real examples in mathlib), compares implementation approaches for multiple inheritance by whether judgmental equality is preserved, and outlines solutions to the problems discovered.