Goldbach's Conjecture, Turing Machines, and Artificial Intelligence

When I was a graduate student I'd work on proving Goldbach's Conjecture when I needed a break from my real research. I'd focus on what this Wikipedia article (http://en.wikipedia.org/wiki/Goldbach's_conjecture) calls the strong form : every even natural number (aka even positive integer) greater than 5 can be expressed as the sum of two prime numbers. So, for example, 6 = 3 + 3, 8 = 5 + 3, 10 = 5 + 5 (and 7 + 3), 12 = 7 + 5, .... Again, this is a conjecture that is believed to be true by virtually everone and its truth has been demonstrated with computers up to huge even numbers, but no one has proved its truth for all even numbers, and there are an infinity of them.

The really attractive thing about number theory is that so many of the problems are so easy to understand by so many -- you may not be able to solve the problem, but you sure understand what's being asked! An approach I hit upon to prove Goldbach's conjecture (or I suppose disprove it, or perhaps that you could'nt prove it one way or the other!) was essentially this, write a computer program that ran forever (if you were to run it), generating the even natural numbers one after the other, and write another computer program that ran forever (again, only if you were to actually run it), that generated all the sums of two primes "in sequence", and then show that the two programs were equivalent. Unfortunately, that last step is REALLY, REALLY hard, if doable at all, but fortunately my PhD research took off about this time and I did that instead, much to the relief of my wife, parents, and in-laws!

But now, just as I want my artificial intelligence students to find projects of interest, this is the project that I want to return to. Its been about 3 years since I've done my own substantive computer programming, and its probably been 15 years since I've done substantive programming in the LISP language. So this will be fun! I can trivially write a program that generates all even natural numbers greater than 5: (defun GenEven () (do ((i 3 (+ 1 i))) (t (princ (* 2 i))))). A program that generates the sum of all pairs of primes is a good deal more complicated, because in general each addend needs to be verified as prime (http://en.wikipedia.org/wiki/Prime_number). In fact, one way to write this second program is simply to write a program that generates all prime numbers, and then "append" it to a copy of itself, and as each copy produces a prime the sum is output. However we write the second, what we imagine is something remarkable -- that the latter very complicated program is equivalent to the former very simple program.

It would be tempting to spend a good deal of time making each of these programs as concise or as efficient as possible, but you see, I am never going to run either program. If I am biased in any direction it is that each program be as "unstructured" and as "primitive" as possible, because once these programs are defined, a third program, an AI program, is going to search for a sequence of rewrites that will transform one program into the other, while provably maintaining the original functionality of each. The third (AI) program is the one that will actually be run, and I'll be writing this program in Lisp. But the two programs, one for generating the even numbers and one for generating the sums of prime pairs, I'm imagining will be written in the most primitive of languages -- the language for programming (or defining) a Turing Machine -- a simple form of computer, but not a computer that you would ever power up -- a Turing Machine is strictly a theoretical device (http://en.wikipedia.org/wiki/Turing_machine).

The reason for the bias of starting with as unstructured and primitive as programs as possible is that though there are optimizations in the test for primality, for example, which I could reflect in my initial programs, these optimizations reflect patterns that almost certainly have been exploited in explorations of Goldbach’s conjecture by better minds than mine. It may be that any proof, if one is possible, has to rely on reasoning that is just off (human-conceived) map.

I'd actually started this process as a grad, exploring the ways to bridge these two programs, via an AI program that searched through billions of possible rewrites. I'm essentially an experimentalist and I start with code and looking for data -- that's my bread and butter. I think that what I am really doing is shaping my retirement 20 years from now (or less, for Pete's sake). When friends visit and ask Pat where I am, she'll point to the shed and tell them that I'm working on "that proof". More likely, I’ll be tinkering with the AI program itself, making sure that there are no bugs in it — can you imagine my despair, if near the end of my life and after searching billions of rewrites, my program comes back with “Proof Found!”, and I didn’t correctly save the path my AI program took to get there!?

The older I get the more I remind myself of my father.

(originally posted Thursday, August 20, 2009 on Wordpress)