Euclides

Oneindig veel priemgetallen

Priemgetallen zijn natuurlijke getallen groter dan 1, die door slechts twee getallen deelbaar zijn (1 en zichzelf). Er is geen grootste priemgetal. Dit werd al bewezen door Euclides, die 300 jaar voor Christus leefde; in het kader kun je de letterlijke vertaling van zijn bewijs lezen. Tegenwoordig wordt het bewijs vaak op de volgende manier gepresenteerd.

Stelling (Euclides). Er zijn oneindig veel priemgetallen: voor ieder getal n bestaat er een priemgetal p dat groter is dan n.

Bewijs. Neem een natuurlijk getal n. Beschouw het getal k = n! + 1 (waarbij n! = 1 × 2 × 3 × ... × n). Kies een priemgetal p dat k deelt. Dan is p > n. Want als p kleiner dan of gelijk aan n zou zijn, dan zou p een deler zijn van n!, en dus niet van k = n! + 1. Maar we hadden p juist als deler van k gekozen. QED

Dit bewijs kan in deze vorm niet door een computer worden begrepen. Het is geschreven in mensentaal en daardoor zijn de stapjes in het bewijs te vaag. Hier is de Mizar versie, die wel begrijpelijk is voor een computer:

theorem Euclides: for n ex p st p is prime & p > n

proof

let n;
set k = n! + 1;
n! > 0 by NEWTON:23;
then n! >= 0 + 1 by NAT_1:38;
then k >= 1 + 1 by REAL_1:55;
then consider p such that
A1: p is prime & p divides k by INT_2:48;
A2: p <> 0 & p > 1 by A1,INT_2:def 5;
take p;
thus p is prime by A1;
assume p <= n;
then p divides n! by A2,NAT_LAT:16;
then p divides 1 by A1,NAT_1:57;
hence contradiction by A2,NAT_1:54;
end;

Zoals je ziet, lijkt dit erg op een computerprogramma. Het formaliseren van een bewijs lijkt dan ook erg op programmeren. In feite combineert formaliseren het leukste van programmeren en van wiskunde. (Sommige bewijssystemen zijn hierdoor bijna een soort computerspel: de te bewijzen stelling is dan het 'level' dat je aan het spelen bent.)