A famous unsolved question, tested on numbers up to 33 million.
goldbach.pl · output · proof · check · try it in the playground
A prime is a whole number greater than 1 that only 1 and itself divide: 2, 3, 5, 7, 11, …
In 1742 Christian Goldbach guessed that every even number greater than 2 is the sum of two primes: 8 = 3 + 5, 16 = 3 + 13. Nobody has proved it yet, but nobody has found an exception either.
This example tests it on every power of two from 4 to 2²⁵ = 33,554,432, and for each one finds the split whose smaller prime is as small as possible.
split(4, [2, 2]).
split(N, Pair) :- 0 =:= N rem 2, N > 4, once(split_from(N, Pair, 3)).
split_from(N, [P, Q], P) :- Q is N-P, is_prime(Q).
split_from(N, Pair, P) :- P < N, once(next_prime(P, Next)), split_from(N, Pair, Next).
In words: start with the prime P = 3. If N − P is prime, that is the split.
If not, move on to the next prime and try again. once means: take the
first split found and stop.
is_prime(2).
is_prime(3).
is_prime(P) :- P > 3, 1 =:= P rem 2, \+ has_factor(P, 3).
has_factor(N, L) :- 0 =:= N rem L.
has_factor(N, L) :- L*L < N, M is L+2, has_factor(N, M).
This is trial division: an odd number is prime if none of 3, 5, 7, …
(up to its square root) divides it. \+ means “not”: it succeeds when
the search for a factor finds nothing.
goldbach(4, [2, 2]).
goldbach(8, [3, 5]).
goldbach(16, [3, 13]).
goldbach(128, [19, 109]).
goldbach(8388608, [37, 8388571]).
goldbach(33554432, [61, 33554371]).
% … 24 lines in all, one per power of two
Every power of two in the range splits into two primes, as Goldbach predicted. (Testing cases is not a proof of the conjecture, of course.)
Take 8 = 2³:
Larger numbers follow the same pattern, sometimes after stepping through several primes P before N − P turns out to be prime.
once steps checked by the step
they rest on.absent obligation like
\+ has_factor(5, 3): “this number has no factor starting from 3”.An absence is Eyedia saying “I searched everything the program allows and found nothing”. A proof can show a factor exists, but it cannot show one doesn’t; so the checker records each of these instead of proving it.
The checker tries to refute each trusted absence: it looks for evidence in the program or the proof that a factor was found after all. All 35 hold up.
Verdict: checked_with_obligations — valid, provided those 35 “no factor found” searches were complete.
Want zero trust? --strict-proof rejects any proof that leans on such an
obligation.
node bin/eyedia.js examples/goldbach.pl # the splits
node bin/eyedia.js --check-proof examples/proof/goldbach.pl examples/goldbach.pl # the report
Or open it in the playground.
Change in_range(2, 25, I) to in_range(2, 26, I) and run again: one more
line appears, goldbach(67108864, [5, 67108859]).
Even a search for “no factor” is made visible: the proof shows every split it found, and the report is honest about the 35 places where it relies on “searched and found nothing”.