Wiskundemeisjes

QED per pc

Voor het februarinummer van Natuurwetenschap & Techniek schreef ik een artikel over (computer)bewijzen. Het tijdschrift ligt nu in de winkel! Voor wie het al heeft gekocht: er is door een technische fout een kolom weggevallen, die is hier te lezen.

Russell O'Connor van de Radboud Universiteit Nijmegen maakte speciaal voor dat artikel een nieuw formeel bewijs van de oude stelling dat er oneindig veel priemgetallen zijn (het klassieke bewijs van Euclides is her en der te vinden op internet). Dit bewijs heeft hij geverifieerd met Coq, een bewijsassistent. O’Connors bewijs was jammer genoeg te moeilijk voor de gemiddelde lezer, maar het komt wel op de site van het blad. En ik mocht dit stuk tekst ook op de wiskundemeisjes plaatsen! Het bewijs van O' Connor biedt namelijk een interessant inkijkje in het formalisme van het computer-gegenereerde bewijs – en in de logica van Coq. Het ziet er zo uit:

***
Theorem NotFinitePrimes : forall l:list nat, ~(forall x, Prime x <-> In x l).
Proof.
intros l H.
cut (Prime 1).
unfold Prime; auto with *.
assert (H':=fun x => (proj1 (H x))).
assert (H0:Prime (product l + 1)).
apply primepropdiv.
firstorder using plus_lt_compat_r ZeroProduct.
intros q Hq H0.
replace q with 1 in Hq by eauto with *.
firstorder.
replace 1 with (product l + 1); eauto with *.
Qed.
***

Zo'n bewijs is voor mensen nauwelijks te lezen en ook de lijn die het bewijs volgt is heel anders dan de redenering van Euclides. In dit formele bewijs wordt bewezen dat als er een eindige lijst met precies alle priemgetallen bestaat, dat het getal 1 dan een priemgetal moet zijn. Omdat 1 geen priemgetal is, kan die eindige lijst met alle priemgetallen niet bestaan. Er zijn dus oneindig veel priemgetallen. Qed: quod erat demonstrandum, ofwel "hetgeen bewezen moest worden."

Als je het bewijs in Coq draait, dan gaat het bewijs door verschillende toestanden. Aan het begin is de toestand:

***
1 subgoal
============================
forall l : list nat, ~ (forall x : nat, Prime x <-> In x l)
***
(Er is één doel, namelijk bewijzen dat er geen eindige lijst met alle priemgetallen bestaat.)

Aan het eind is de toestand:

***
Proof completed.
***
(Het bewijs is klaar en correct bevonden.)

Het programma verandert de toestand na elke stap. Neem bijvoorbeeld de stap "apply primepropdiv" in het bewijs. Daar wordt het volgende lemma gebruikt

***
primepropdiv
: forall n : nat,
n > 1 ->
(forall q : nat, Prime q -> Divides q n -> q * q > n) -> Prime n
***
(Laat n een positief geheel getal zijn dat groter is dan 1. Als elk priemgetal q dat n deelt groter is dan wortel(n), dan is n een priemgetal.)

Voor deze stap staat dit doel in de toestand van het bewijs:
***
subgoal 1 is:
l : list nat
H : forall x : nat, Prime x <-> In x l
H' : forall x : nat, Prime x -> In x l
============================
Prime (product l + 1)
***

Na deze stap is dit doel veranderd in:
***
subgoal 1 is:

l : list nat
H : forall x : nat, Prime x <-> In x l
H' : forall x : nat, Prime x -> In x l
============================
product l + 1 > 1

subgoal 2 is:
forall q : nat,
Prime q -> Divides q (product l + 1) -> q * q > product l + 1
***
Wat is er gebeurd in deze stap? Eerst was het doel om te bewijzen dat product l + 1 een priemgetal is. Na toepassing van het lemma zijn er twee doelen: laten zien dat product l + 1 groter is dan 1 en laten zien dat elke deler van product l + 1 groter is dan wortel(product l + 1 ). Het lemma zegt immers dat deze twee doelen samen betekenen dat product l + 1 een priemgetal is. Coq houdt zo steeds bij wat er nodig is om de bewering te bewijzen.

Met dank aan Freek Wiedijk voor de uitleg van Coq.