The implication graph is 99.9957% complete.

An implication is explicitly true or explicitly false if we directly have a proof of the corresponding proposition in Lean. It is implicitly true or implicitly false if the proposition follows 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
30515	8147764	582132	13272284	941

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	197	12	732

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

progress visualization