Here is the abstract:
Call a program `elegant' if no smaller program has the same output. I.e., a LISP S-expression is defined to be elegant if no smaller S-expression has the same value. For any computational task there is at least one elegant program, perhaps more. Nevertheless, we present a Berry paradox proof that it is impossible to prove that any particular large program is elegant. The proof is carried out using a version of LISP designed especially for this purpose. This establishes an extremely concrete and fundamental limitation on the power of formal mathematical reasoning.
In his proofs, Chaitin uses a simple form of the AI programming language LISP. This LISP is powerful enough to do anything a computer can do (but it would be painful to program and very slow) The LISP complexity of an axiomatic system is, more or less, the number of characters used in the LISP description of the system.
Here is how bad things are: "A formal axiomatic system whose LISP complexity is N cannot prove that a LISP expression is elegant if the expression's size is greater than N + 410. So at most finitely many LISP expressions can be shown to be elegant."