bewijzen in de computer

Freek Wiedijk Radboud Universiteit Nijmegen Katholieke Universiteit Nijmegen

Nationale Wiskunde Dagen Noordwijkerhout 2004 02 06, 16:15 principia mathematica wiskunde in volledig detail in een formele taal

Leibniz, eind 17de eeuw

uitvinder van differentiëren en integreren

bouwer van één van de eerste rekenmachines: ×, ÷, √

lingua characteristica universalis (universele taal) calculus ratiocinator

Boole, The Calculus of Logic, 1848 Frege, Begriffsschrift, 1879 Peano, tijdschrift Rivista di Matematica, 1891-1906 Russell & Whitehead, Principia Mathematica

drie delen: 1910, 1912, 1913 automath

computer → bewijzen in volledig detail uitwerken wordt praktisch

eerste ter wereld: de Bruijn, Eindhoven

‘de automath’ = computer om wiskunde mee te controleren
automath = taal om wiskunde in op te schrijven

1968: eerste ideeën jaren zeventig: groot onderzoeksproject

Jutting, 1977: vertaling van een heel wiskundeboek

dik pak computertekst

controle op correctheid: paar uur computertijd (tegenwoordig: een halve seconde)

wiskunde in de computer

berekenen en bewijzen de twee activiteiten van de wiskundige

• berekenen het gaat om het antwoord: wat?

• bewijzen het gaat om het begrip: waarom? is bewijzen nog wel van deze tijd? middelbaar onderwijs: bewijzen wordt nauwelijks meer onderwezen

• er is geen grootste priemgetal

• decimalen van

\sqrt{2} = 1.41421356237309504880168872420969807856967187537694807317…

herhalen niet

• er zijn meer reële getallen dan natuurlijke getallen

• er zijn evenveel punten in een lijn als punten in het vlak universitair onderzoek: computer-experimenten steeds belangrijker

… nemen de plaats van bewijzen over? bewijzen spelen tegenwoordig een rol in de informatica kritische hardware/software mag geen ‘bugs’ hebben wiskunde in de computer

• numeriek berekeningen getallen: computer → mens

• computer algebra berekeningen formules: computer → mens

• stellingenbewijzers bewijzen: computer → mens

• bewijscheckers

bewijzen: mens → computer (computer kijkt alleen of het klopt)

numeriek

het vermoeden van Mertens Möbius functie:

