The implication graph is 99.99998% complete.

An implication is considered explicitly true or explicitly false if we have a proof of the corresponding proposition formalised in Lean. It is implicitly true or implicitly false if the proposition can be derived by taking the reflexive transitive closure of explicitly proven implications.

Our current counts of implications in each of those categories are:

explicitly true implicitly true explicitly false implicitly false no proof
10,657 8,167,622 586,924 13,268,429 4

The no proof column above represents work that we still need to do. Among the no proof implications, we have the following conjecture counts:

explicitly true implicitly true explicitly false implicitly false no conjecture
0 0 1 3 0

The implication graph is 100.00000% complete if we include conjectures.

Finite graph

Some implications are true specifically only for finite magmas.

The finite implication graph is 99.99999% complete.

explicitly true implicitly true explicitly false implicitly false no proof
10,750 8,168,349 586,220 13,268,315 2

The finite implication graph is 99.99999% complete if we include conjectures.

explicitly true implicitly true explicitly false implicitly false no conjecture
0 0 0 0 2

Graph info

The following information is derived from graphs without sporadic equations (equations of order > 4) included.

  General graph Finite graph
Implication theorems
Note: The difference from explicit implications is due to duplicates		 10,667 10,760
Refutation theorems
Note: The difference from explicit refutations is that a single theorem can satisfy M equations and refute N equations, explicit refutations is the sum of all M*N, and this is the count of individual such theorems.		 1,321 1,119
Equivalence classes 1,415 1,370
Equivalence classes of size = 1 1,145 1,083
Equivalence classes of size > 1 270 287
Size of the largest equivalence class 1,496 1,496
Transitively closed implications between equivalence classes 28,442 28,106
Transitively reduced implications between equivalence classes 4,824 4,759
Edges in the minimal equivalent graph, this is the optimally minimal number of edges to represent the implication graph making use of transitivity, but not dual relations 8,373 8,370

Raw data

The following compressed JSON blobs contain the raw data generated by project tooling. Note that the exported data includes conjectures.

General graph:

Finite graph:

Progress visualization