ABSTRACT. The Census of Cubic Vertex Transitive Graphs, by Potočnik, Spiga, and Verret, has recently been extended with additional data. We took this opportunity to make the new dataset as useful as possible according to current best practices and with the current technology. As part of this, we explore the best practices for research data in the mathematical community.

In this work, we describe the steps we took to make the data as FAIR and as machine actionable as possible. We also describe how we made the data searchable and easy to interact with through a web interface by publishing it on an instance of the platform MathDataHub.

ABSTRACT. In principle, dependent type theory should provide an ideal foundation for formalizing graded rings, where each grade can be of a different type. With such a powerful foundation comes a large number of choices for how to proceed with such a formalization. This paper explores various different approaches to how formalization could proceed, and then demonstrates precisely how graded algebras were formalized in Lean's {\mathlib}. Notably, we show how this formalization was used as an API; allowing us to formalize various types of graded structure such as those on tuples, free monoids, tensor algebras, and clifford algebras.

ABSTRACT. We report on using logic software in a novel course-format for an undergraduate logic course for students in computer science or artificial intelligence. Although being designed as the students' basic introduction to the field of logic, the course features a novel structure and it adds some modern content, such as SAT solving and SMT, to the traditional and established topics, such as propositional logic and first order predicate logic. The novel course design is characterized by, among others, the integration of existing logic software into the teaching of logic.

In this paper we focus on the module on first-order predicate logic (FO) and the use of the Theorema system as a proof-tutor for the students. We report on statistical evaluation of data collected over two consecutive years of teaching this course. On the one hand, we asked for feedback of students on how helpful they felt the software support was. On the other hand, we evaluated their results in the exams during the course and their development over the entire teaching period. The performance in exams is then correlated with students' own perception of the helpfulness of software.

ABSTRACT. The European Erasmus+ project ARC - Automated Reasoning in the Class aims at improving the academic education in disciplines related to Computational Logic by using Automated Reasoning tools. We present the technical aspects of the tools as well as our education experiments, which took place mostly in virtual lectures due to the COVID pandemics. Our education goals are: to support the virtual interaction between teacher and students in the absence of the blackboard, to explain the basic computational logic algorithms, to study their implementation in certain programming environments, to reveal the main relationships between logic and programming, and to develop the proof skills of the students. For the introductory lectures we use some programs in C and in Mathematica in order to illustrate normal forms, resolution, and DPLL with its Chaff version, as well as an implementation of sequent calculus in the Theorema system. Furthermore we developed special tools for SAT, some based on the original methods from the partners, including complex tools for SMT solving that allow the illustration of various solving approaches. An SMT related approach is natural-style proving in Elementary Analysis, for which we developed and interesting set of practical heuristics. For more advanced lectures on rewrite systems we use the Coq programming and proving environment, in order on one hand to demonstrate programming in functional style and on the other hand for proving properties of programs. Another advanced approach used in some lectures is the deduction based synthesis of algorithms and special programming transformation techniques.

ABSTRACT. A generalized set theory (GST) is like a standard set theory but also has non-set structured objects that can contain other struc- tured objects including arbitrary sets. This paper presents Isabelle/HOL support for GSTs, which are treated as type classes that combine fea- tures that specify kinds of mathematical objects: sets, ordered pairs, or- dinal numbers, natural numbers, functions, binary relations, etc. GSTs can have an exception feature that eases representing partial functions and undefinedness. When assembling a GST, extra axioms are generated following a user-modifiable policy to fill specification gaps. Specialized type-like predicates called soft types are used extensively. Although a GST can be used without a model, for confidence in its consistency we build a model from components that specify each feature’s contribution to each tier of a von-Neumann-style cumulative hierarchy defined via ordinal recursion. We use Isabelle/HOL type definitions and the Lifting and Transfer packages to connect a model of a GST built within type dᵢ to another type dⱼ which the GST occupies.

ABSTRACT. Formalization libraries for interactive theorem provers are rapidly growing in size, but only little is understood structurally about those developments. We aim to address the arising challenges by utilizing dependency graphs of the underlying formal entities. For the Isabelle Archive of Formal Proofs, the individual entry graphs consist of 1.8 million nodes and 28.3 million edges in total, and exhibit certain complex network characteristics: Node in-degrees weakly follow scale-free distributions with an average exponent of α = 1.81, and the high clustering coefficient (avg. 0.33) together with the short average path length (3.64) indicate small-world effects. We did not find network centrality metrics to be good indicators of theory quality (measured by lint frequency): The Spearman correlation of our six different centrality metrics was weaker than in similar experiments from software systems, and with a coefficient of s = 0.38, the source lines of code metric exhibited a stronger correlation than all centrality metrics considered. In contrast, network centrality metrics worked well in predicting the most important concepts within AFP entries: Of the definitions deemed most important by entry authors, 52.2% could be identified at a precision of 27.8% (optimal F1-score), using in-degree centrality. At the cost of a few percentage points of precision, a second maximum can be achieved with 69.2% recall.

ABSTRACT. Since its inception in 2004 the Archive of Formal Proofs has grown in size but its interface and functionality have only been minimally improved. To transform the AFP into a more user-friendly and effective resource, we redesigned the website to meet modern web standards and practices. We ensure that our work is community-driven by basing the redesign on results from a survey of the Isabelle community. The site generation uses Hugo and is implemented as a proper Isabelle component, which also allows us to adapt the AFP meta-data model to avoid inconsistencies in the future. Notable improvements include a responsive design, new theory browsing interface, integrated search, and enhanced navigation.

ABSTRACT. Mathematical formulae are a foundational component of information in all scientific and mathematical papers. Parsing meaning from these expressions by extracting textual descriptors of their variable tokens is a unique challenge that requires semantic and grammatical knowledge. In this work, we present a new manually-labeled dataset of mathematical objects, the contexts in which they are defined, and their textual definitions. With this dataset, we evaluate the accuracy of a number of modern neural-network models on two definition extraction tasks. While this is not a solved task, modern language models such as BERT perform very well (∼90%). Both the dataset and neural-network models (implemented in PyTorch jupyter-notebooks) are available online to help aide future researchers in this space.

ABSTRACT. The ar5iv Lab was introduced in February 2022. It is an official, web-native preview of arXiv's corpus of scholarly preprints. In 2022, we can showcase a level of coverage and fidelity in converting LaTeX to HTML5 so as to receive wide community approval and initiate a new partnership under the arXiv Labs umbrella. This feat took us 15 years since the project was first presented to the CICM community.

In this talk, I will outline the history and strategic decisions that helped us get here. I will also explore some of the open problems that keep us at 75% success rate in conversion. The core task at hand continues to be one of rescuing documents written for the requirements of a printed page into a web-native future.