de kunst van het bewijzen

Freek Wiedijk & Herman Geuvers Radboud Universiteit Nijmegen & Technische Universiteit Eindhoven

Vakantiecursus wiskunde 2008

Technische Universiteit Eindhoven 2008 08 23, 14: 15

Centrum voor Wiskunde en Informatica, Amsterdam 2008 08 29, 18: 30

lagere en hogere wiskunde

de twee soorten wiskunde

• berekenen bij berekenen gaat het om de uitkomst

wat?

• bewijzen bij bewijzen gaat het om het begrip

waarom? het diagonaal van een vierkant

[figure]

• berekenen: wat is de verhouding tussen de zijde en de diagonaal?

Pythagoras: 1 : \sqrt{2} = 1 : 1,4142135623 …

• bewijzen: is dit als een verhouding van gehele getallen te schrijven?

Pythagoras: niet mogelijk, want …

computerwiskunde

vier soorten

• berekenen: getallen numerieke wiskunde, visualisatie, experimentatie

• berekenen: formules computer algebra

• bewijzen: door de computer automatische stellingenbewijzers

• bewijzen: door de mens, met behulp van de computer bewijsassistenten numerieke wiskunde: de Mandelbrot-verzameling

z_{0} = 0, z_{1} = z_{0}^{2} + c, z_{2} = z_{1}^{2} + c, …
{c ∈ ℂ | de rij z_{i} gaat niet naar ∞}

hoe belangrijk is het dat iedere pixel in dit plaatje correct is? numerieke wiskunde: het Mertens-vermoeden 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} ?

