Goldbach's conjecture says that every positive even number greater than 2 is the sum of two prime numbers. Example: 28 = 5 + 23. It is one of the most famous facts in number theory that has not been proved to be correct in the general case. It has been numerically confirmed up to very large numbers. Write a predicate to find the two prime numbers that sum up to a given even integer.

### Test/Example

(deftest p40-goldbach
(is (= [5 23] (goldbach 28))))
(def even-nats-greater-two (gen/such-that #(< 2 %) (gen/fmap #(* 2 %) gen/nat)))
(defspec goldbach-conjecture
100
(prop/for-all [i even-nats-greater-two]
(let [res (goldbach i)]
(and
(= 2 (count res))
(every? prime? res)
(= i (reduce + res))))))

### Discussion

A naive approach just looks at all prime numbers below the input value. We are then only interested in those primes that if subtracted from that input leave us with another prime number. Both numbers obtained by that method form the result. We already got a list of prime numbers, Clojure's take-while and filter do the rest. I expressed the fact that Goldbach's conjecture is only defined for even natural numbers greater than two with a precondition.

If you have been following this series you might have noticed that the example I give in the blog posts is almost always a unit test. I think this a quite succinct way to illustrate the intended behaviour of a function. But this time you will have noticed that there is something else.

I have added a dependency to clojure.test.check. Test.check is a QuickCheck inspired property-based testing library for Clojure. You can learn more about QuickCheck by having a look at the original paper.

Looking at the code above you will notice that a generative test consists of two parts. First a property (within the defspec). In this case I specified that for all even natural numbers greater than two the Goldbach function should return two prime numbers whose sum is equal to the input value. This property is an almost literal translation of Goldbach's conjecture.

Secondly you need to specify how to generate all possible input values that the test runner should use. Again: Instead of doing this explicitly for every single input value, as you would have to in a traditional exemplary unit test, you just define a generator. I used the built-in generator for natural numbers called nat. But in order to create only valid input values for the Goldbach function the generated values need to be greater than two and even. You can achieve this by using combinators on the original generator. A fmap * 2 shifts the domain of the generator into the even values. I then used the such-that combinator to filter out everything below two.

While writing these generative tests seems like more work at first sight you get back a more thorough verification of your program in return.

Property-based testing recognises the impossibility of coming up with test inputs that expose all edge cases. Instead it encourages you to define properties of your function that you expect to hold. The flip side of the coin is that property based tests won't contribute as much to the design of your APIs and your system as the traditional TDD approach did. But it is a very valuable attempt at automated verification.

Read more about this series.