Automated mathematics: integrating proofs, algorithms and data

In addition to well-known mathematical databases, such as the OEIS, LMFDB and the House of Graphs, there is a multitude of smaller projects. Any of these might be interesting to researchers from other areas, including machine learning. However, the smaller dataset projects are typically hard to find: just the right keywords are usually necessary (but not necessarily sufficient) to find them with standard search engines and even in scientific research data repositories (like Zenodo). As a community, we should build a collaborative, and at least partly automated, index of mathematical datasets. Personal projects, such as my own mathdb.mathhub.info, can serve as a starting point.

I’d be happy to report on and discuss some ongoing work (with S. Dahmen and S. Huriot-Tattegrain) implementing a tricky mathematical algorithm in the field of number theory / arithmetic geometry in a proof assistant (this computes certain quantities appearing in the famous BSD conjecture many of which are recorded in the LMFDB). This algorithm, known as Tate’s algorithm in the field, is quite involved with many subcases and a non-trivial proof of terminations, and takes many pages to describe when expressed in paper form.

One thing that makes this an interesting is that to give a formal definition of the quantities the algorithm actually computes is still out of reach, nevertheless the steps of this algorithm as described in the literature can be implemented and termination can be proved with some non-trivial tracking of the state involved, but in what ways is this implementation more trustworthy than one in a regular programming language? I’d like to consider what guarantees implementing such code in a the strict setting of a proof assistant can give us, compared to ordinary code, even when the gold standard isn’t yet attainable.

The direct relationship between the mathematical theory and the code in this case means that this implementation very clearly states what assumptions are made about the ring we are working in, and in fact makes this the most general implementation available, this then begs the question: how can we best integrate mathematical code written using proof assistants into existing CASes? So it may be useful to users not running proof assistants themselves.

Recently Andrej Bauer coined the term “invisible mathematics” for those aspects of mathematics which are readily apparent when doing them mechanically (especially, but not only, in proof assistants) but which is essentially invisible in traditional paper-math. Three main examples were given, and their formalization discussed.

Here we aim to give more such examples – but the aim is not on how to formalize them, but rather to observe their consequences. In particular, some instances of “invisible mathematics” readily reveal the cognitive load on learners of some (visible) mathematics. Rather than seeing parts of the “de Bruijn factor” as an impediment, we instead regard it as a learning opportunity.

We have previously [1] asked the question “Do I believe the output from my (complicated, optimised, unverified) computer algebra system?”. If it gives me a positive answer, e.g. “the answer to $\int f$ is $g$”, then we can check that $g^{\prime }=f$, etc. But what if it says “there is no answer”? In particular, if we ask to factor the polynomial $F$, then we can check that the factors multiply to $F$, but what about the (implicit) statement that these factors are irreducible? Currently, the user just has to believe the algebra system. We ask, and partially answer, the question “could the algebra system also produce a certificate, or the hints to construct a certificate, of irreducibility of the factors” (based on the work the algebra system has already done). This was taken up by one working group.

We describe the project Network Mathematics we are developing at the Topos Institute, Berkeley, CA. We hope to take advantage of the tremendous recent progress in Natural Language Processing (NLP), including LLMs, transformers, etc, to extract information from mathematical texts. Also we think mathematical language is what mathematicians use when communicating with each other, so we should leverage mathematical English to increase the accessibility of mathematics to mathematicians, students and the general public.

To work on these goals, we have three main preliminary subprojects:

1. 1.

   MathGloss (together with Lucy Horowitz, Chicago) – a collection of glossaries of college math, connected to each other via WikiData.

2. 2.

   Parmesan (together with Jacob Collard and Eswaran Subramahnian, NIST) provides semantic search on the field of Category Theory, using different knowledge bases at different levels (research math, wiki math and textbook math).

3. 3.

   MathChat (together with Gao, Kovalev and Moss, Indiana) using generative AI (chatGPT and GTP-4) to extract concepts from text.

All these subprojects need to grow and need to include more sources. Also, further work needs to be done to structure the extracted concepts into a proper ontology, to obtain a proper Knowledge Graph for mathematics.

