A library for computational graph theory in Lean 4, with emphasis on verification of large datasets of graphs; in particular the House of Graphs (HoG).
You need the following software:
- Lean 4 proof assistant: Install Lean 4 by following these instructions. When successful, you should have the executables
elan
(for installing and updating versions of Lean),lean
itself, andlake
(the Lean build system). - (Visual Studio Code): the editor that has good Lean support.
- Node.js and
npm
cli. - Python version 3, with the requests library, which you can install with
pip3 install requests
.
On MacOS you can use Homebrew to install Visual Studio Code and Node.js
with
brew install npm
brew install --cask visual-studio-code
For using the SAT solving facilities of the library (e.g. computing Hamiltonian paths) you need the following:
- A modern SAT solver capable of producing proofs of unsatisfiability, we recommend CaDiCaL.
- A SAT proof checker, we recommend the formally verified checker cake_lpr.
Once you have installed the SAT solver and a proof checker, you should set in Lean
leanHoG.solverCmd
to the location of the SAT solver executable.leanHoG.proofCheckerCmd
to the location of the SAT proof checker.
To install all the dependencies and compile Lean-HoG, run these commands from withing the Lean-HoG directory:
elan update
to make sure you have an up-to-date version of Lean,lake exe cache get
to get a cached version of Mathlib (or else wait for it to compile),lake exe build_widgets
to build the Javascript graph visualization widgets,lake build
to compile Lean-HoG
The library uses Python to interact with the HoG database and process the data before it's imported in Lean. To make Lean aware of the location of your Python executable set
set_option leanHoG.pythonExecutable <path-to-python>
Open the file Examples.lean
to check whether the example graphs load successfully.
To download graphs from the House of Graphs (HoG) you can
use the #download <graphName> <hog_id>
command.
It downloads the graphs with House of Graphs ID hog_id
and loads it into the variable graphName
.
You can check that it loaded it with #check <graphName>
.
Note: To download the graph it uses an external python script. The location of the python executable is provided by the user option leanHoG.pythonExecutable
.
Note: The python environment is expected to have the requests library installed.
#download Petersen 660
#check Petersen
Lean-HoG can visualize the imported graphs in the Lean infoview using widgets, which work by running Javascript in the Infoview. The visualization uses the cytoscape.js javascript library.
Try them out by opening the Examples.lean
file and clicking on the line #show Cycle7
. In the info view you should now see something like this:
You can query the House of Graphs database from within Lean via the command #search
.
To use it you have to construct a valid hog_query
and enclose it into
hog{ }
syntax. It has the following syntax:
hog_query q ::= boolean_invariant = b | numerical_invariant op x | query_formula op query_formula | ( q ) | q ∧ q | q ∨ q
where b
is a boolean value, x
is a numerical value
(Int
for invariants with integral values, Float
for invariants with continous values),
op ::= < | <= | > | >= | =
and
query_formula f ::= x | numerical_invariant | f + f | f - f | f / f | f * f
The list of available invariants can be found in the House of Graphs documentation. The invariants use lower camel case.
#search_hog hog{ bipartite = true ∧ (numberOfEdges = 1 ∨ numberOfVertices < 6) }
Should display the following in the Infoview:
Found 9 graphs satisfying given query
Found solution hog_302
Found solution hog_300
Found solution hog_296
Found solution hog_294
Found solution hog_310
Found solution hog_298
Found solution hog_304
Found solution hog_19655
Found solution hog_49432
The solutions point to the relevant page on the House of Graphs for each graph. The graphs are also available in Lean, which you can check with e.g.
#check hog_302
The library provides a tactic find_example
,
which uses the search feature to close certain goals of the form
∃ (G : Graph), P G
for Boolean predicates P
.
The predicate P
must be a conjunction of comparisons of invariants with
either invariants or numbers.
The supported invariants are those Lean-HoG currently implements. They include:
vertexSize
edgeSize
minimumDegree
maximumDegree
numberOfConnectedComponents
traceable
bipartite
connectedGraph
example : ∃ (G : Graph), G.traceable ∧ G.vertexSize > 3 ∧
(G.minimumDegree < G.vertexSize / 2) := by
find_example
The JSON file should have the following structure.
{
"graph" : {
"vertexSize" : <number of vertices>,
"edges" : <list of edges>,
},
<invariants>
}
IMPORTANT:
Lean-HoG expects all lists and maps, including the list of edges, to be (lexicographically) ordered.
In particular, edges must be ordered pairs ([1, 2]
, never [2, 1]
) and
the list of edges should be lexicographically ordered.
Consult the (examples
)[./examples] folder.
"neighborhoodMap" : {
"neighbors" : <map vertices to their neighbors>,
}
"connectedComponents" : {
"val" : <number of components>,
"component" : <map vertices to components>,
"root" : <map components to their roots>,
"next" : <map vertices to their parents, roots to roots>,
"distToRoot" : <map vertices to their distance to the root>,
}
"bipartite" : {
"color" : <map vertices to color, 0 or 1>,
"vertex0" : <vertex with color 0>,
"vertex1" : <vertex with color 1>,
},
"oddClosedWalk" : {
"closedWalk" : <list of vertices>,
}