Two formalizations of Löb's Theorem.
In axiomatization/, an axiomatic formalization of Löb's Theorem,
based on The Cartoon Guide to Löb's
Theorem
In internal/, a start on a formalization based on a well-typed
quine, started with the help of Benja Fallenstein at the June 2015
MIRI Workshop on Decision Theory.