Gödel's incompleteness theorem  project summary
Some related reading 

Janna Levin's recent novel based on the lives of Kurt Gödel and Alan Turing 

My Gödel's incompleteness theorem project has now produced an undecidable statement, and on this page there is a brief summary of how the project has gone, and what it might lead to in the future. The first thing to note is that the undecidable statement produced is a lot shorter than I thought it might be. When I started I had in mind a compiler which might produce a program of hundreds of kilobytes in length. I would then have to convert this into an arithmetical statement, and this might well have produced hundreds of characters for each byte of the program, leading to a statement of over a hundred megabytes. What made things a lot simpler was realising how suitable the programming language Haskell was for the task. The pure functional nature of Haskell made it very similar to the arithmetical formulae that it was to be converted too, and so this great expansion of the program did not occur.
Possible Problems
I have to say here that I am not an expert in mathematical logic, and there might be something that I have overlooked that means that what I have done is not valid, and so that the sentence produced is not undecidable. Alternatively there might be a bug in the programs I have written (but that would be easier to patch up). The main area that I intend to look at is whether there will be any problems due to using a bit shifting method to define the Gödel numbering rather than Gödel's method based upon the prime decomposition of numbers. The reason that I will focus on this is that in Computability and logic by Boolos, Burgess and Jeffrey, a positional numbering method is considered, but rejected in favour of the prime number method. On the other hand, I feel that the method I have used is fairly persuasive, and so is probably OK.
Future Work
There are certainly plenty of ways in which this project can be continued. I intend to tidy up and document the code,in particular to describe what parts of Haskell the conversion applet will accept. Apart from that, I've listed several ideas below. However, I'm not sure that I'll carry these out  for one thing I've got plenty of other stuff to do, but it also struck me that most of these would make an ideal project for a computer science undergraduate. If you plan to do any of these then do let me know.
Extend conversion program
The conversion applet at present only accepts a very limited subset of Haskell. In particular it doesn't do any of the pattern matching which is really the essence of Haskell. This is because the limited subset was all that was needed to carry out the project, but adding such pattern matching shouldn't be too much of a problem, at least as far as generating the output is concerned  the mechanics of the pattern matching is technial, but is present in existing Haskell compilers.
Haskell version of conversion program
I wrote the conversion program in Java because I was reasonably familiar with the language, and it provides a straightforward way of putting it on to a website. However, there are programming languages which are more suited to writing such 'compilerlike' programs, in particular Haskell itself  Haskell compilers are generally written in Haskell.
∃ ∧ ∨
When I started the project I wanted to keep the programs as simple as possible. Hence I chose a form of the arithmetical axioms with the least number of symbols. This meant, however, that expressions involving the symbols ∃ ∧ and ∨ had to be converted into ones just using ∀ and ⇒, which rather disguised what was going on. If I was starting again, I would definitely include ∃ ∧ and ∨ even though this would involve more axioms to define the relationships between the symbols.
Simpler interfaces, proof creation program
Encoding my proof of 1+1=2 took quite a while, with plenty of opportunity to introduce errors. It would be good if there was a program to help with this, so that more proofs could be encoded, and thus checked with the proof code applet. There is also scope to simplify the process of entering a proof and obtaining the statement proved at the end.Further exploration of mathematical logic
Gödel's incompleteness theorem isn't the only important theorem of mathematical logic  there are plenty of related results, which would benefit from a similar project to actually produce statements that are shown to exist.
Who needs a computer?
One thing that struck me when I was writing and testing the conversion program was that it involved a lot of working out by hand what a result should be and checking that the program agreed with this. So why not do the whole thing by hand?  it probably wouldn't have taken any longer. Also, there would be the possibility to introduce abbreviations in the rather long winded undecidable statement, and so end up with something that could be written in an even shorter way.