Bevisets stilling

Et godt bevis skal kunne overbevise andre.
Et godt bevis skal kunne overbevise andre.

Når jeg underviser, skal de studerende lave opgaver, hvor de skal udføre matematiske ræsonnementer. For de allerfleste er det første gang, de selv skal prøve at konstruere og skrive et matematisk bevis, og de allerfleste er meget usikre på hvordan man gør. Er det, vi har skrevet, godt nok? spørger de mig. Faktisk rører de ved noget helt centralt, nemlig hvad et matematisk bevis er og hvilken rolle det har.

Leslie Lamport skriver i sin artikel How To Write A 21st Century Proof om hvordan man kan lave bedre matematiske beviser. Han skelner mellem beviser i det 21. århundrede og beviser i stilen fra det 17. århundrede, hvor sidstnævnte beviser simpelthen er “prosa med  formler”.  Lamports påstand er dels at mange matematiske beviser stadig lever i det 17. århundrede, dels at der er mange ukorrekte beviser i den matematiske litteratur.

Formodentlig har han ret i begge påstande. Der er masser af beviser i artikler og bøger, som er sværere at forstå end de burde være. Typisk har beviserne en uklar struktur. Jeg har selv begået sådanne beviser, og min fornemmelse er at vi skriver rodede beviser fordi vi først og fremmest skriver beviserne til os selv.

Når vi bevæger os uden for den del af matematisk logik, der hedder bevisteori (et område, jeg selv har haft en del kontakt med, men ikke kan påstå at kende godt), er der ikke nogen klare kriterier for hvad et korrekt bevis egentlig er.

Et klart og samtidig uformelt krav er at et matematisk bevis skal overbevise læseren. Netop derfor må beviset ikke være “privat”; amatører udi matematikken har gennem årene forsøgt at løse åbne problemer, og deres “beviser” har altid overbevist dem selv – og oftest kun dem selv.

Derfor siger jeg ofte til de studerende, der spørger mig, at et godt bevis er et, der kan læses og accepteres af en anden. Denne anden  kan enten være en anden studerende eller den studerende selv, der genlæser beviset på et senere tidspunkt.

Men jeg prøver også at gøre det klart for studerende, at et bevis ikke er “magi”. Mange tror at et bevis er udtryk for en særlig og genial indsigt. Sådan er det selvfølgelig af og til, men  i mange områder af teoretisk datalogi, som studerende møder, kan beviserne udformes ud fra en meget præcis opskrift. Dette gælder f.eks. for beviser for uafgørbarhed ved reduktion. Og uanset hvad: De fleste (måske alle) matematiske beviser kan gives en klar struktur. Når man skal kontrollere gyldigheden af et bevis, består arbejdet typisk i at undersøge om dets struktur er fornuftig.

Så måske skal vi gøre særlig meget for at få dette næste-algoritmiske aspekt af matematiske beviser gjort klart for de studerende, vi underviser.

Lamport og mange andre – her specielt Per Martin-Löf og traditionen fra intuitionistisk typeteori – har hver især og sammen arbejdet på at finde en måde at konstruere og strukturere beviser, således at det også kan tjekkes automatisk om et bevis er gyldigt. Vi må kunne lade os inspirere af alle disse gode anstrengelser i vores undervisning, også selv om vi måske ikke bruger Lamports TLA+-system eller bevisassistenter som Coq eller Isabelle.