When I stumbled upon this title , I did not hesitate for a second to order it. A mathematical book on the theory of evolution and written by the the famous Gregory Chaitin on top of that. Things looked so promising and I was anxious to get the book by mail.
The first impression when I got the book in my hands was that it was very thin. Though, I did not want to let myself be fooled by the the size.
Proving Darwin aims at introducing a new science founded by Gregory Chaitin himself and called Metabiology. The book describes a toy universe of evolution. A model that,according to Chaitin, captures the essence of evolution yet it remains simple enough to be tackeled mathematically.
In a nutshell, Chaitin's universe consists of a single individual, a program. This program calculates a natural number. At every step, this program is randomly mutated into a new individual. If the new individual halts and if it produces a number bigger than its parent, then it replaces the parent. Chaitin proved that this evolutianary process converges to an individual that produces the biggest integer after a polynomial number of generations.
Now, let us dive a little bit more into some mathematical technicalities. Every program P is encoded as a binary string of size N. A program is the concatenation of a script and some input data. The script represents the instructions of P. Chaitin's theorem states that evolution will yield a program P* that generates a number called the busy beaver number (denoted by BB(N)) in a number of generations bounded by N2 and N3.
In this universe, like in biology, mutations occur probabilistcally. Life makes use of point-change mutations, that is changes to individual genes. Therefore, the most disruptive mutations (those that change many genes in a single step) are much less likely. Chaitin makes use of what he calls algorithmic mutations in his universe and this was the most exciting idea I have found in this book. I think that algorithmic mutations compare to point-change mutations in the same way as program code compares to program data or as Kolmogorov-Chaitin complexity compares to Computational complexity.
An algorithmic mutation Mk is an algorithm than transforms some program P into a program P'. Parameter k is the size of this algorithm in bits. Mutations of size k are generated with a probability of 1 / 2-k as one can guess a bit of this mutation with a probability of 1/2 and all k bits with a probability that equals the product of the individual probabilities. The interesting fact about algorithmic mutations is that very distruptive mutations might be chosen with a high probability. For instance, an algorithmic mutation that flips every bit of a program P can be described very concidely and therefore will be chosen often.
As not every k-bit string is a valid mutation. Chaitin makes use of oracles to decide if Mk is a valid mutation and if it will ever halt and generate a mutant P'. Oracles have first been introduced by Alan Turing in 1939. We can see them as super powers that are able to compute what computers are not able to. In this particular case, oracles are used to solve the non-computable halt problem. Oracles are also used to decide whethere the mutant programs are going to halt or not.
So, this means that evolution in this universe still needs the intervention of some external entities with higher-powers. Call these entities God, Aliens or whatever, but for the time beings it still needs to be proven that programs (or artificial life) is able to evolve.
Finally here a few pet peeves. The book was quickly written and mostly used an informal style. I looked more like a compilation of lecture notes and talks' material. Gregory Chaitin touched upon interesting topics in biology, mathematics and computer science. Though, no deep insights have been given which was disappointing.
A more formal presentation of the problem as well as the proof of the theorem can be found in this Chaitin's technical report : To a mathematical theory of evolution and biological creativity.
Chaitin's model isn't really algorithmic
You give a nice summary of the book, but it is dangerous to stick to Chaitin's terminology. By his choice of words he inflates the significance of his model, except for the first program, all subsequent 'mutations' produce specific types of programs which are just a self-delimiting header followed by a fraction. The sad part is that he never uses the full power of algorithms at all, and produces a very boring model when it is recast in simpler terms:
http://egtheory.wordpress.com/2012/07/08/algorithmic-mutation/
I had very high hopes for this book (much like you) when I saw it in the bookstore. After reading and reflecting, I was extremely disappointed :(.