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),leanitself, andlake(the Lean build system). - (Visual Studio Code): the editor that has good Lean support.
- Node.js and
npmcli. - 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 LRAT proofs of unsatisfiability, we recommend CaDiCaL.
Unsatisfiability proofs are checked by Lean's built-in verified LRAT checker; no separate proof-checker executable is required.
Once you have installed the SAT solver, set leanHoG.solverCmd in Lean to the
location of the solver executable.
To install all dependencies and compile Lean-HoG, run this command from the Lean-HoG directory:
lake buildLake installs the Lean version pinned in lean-toolchain, fetches the package
dependencies, installs the JavaScript dependencies, builds the graph
visualization widget, and then compiles Lean-HoG. The widget does not need to be
built separately. Mathlib's update hook also fetches its cached build artifacts
automatically, so there is no separate cache command to run.
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 Petersengraph6 is nauty's encoding of an undirected simple graph as a short string of printable ASCII, and is what geng, nauty, networkx, SageMath and the House of Graphs hand out. HoG's canonicalForm field is a graph6 string.
load_graph_from_g6 <graphName> <g6> loads the graph encoded by a graph6 string:
load_graph_from_g6 Petersen "IsP@OkWHG"
#show Petersen
#eval Petersen.numberOfConnectedComponentsload_graphs_from_g6_file <graphName> <file> loads every graph in a graph6 file, one per line as geng writes them, into graphName_0, graphName_1, … in the order the lines appear. Blank lines and a lone >>graph6<< header line are skipped.
load_graphs_from_g6_file Sample "examples/hog-sample.g6"
#show Sample_0Each graph in the file becomes a separate compiled declaration, so a file with thousands of lines takes a correspondingly long time to elaborate.
Neither command attaches any invariant certificate, so invariants of a graph read from graph6 are decided by search rather than read off a certificate.
Graph.toGraph6 goes the other way, encoding a graph under its own vertex labelling:
#eval Petersen.toGraph6Only graph6 is supported; sparse6, the :-prefixed format, is not.
Without a certificate, Graph.bipartite is decided by enumerating all 2^n maps G.vertex → Fin 2, which is out of reach past a couple of dozen vertices. #check_bipartite <graphName> decides it by breadth-first search instead, and registers the certificate for whichever answer it reaches: a TwoColoring if the graph is bipartite, an OddClosedWalk if it is not. Later invariant queries read the answer off that certificate.
load_graph_from_g6 Petersen "IsP@OkWHG"
#check_bipartite Petersen
#eval Petersen.bipartiteThe command reports what it found. The tactic check_bipartite <graphName> puts the fact into a proof, adding G.bipartite or ¬ G.bipartite to the context as a hypothesis; check_bipartite <graphName> with h names it, and check_bipartitea <graphName> closes the goal with it directly. No solver is involved and no axiom is asserted: the kernel checks the certificate the search produced.
example : ¬Petersen.bipartite := by
check_bipartitea PetersenLean-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_302The 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:
vertex sizeedge sizeminimum degreemaximum degreenumber of connected componentstraceablenon traceablebipartitenon bipartiteconnectedHamiltonian
example : ∃ (G : Graph), G.traceable ∧ G.vertexSize > 3 ∧
(G.minimumDegree < G.vertexSize / 2) := by
find_exampleThe 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>,
}