The Coq mailing list

[Laurent Théry <Laurent.Thery AT inria.fr>]

On 02/04/2015 11:16 PM, Bas Spitters wrote:
> Russell proved the *first* incompleteness theorem.
> Remarks on the second incompleteness theorem can be found in sec 7.4 here:
> http://link.springer.com/chapter/10.1007%2F11541868_16
>
> Larry Paulson was the first to formalize the *second* incompleteness
> theorem (in Isabelle):
> http://www.cl.cam.ac.uk/~lp15/papers/Sets/
> http://afp.sourceforge.net/entries/Incompleteness.shtml

John Harrison also mentions something about the proofs of Gödel theorem 
in his wonderful book
Practical Logic and Automated Reasoning

--
Laurent