μ(n) = \{ \begin{matrix}0 & als n dubbele priemfactoren heeft \\ 1 & als n een even aantal verschillende priemfactoren heeft \\ −1 & als n een oneven aantal verschillende priemfactoren heeft \end{matrix}

Mertens, 1897:  | ∑_{k=1}^{n} μ(n)| < \sqrt{n} ?

het vermoeden van Mertens (vervolg)

Odlyzko & te Riele, 1985: vermoeden van Mertens is niet waar ! 50 uur computertijd

eerste n waar het mis gaat heeft tientallen cijfers indirect bewijs !

2000 nulpunten van Riemann zeta functie op 100 decimalen nauwkeurig

14.1347251417346937904572519835624702707842571156992431756855674601499634298092567649490103931715610127… 21.0220396387715549926284795938969027773343405249027817546295204035875985860688907997136585141801514195… 25.0108575801456887632137909925628218186595496725579966724965420067450920984416442778402382245580624407… 30.4248761258595132103118975305840913201815600237154401809621460369933293893332779202905842939020891106… 32.9350615877391896906623689640749034888127156035170390092800034407848156086305510059388484961353487245… 37.5861781588256712572177634807053328214055973508307932183330011136221490896185372647303291049458238034… 40.9187190121474951873981269146332543957261659627772795361613036672532805287200712829960037198895468755… 43.3270732809149995194961221654068057826456683718368714468788936855210883223050536264563493710631909335… 48.0051508811671597279424727494275160416868440011444251177753125198140902164163082813303353723054009977… 49.7738324776723021819167846785637240577231782996766621007819557504335116115157392787327075074009313300… 52.9703214777144606441472966088809900638250178888212247799007481403175649503041880541375878270943992988… 56.4462476970633948043677594767061275527822644717166318454509698439584752802745056669030113142748523874… 59.3470440026023530796536486749922190310987728064666696981224517547468001526996298118381024870746335484… 60.8317785246098098442599018245240038029100904512191782571013488248084936672949205384308416703943433565… 65.1125440480816066608750542531837050293481492951667224059665010866753432326686853844167747844386594714… 67.0798105294941737144788288965222167701071449517455588741966695516949012189561969835302939750858330343… 69.5464017111739792529268575265547384430124742096025101573245399996633876722749104195333449331783403563… 72.0671576744819075825221079698261683904809066214566970866833061514884073723996083483635253304121745329… 75.7046906990839331683269167620303459228119035306974003016477753015741970277063236083840370218346527980… 77.1448400688748053726826648563046370157960324492344610417652314531511391642537150894082886946997377597… 79.3373750202493679227635928771162281906132467431200308784387204971015419326770909746774519946121241090… 82.9103808540860301831648374947706094975088805937821491465713062832359290863566190755125631923348968187… …

7

computer algebra

symbolische integratie

> Int(ln(x)/(1 - x),x = 0..1);

∫_{0}^{1} \frac{ln x}{1 − x} dx

> value(%);

−\frac{π^{2}}{6}

het algoritme van Risch

integraal uitdrukken in ‘elementaire functies’ √, ln, e^{x}, sin, arcsin, … – zegt of het kan

– geeft het antwoord als het kan mathXpert populaire computer algebra systemen

• maple

• mathematica computer algebra voor het onderwijs

• mathXpert Beeson, 1997 niet heel krachtig wel heel duidelijk

– formules zien er uit als in de leerboekjes

– niet alleen de antwoorden maar ook de berekeningen

automatische stellingenbewijzers

het vermoeden van Robbins

computers … kunnen binnenkort beter schaken dan mensen … kunnen binnenkort beter bewijzen dan mensen?

Robbins, 1933: is iedere Robbins algebra een Boole algebra?
eqp, 1996: ja !

acht dagen computertijd

één van de weinige bewijzen het eerst gevonden door een computer niet erg conceptueel: probeert gewoon heel veel mogelijkheden

interessant onderzoek, maar momenteel niet relevant voor de wiskunde

bewijscheckers

de pentium bug pentium: intel processor midden 1994: processor maakt rekenfouten FDIV bug, niet genoeg precisie \frac{5505001}{294911} = 18.66665197… (wiskunde) \frac{5505001}{294911} = 18.66600093… (pentium) pentium processor met bug wordt gratis vervangen schatting schade: 475 miljoen dollar Harrison: werkt voor intel bewijst full time met de HOL bewijschecker micro programma’s correct de metro en de B methode

1998: metro zonder bestuurder météor = métro est-ouest rapide

lijn 14 van de metro in Parijs madeleine ↔ bibliothèque nationale

systeem voor de besturing sacem = système d’aide à la conduite, à l’exploitation et à la maintenance

geprogrammeerd in de programmeertaal ada

veiligheid van sacem bewezen met de B methode commerciële bewijschecker het vermoeden van Kepler

Kepler in strena sue de nive sexangula, 1661:

is de sinaasappelstapeling de efficientste manier om bollen op te stapelen?

Hales, 1998: ja !

bewijs: bevat groot en onbegrijpelijk programma bekijkt heel veel gevallen 3 gigabytes programma’s/data + paar maanden computertijd

referees zeggen 99% zeker te zijn dat het klopt

flyspeck project ‘formal proof of Kepler’ mizar

bewijschecker uit Polen

Trybulec 1973: eerste ideeën vandaag: grootste wiskunde bewijscheck project ter wereld

anderhalf miljoen regels gecodeerde wiskunde achthonderd artikelen

gebaseerd op de axiomatische verzamelingenleer wiskundige & leesbare bewijstaal hyperproof

bewijschecken in de informatica bewijschecken in de wiskunde bewijschecken in het onderwijs

eerste orde predicatenlogica

Barwise & Etchemendy, 1994: hyperproof

eenvoudige redeneringen over een eenvoudige blokkenwereld draait momenteel alleen op apple macintosh computers

redeneren in een diagram

voorbeeld van een checkbaar bewijs

Pythagoreïsche tripels een oplossing van

a^{2} + b^{2} = c^{2}

met a, b en c geen gemeenschappelijke delers, is altijd van de vorm

a = m^{2} − n^{2} b = 2mn c = m^{2} + n^{2}

voorbeelden

\begin{aligned}m = 2  n = 1 & → & 3^{2} & + & 4^{2} & = & 5^{2} \\ m = 3  n = 2 & → & 5^{2} & + & 12^{2} & = & 13^{2} \\ m = 4  n = 1 & → & 15^{2} & + & 8^{2} & = & 17^{2} \\ m = 4  n = 3 & → & 7^{2} & + & 24^{2} & = & 25^{2} \end{aligned}

mizar bewijs

reserve a,b,c,m,n for Nat;
let a,b,c; assume a^2 + b^2 = c^2;
assume a,b are_relative_prime;
then a is odd or b is odd; assume a is odd;
ex m,n st a = m^2 - n^2 & b = 2*m*n & c = m^2 + n^2
proof
 b is even; c is odd;
X: (c + a)/2,(c - a)/2 are_relative_prime;
 ((c + a)/2)*((c - a)/2) = (c^2 - a^2)/4 .= (b/2)^2;
 then ((c + a)/2)*((c - a)/2) is square;
 then (c + a)/2 is square & (c - a)/2 is square by X;
 consider m,n such that m^2 = (c + a)/2 & n^2 = (c - a)/2;
 take m,n;

mizar bewijs (vervolg)

consider m,n such that m^2 = (c + a)/2 & n^2 = (c - a)/2;
take m,n;
thus a = (c + a)/2 - (c - a)/2 .= m^2 - n^2;
b^2 = (c + a)*(c - a) .= 4*m^2*n^2 .= (2*m*n)^2;
hence b = 2*m*n;
thus c = (c + a)/2 + (c - a)/2 .= m^2 + n^2;
end;

dit is bijna het echte mizar bewijs, maar te kort door de bocht

• stappen zijn te groot

• verwijzingen tussen stappen ontbreken het volledige bewijs (fragment)

then
X: (c + a)/2,(c - a)/2 are_relative_prime by Lm3;
((c + a)/2)*((c - a)/2) = ((c + a)*(c - a))/(2*2)
  by REAL_1:35
 .= (c^2 - a^2)/4 by SQUARE_1:67
 .= (b^2)/(2*2) by H1,INT_1:3
 .= (b^2)/(2^2) by SQUARE_1:def 3
 .= (b/2)^2 by SQUARE_1:69;
then ((c + a)/2)*((c - a)/2) is square by A1,Def1;
then (c + a)/2 is square & (c - a)/2 is square by X,Lm4;
then (ex m st m^2 = (c + a)/2) &
 (ex n st n^2 = (c - a)/2) by Def1;
then consider m,n such that
A9: m^2 = (c + a)/2 & n^2 = (c - a)/2;

waarom proofchecken?

wordt wiskunde nu eindelijk echt wiskunde?

• bugs in de checker, kapotte hardware

(in de praktijk geen probleem) de Bruijn kriterium: eenvoudige checker

• definiëren je definities wel wat je denkt dat ze definiëren?

QED 1994, anonieme groep wiskundigen & informatici:

laten we alle wiskunde in de computer stoppen !

erg interessant QED manifesto antwoorden op twaalf mogelijke tegenwerpingen

tot nog toe nog een utopie het leukste computerspel ter wereld

wiskunde: spannend
programmeren: spannend
bewijzen in de computer: het beste van twee werelden

je hoeft niet alleen op je begrip te vertrouwen → de computer helpt ! je weet zeker dat wat je doet helemaal goed is → geen ‘bugs’ !

een stelling die nog niet helemaal bewezen is = een ‘level’ van een computerspel dat nog niet is uitgespeeld