Proof is a collection of tools constituting a new way of writing and reading proofs inspired by the ideas of Leslie Lamport.
At the end of the day, the aim of these tools is to end up with a beautiful, interactive proof page like this.
Proof is a markup language for writing structured proofs which compiles to an HTML page. It is heavily inspired by the ideas of Leslie Lamport and by type-theory based proof assistants (specifically Coq and Agda). The aim and the promise of structured proofs is to make mathematics