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)
