Gödel proof code applet
Some related reading 

In this book Torkel Franzen examines various ways that this theorem has been wrongly quoted, and tries to set the reader straight on what it is really about. He looks at what has been said about incompleteness in physics, in theology and of course in various postmodern ramblings. 
My review of Godel's theorem : an incomplete guide to its use and abuse 
This is an applet to implement a numerical encoding of arithmetical proofs, as is required in the proof of Gödel's incompleteness theorem. It uses the axiom system describes in A proof system for arithmetic. I you look at the proof in A formal proof that 1+1=2, you will see that the second column is what is normally considered to be the proof  a sequence of arithmetical statements. This encoding however, is based on what is in the third column  a description of the axiom used, with parameters as required. These descriptions can then be used to build the sequence of statements in the second column.
The proofs are encoded based on the following table:
The proofs are encoded based on the following table:
End of proof  00  
Ax1(WF1,WF2)  WF1⇒(WF2⇒WF1)  0001 
Ax2(WF1,WF2,WF3)  (WF1⇒(WF2⇒WF3))⇒((WF1⇒WF2)⇒(WF1⇒WF3))  0101

Ax3(WF1,WF2)  (¬WF2⇒¬WF1)⇒((¬WF2⇒WF1)⇒WF2)  1001 
Ax4(V,T,WF)  ∀V WF(V)⇒WF(T)(T is a term free for V in WF)  0010 
Ax5(V,WF1,WF2)  ∀V(WF1⇒WF2)⇒(WF1⇒∀V WF2) WF1 has no free occurence of V  0110 
Ind(V,WF)  WF(0) ⇒((∀V (WF(V) ⇒ WF(V'))) ⇒ ∀V WF(V))  1010 
MP(l1,l2)  WF1,WF1 ⇒ WF2  WF2  0011 
Gen(V,l1)  WF  ∀V WF  0111 
I1  x=y⇒(x=z⇒y=z)  0001 
I2  x=y⇒x'=y'  0011 
I3  ¬0=x'  0101 
I4  x'=y'⇒x=y  0111 
I5  x+0=x  1001 
I6  x+y'=(x+y)'  1011 
I7  x*0=0  1101 
I8  x*y'=(x*y)+x  1111 
The formulae, variables and terms in the proofs are encoded using the scheme described in Gödel numbering applet. As with that page, the encoding uses a reverse polish encoding, and progresses from the least significant bit of the number. The applet thus takes a number representing the sequence of axioms used, and outputs a list of numbers representing the statements proved (using the encoding in Gödel numbering applet).
I realise that this is likely to be confusing, so the best thing to do is to try it out. Copy the number from the the proof.txt file into the top box, and press the down button.
I would have put the number on this page  its less than 500 digits  but it needs to be all in one piece and so won't wrap on the page.
A sequence of numbers will appear in the lower box. Copy these to the applet on the Gödel numbering applet page and use that to generate a sequence of statements. This should end with (0'+0')=0'', which is the same as 1+1=2. The statements will reproduce the proof given on the page A formal proof that 1+1=2
I recognise that these applets are a bit clumsy at the moment, (it took several days work to create the encoding for the proof of 1+1=2). I hope to improve them as time goes on. But the important part isn't so much using them, it's the existence of a function which can translate and encoded form of a proof into an encoded form of the statement to be proved. This will be used in generating an undecidable statement.
Source code 
Source code Licence 