This is a detailed WWW representation of a KIV project with specifications, theorems, and proofs.
You should begin with a look at the project with graph to get an overview over the specifications and their structure. From there you can browse the individual specifications and then the proofs.
The project statistic contains information about the number of theorems, proofs, proof steps, user interactions, etc.
The formulas use logical symbols like and, or, always quantifier, and mathematical symbols like empty set, union etc. To check which symbols are available in your browser you can take a look at the KIV symbols.
The meaning of colours in proof trees is explained here.