The talk gives a quick overview of some tools developed around Dedukti to verify, re-verify or cross-verify proofs, more precisely, Zenon Modulo, iProverModulo, Archsat, and Ekstrakto. The three first ones directly produce Dedukti proofs that can be checked by the Dedukti checker. The latter reconstructs a Dedukti proof from a proof trace by reproving each step using a Dedukti producing tool and combining the proofs of the steps to get a proof of the original formula. In the talk, we also point out two projects: BWare and ICSPA. The first one aimed at developing a mechanized framework for automated verification of AtelierB proof obligations where Zenon Modulo and iProvermodulo were developed or used. ICSPA is a project in progress where the objectives are to improve confidence in the proofs realized in the context of B/Event-B and TLA+ by formally and independently verifying these proofs and also to enable sharing and reusing proofs and models between B/Event-B and TLA+ using lambda-PI calculus modulo theory and Dedukti.

Automated deployment of component-based applications in the Cloud consists in the allocation of virtual machines (VMs) offers from various Cloud Providers such that the constraints induced by the interactions between components and by the components hardware/software requirements are satisfied and the performance objectives are optimized (e.g. costs are minimized). It can be formulated as a constraint optimization problem, hence, in principle, the optimization can be carried out automatically. In the case the set of VM offers is large (several hundreds), the computational requirement is huge, making the automatic optimization practically impossible with the current general optimization modulo theory (OMT) and mathematical programming (MP) tools. We overcame the difficulty by methodologically analyzing the particularities of the problem with the aim of identifying search space reduction methods. Some of these methods are exploiting the symmetries of the general Cloud deployment problem leading to symmetry breakers. However, little is know/understood about the symmetries of this problem which could lead to symmetry breakers which are not experimentally constructed. We present some of the symmetries of a simplistic formulation of automated deployment with the hope that the audience:

• $\mathrm{■}$

  can bring input regarding approaches applied for similar problems (bin-packing)

• $\mathrm{■}$

  is interested in taking part in a small working group to discuss if invariant theory of finite groups (see, e.g., Chapter 7 of [1]) could bring some insights towards the formalization of symmetries.

