Incorporating a Database of Graphs into a Proof Assistant

Incorporating a Database of Graphs into a Proof Assistant

연구 분야: Databases

학회: International Conference on Intelligent Computer Mathematics

There are clear benefits to incorporating mathematical databases and software into a proof assistant. On the one hand, the assistant gains access to mathematical facts that require significant computational resources or manual curation. On the other hand, formal verification carried out by the proof assistant provides a high degree of correctness assurance on the data. We implemented Lean-HoG, a Lean 4 library for finite simple graphs that imports and verifies mathematical facts from the House of Graphs, a popular collection of more than 23000 curated graphs with associated graph-theoretic invariants. In order for Lean 4 to be able to process the database, we formalized a computationally efficient definition of graphs and auxiliary structures for a selection of graph-theoretic invariants. To verify the invariants provided by the database, we used several techniques. Some invariants, such as the number of edges, can be efficiently computed by the Lean kernel directly from their definitions. There are invariants that the Lean kernel can verify efficiently when given a suitable certificate, e.g., bipartiteness is witnessed by a vertex 2-coloring and its failure by an odd cycle. In these cases we generate the certificates externally (the database typically does not provide them). The most demanding are the NP-complete invariants. To demonstrate this case, we used the LeanSAT library to formalize the SAT encoding of traceability (existence of a Hamiltonian path) and have Lean delegate verification to an external SAT solver. We expect our approach to apply to other mathematical databases, as well as to computational software.