numerieke wiskunde: het Mertens-vermoeden (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… …

6

computer algebra: een integraal uitrekenen Matlab, Mathematica, Maple, Magma

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

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

   > value(%);

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

   > evalf(%);

−1.644934068
correcte uitkomst:  −1.6449340668482264…

automatische stellingenbewijzers: de systemen

TPTP Thousands of Problems for Theorem Provers 7068 problemen

CASC CADE ATP System Competition Conference on Automated Deduction, Automated Theorem Prover

winnaar 2008: Vampire 169 van de 200 problemen opgelost

tweede 2008: E 164 van de 200 problemen opgelost

Otter ≈ Prover9 automatische stellingenbewijzers: het Robbins-vermoeden

is iedere Robbins algebra een Boolse algebra?

a ∨ b = b ∨ a
a ∨ (b ∨ c) = (a ∨ b) ∨ c
¬(¬(a ∨ b) ∨ ¬(a ∨ ¬b)) = a

Bill McCune + EQP, 1996: inderdaad! 8 dagen computertijd bewijs van 34 regels

automatische stellingenbewijzers kunnen tot nog toe:

• ‘puzzels’ waarin heel veel gevallen moeten worden onderzocht

• elementaire stapjes in een bewijs bewijsassistenten

• numerieke wiskunde en computer algebra: geen bewijzen • automatische stellingenbewijzers: geen interessante wiskunde • bewijsassistenten: wél bewijzen & wél interessante wiskunde

de prijs die moet worden betaald: gebruiker moet veel zelf doen bewijsassistenten = interactieve stellingenbewijzers samenspel van mens en computer

vier bewijsassistenten

100 leuke stellingen, 80 geformaliseerd

1. The Irrationality of the Square Root of 2  ≥ 17
2. Fundamental Theorem of Algebra  4
3. The Denumerability of the Rational Numbers  6
4. Pythagorean Theorem  6
5. Prime Number Theorem  2
6. Gödel’s Incompleteness Theorem  3
7. Law of Quadratic Reciprocity  4
8. The Impossibility of Trisecting the Angle and Doubling the Cube  1
9. The Area of a Circle  1
10. Euler’s Generalization of Fermat’s Little Theorem  4
11. The Infinitude of Primes  6
12. The Independence of the Parallel Postulate  0
13. Polyhedron Formula  1

… google: 100 theorems

de beste bewijsassistenten vijf systemen serieus gebruikt voor wiskunde:

HOL {  HOL Light  69
ProofPower  42
Isabelle  40
Coq  39
Mizar  45

HOL Light

in lange traditie: LCF → HOL → HOL Light Stanford, US → Cambridge, UK → Portland, US

John Harrison

bewijst floating point hardware correct bij Intel formaliseert wiskunde in zijn vrije tijd

bijzonder elegant systeem makkelijk uit te breiden niet gebruikersvriendelijk Isabelle

soort ‘opvolger’ van HOL

samenwerking tussen twee universiteiten: Cambridge, UK vooral: computerveiligheid München, Duitsland vooral: wiskunde

gebalanceerd systeem mooie bewijstaal krachtige automatisering Coq

INRIA en Microsoft Institut National de Recherche en Informatique et en Automatique

systeem met de indrukwekkendste formalisatie tot nu toe systeem dat wij in Nijmegen gebruiken

geïntegreerde programmeertaal ≈ Haskell

wiskundige expressief

intuïtionistisch intuïtionistische wiskunde

Luitzen Egbertus Jan Brouwer pionier van de topologie

proefschrift, 1907 Over de grondslagen van de wiskunde

niet valide om over een reëel getal x te redeneren ‘óf x is nul, óf x is ongelijk aan nul’

‘uitgesloten derde’

tussenwaardestelling intuïtionistisch niet bewijsbaar Mizar

Andrzej Trybulec Białystok, Polen

ook: Nagano, Japan

wiskundigste van de bewijsassistenten

grootste bibliotheek met geformaliseerde wiskunde 2,1 miljoen regels code

gebruikersvriendelijk soms moeilijk te begrijpen

geformaliseerde stellingen

de hoofdstelling van de algebra

Carl Friedrich Gauss, 1799 Mizar: Robert Milewski, 2000 HOL Light: John Harrison, 2000 Hellmut Kneser, 1940 Coq: Herman Geuvers e.a., 2000

x^{2} = −1 ?

x = i = \sqrt{−1}

welke polynomiale vergelijkingen kunnen we nu oplossen?

x^{2} = i ?

de priemgetalstelling

Paul Erdös en Atle Selberg, 1949 Isabelle: Jeremy Avigad, 2004 Jacques Hadamard, Charles Jean de la Vallée-Poussin, 1896 HOL Light: John Harrison, 2008

aantal priemgetallen ≤ gegeven getal:

π(1000000000000) = 37607912018
\frac{1000000000000}{ln(1000000000000)} = 36191206825,27…
∫_{2}^{1000000000000} \frac{dx}{ln(x)} = 37607950279,75…

wat is de verhouding in de limiet van het aantal getallen naar ∞? de stelling over Jordan-krommen

Oswald Veblen, 1905 HOL Light: Tom Hales, 2005 Mizar: Artur Korniłowicz e.a., 2005

Jordan-krommen geen Jordan-krommen

in hoeveel stukken verdeelt een Jordan-kromme het platte vlak? de eerste onvolledigheidsstelling

Kurt Gödel, 1931 Boyer-Moore prover: Natarajan Shankar, 1986 Coq: Russell O’Connor, 2003 HOL Light: John Harrison, 2005

de Gödel-zin:

‘deze zin is niet bewijsbaar’

als deze zin waar is, zijn er onbewijsbare ware zinnen (onvolledigheid) als deze zin onwaar is, zijn er bewijsbare onware zinnen (inconsistentie)

is er een bewijssysteem waarin waarheid en bewijsbaarheid samenvalt? de vierkleurenstelling

Kenneth Appel en Wolfgang Haken, 1976 Neil Robertson e.a., 1996 Coq: Georges Gonthier, 2004

kan iedere kaart met maar vier verschillende kleuren worden gekleurd?

zelf formaliseren?

wetenschappelijk onderzoek

tijd voor het formaliseren van om één bladzijde uit een leerboek: één volle werkweek ≈ 40 uur

lengte van een formalisatie van één bladzijde uit een leerboek: een aantal computerschermen vol ≈ 200 regels

≈ een kwartier per regel moeilijk!

toch proberen Mizar te leren?

writing a Mizar article in nine easy steps

http://www.cs.ru.nl/~freek/mizar/mizman.pdf

bewijzen Marjolein Kool

Een bolleboos riep laatst met zwier theorem gewapend met een vel A-vijf: not ex n st for m holds n >= m Er is geen allergrootst getal, proof dat is wat ik bewijzen ga. Stel, dat ik u nu zou bedriegen assume not thesis; en hier een potje stond te jokken, then consider n such that dan ik zou zonder overdrijven let n; A1: for m holds n >= m; het grootste kunnen op gaan noemen. Maar ben ik klaar, roept u gemeen: set n' = n + 2; ‘Vermeerder dat getal met twee!’ En zien we zeker en gewis

n + 2 > n by XREAL_1:31; n' > n;by XREAL_1:31; dat dit toch niet het grootste was.

*4 En gaan we zo nog door een poos, then not for m holds n >= m; dan merkt u: dit is onbegrensd. En daarmee heb ik q.e.d.

hence thesis; hence contradiction;by A1; Ik ben hier diep gelukkig door.

*1 ‘Zo gaan’, zei hij voor hij bezwijmde, end; ‘bewijzen uit het ongedichte’.

Pythagoreïsche drietallen: een formule

[figure: b; a; c]

een oplossing van

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

zonder gemeenschappelijke delers is altijd van de vorm:

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

voorbeelden

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}
↛  9^{2} + 12^{2} = 15^{2}

Pythagoreïsche drietallen: ‘formal proof sketch’

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 (c + a)/2 = m^2 & (c - a)/2 = n^2;
  take m,n;

Pythagoreïsche drietallen: ‘formal proof sketch’ (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;

syntactisch correct semantisch correct te kort door de bocht

stappen te groot relaties tussen de stappen niet expliciet Pythagoreïsche drietallen: fragment van de uitgewerkte formalisatie

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;

een zeer korte geschiedenis van de wiskunde

de drie revoluties

Euclid bewijzen  Cauchy rigoreus  de Bruijn formeel