We will present the House of Graphs (https://houseofgraphs.org/), which is a database of graphs. The House of Graphs hosts complete lists of graphs of various graph classes (e.g. cubic graphs, fullerenes, trees, etc.), but its main feature is a searchable database of so called “interesting” graphs, which includes graphs that already occurred as extremal graphs or as counterexamples to conjectures. We will highlight the features of the website and demonstrate how users can perform queries on this database and how they can add new interesting graphs to it.

The cost of maintaining formally specified and verified software is widely considered prohibitively high due to the need to constantly keep code and the proofs of its correctness in sync—the problem known as proof repair. One of the main challenges in automated proof repair for evolving code is to infer invariants for a new version of a once verified program that are strong enough to establish its full functional correctness.

In this work, we present the first proof repair methodology for higher-order imperative functions, whose initial versions were verified in the Coq proof assistant and whose specifications remained unchanged. Our proof repair procedure is based on the combination of dynamic program alignment, enumerative invariant synthesis, and a novel technique for efficiently pruning the space of invariant candidates, dubbed proof-driven testing, enabled by the constructive nature of Coq’s proof certificates.

Mathematical data are available in all sorts of formats on the web. Often it is difficult for those who did not create the data to use them. Also these data are at risk of disappearing. We advocate for the building of a system consisting of

• $\mathrm{■}$

  a centralised database of mathematical objects, checked by peers,

• $\mathrm{■}$

  a website permitting to extract data from the database and send it to computational software (Magma, gap, etc.) to test conjectures, build more objects, …

MLFMF is a collection of data sets for benchmarking recommendation systems used to support formalization of mathematics with proof assistants. Each data set is derived from a library of formalized mathematics written in proof assistants Agda or Lean. The collection includes the largest Lean 4 library Mathlib, and some of the largest Agda libraries: the standard library, the library of univalent mathematics Agda-unimath, and the TypeTopology library. Each data set represents the corresponding library in two ways: as a heterogeneous network, and as a list of s-expressions representing the syntax trees of all the entries in the library. The network contains the (modular) structure of the library and the references between entries, while the s-expressions give complete and easily parsed information about every entry.

I will present how I integrated in LambdaPi an indexer and search engine for mathematical formulae up to instantiation/generalization. The search engine allows to query in parallel libraries obtained by various provers (e.g. HOL/Matita/Coq/…) via an encoding into Dedukti/LambdaPi.

The task poses several challenges that are novel compared to search engines developed for a single system:

1. 1.

   the statements occur encoded in LambaPi and the same statement coming from several systems is encoded in a different way

2. 2.

   the statement can occur in several shapes, up to rewriting rules

3. 3.

   in order to look in parallel in several libraries, one need to search up to alignment of constants.

I have solved all three previous challenges exploiting the rewriting engine of LambdaPi in order to:

1. 1.

   undo the encoding via a non-type preserving transformation,

2. 2.

   normalize the statements before indexing and the queries as well,

3. 3.

   rewrite all cosntants to a canonic form (the representative of the equivalence class of aligned formula).

Indexing has been implemented combining substitution trees and information positioning (the one exploited in the Whelp system).

SRI’s Prototype Verification System (PVS) is an interactive proof assistant based on higher-order logic developed at SRI over the last three decades as a unified platform and language for formal specification, mathematical modeling, programming, and proof. It has been used to develop extensive libraries for mathematics and computing and for verification projects spanning fault-tolerant systems, air-traffic control systems, parsers, compilers, separation kernel, data refinement, and hardware. Nearly all of the specification language is efficiently executable with code extraction to Common Lisp and C, and experimental code generators targetting standard ML and Rust. We describe some of our experiments with modeling, proof, and computation focusing on extracting efficient C code from verified definitions.

During the Dagstuhl Seminar, we used PVS to verify two witness formats and executable checkers for graph connectivity. The witness for connectivity is a sequence containing all of the vertices such that each vertex has a neighbor in the preceding part of the sequence. This implies, by induction, that the graph is connected. For disconnectivity, the witness is a $k$-coloring of the vertices for $k>1$ such that no vertex has a neighbor of a different color.

In the talk I presented my recent work in progress on Enumerion, which is a system for systematic enumeration of finite mathematical structures based on dependent type theory and implemented in OCaml. The problem of counting and enumerating discrete finite structures is a classical one. In the history of counting there are however quite a few published mistakes[1]. The idea of this system is to have a systematic way of describing the enumeration problem which is amenable to formalization. After explaining the idea behind the system I showed a short demo of the current capabilities of Enumerion.

We introduce a self-learning algorithm for synthesizing programs that provide explanations for OEIS sequences. The algorithm starts from scratch initially generating programs at random. Then it runs many iterations of a self-learning loop that interleaves (i) training neural machine translation to learn the correspondence between sequences and the programs discovered so far, and (ii) proposing many new programs for each OEIS sequence by the trained neural machine translator. The algorithm discovers on its own programs for more than 78000 OEIS sequences, sometimes developing unusual programming methods. We analyze its behavior and the invented programs in several experiments.

Isabelle is usually seen as an interactive proof assistant, mostly for Higher-Order Logic (HOL), but that is somehow accidental. In reality, Isabelle is a system platform for functional programming and formal proofs, with sufficient infrastructure to carry its own weight and gravity. The Archive of Formal Proofs (AFP) is the official collection of Isabelle applications that is maintained together with the base system. That poses ever growing demands on the Isabelle platform. This talk gives an overview of Isabelle software technology, with specific focus on Programming and Scaling, e.g. distributed build clusters for AFP.

The working group worked on pushing the entries (that correspond to formalized mathematical concepts) from Coq, Isabelle and Dedukti systems into graph databases, on which machine learning can be applied.

To unify the schema of the created networks, we

• $\mathrm{■}$

  adjusted the RDF triplets describing the Coq entries,

• $\mathrm{■}$

  wrote an extension of Dedukti parser that extracts the necessary information from abstract syntax trees of the entries,

• $\mathrm{■}$

  and wrote parsing tool for Isabelle XMLs.

The end goal was include this work to the series of the existing networks, extracted from the largest Agda libraries and Mathlib4 library of Lean.

We thank Talia Ringer and Catherine Dobuis for the ideas.

Object identification up to isomorphism is in general computationally expensive (group isomorphism, graph isomorphism…) and identifying a given object with a representative from a known dataset is difficult.

But often, one is presented with object together with few pre-computed invariants or some invariants, that can quickly be computed from a given representation. Most of the time, the difficulty of calculating the invariant can be approximated relatively well or one can use the timings produced as a side effect of constructing the whole database of objects and associated invariants.

The working group was mostly focused on the problems where objects are graphs or groups and the preliminary experiments were carried out on the dataset, representing graphs. Every graph (a row in the data table) was represented by the number of invariants (columns in the dataset). Some of the values in the table were missing, i.e., not all the variants were computed for all the graphs. The working group experimented with a modification of decision tree algorithm that uses both information gain of an invariant and its calculation difficulty to compute the next invariant on which to split the dataset. With such an approach, we can speed up the identification of unknown object in an existing database of objects.

The results of experimentation: implemented decision tree variant and data acquisition from house of graphs together with evaluation are available at https://github.com/Petkomat/invariant-computation-trees.

Participants in this working group worked on several smaller, but related tasks.