We have started talking about a collection of notes. More info on the page about The book.
Working group on informal type theory
One of our projects is to present informal versions of various theorems, both verbally and in a written way, and criticize them. These theorems may or may not have yet been proven formally.