Wiskundemeisjes

Ionica & Jeanine
 
Slik Internetbureau Rotterdam Internetbureau Rotterdam



  • Laatste Reacties

Categorieën

Archief

QED per pc


In Leestip, door Ionica

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.

Coq

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.
***

Coq

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.

5 reacties op “QED per pc”

  1. Vincent:

    Ik heb wat moeite het bewijs te volgen. Kan iemand het vertalen naar huis-, tuin- en keukenwiskunde?

  2. Ionica:

    Freek Wiedijk mailde in de voorbereiding van het artikel de volgende uitleg:

    The proof works as follows:

    - we work towards a contradiction by showing that from the assumption that we have a list holding precisely the primes it follows that 1 is prime; once we have that we're done, as clearly 1 is not a prime

    - actually, it is sufficient that this list holds all the primes (so there also might be non-primes in it); this is the "assert (X:=...)" step in the proof script

    - as a first step we are going to show that the product of this list plus 1 is prime

    - for this it is sufficient that any prime q that divides this product plus 1 has a square that is bigger than that product plus 1

    - we do this by contradiction by showing that such a q has to be 1, so cannot be prime after all

    - Coq shows that this q is 1 by the magic of "eauto with *"; when you investigate how this works, it turns out that it shows that q divides 1; that is the case because it divides the product of the list (it being a prime) as well as that product plus 1 (that was how q was chosen)

    - so now we know that the product of the list plus 1 is prime; from this we then deduce that 1 is prime (our goal) by showing that that product plus 1 actually is 1. Again that happens by showing that it divides 1, by showing that it both divides the product of the list (it having shown to be prime) as well as the product of the list plus 1 (because that is itself).

    - so now we have that 1 is prime, the contradiction that we were looking for, and we're done

  3. Johan B.:

    In hoeverre wordt er eigenlijk gewerkt aan de computerverificatie van grote bewijzen, zoals de classificatie van eindige simpele groepen?

  4. Rinse Poortinga:

    Dat er oneindig veel priemgetallen zijn, is allang bewezen. Ik ben meer geïnteresseerd in een computerprogramma waar ik zelf een stelling kan invoeren, waarna het programma een bewijs van de stelling levert of het tegendeel bewijst. Nog interessanter is natuurlijk een programma dat zelf stellingen formuleert en bewijst. Kortom: ik heb niet zo'n hoge pet op van dit soort programma's en zou daar geen energie in steken.

  5. Lieven:

    @Rinse:

    zo'n programma's bestaan ook al een hele tijd. Graffiti http://math.uh.edu/~clarson/graffiti.html heeft een hele boel leuke conjectures in de grafentheorie ontdekt.

    @Johan:

    zo'n grote bewijzen zijn nog heel ver boven de capaciteit van de huidige systemen. Het was een hele verwezenlijking toen het Mizar project, dat de bedoeling heeft op termijn om de gehele wiskunde in hun systeem te krijgen, een paar jaar geleden erin slaagde om de Jordan curve stelling te bewijzen.

Plaats een reactie


Je kunt LaTeX gebruiken in je reactie.
Gelieve antwoorden op puzzels tussen [SPOILER] en [/SPOILER] te plaatsen.