Wordt de computer de bewijsexpert van de toekomst?

Dit artikel is gepubliceerd in NRC Handelsblad, 31 januari 2009

Laat de computer elk wiskundebewijs controleren, vindt een groep wiskundigen en logici. Dan weten we absoluut zeker of een bewijs klopt. Maar het gros van de wiskundigen ziet daar nog niets in.

Als er één wetenschap exact is, dan is het de wiskunde wel. De natuurwetenschappen produceren nooit absolute zekerheden. De wiskunde wel. Toen de stelling van Pythagoras eenmaal was bewezen, gold het bewijs voor eens en altijd. Toch lijkt er een kentering te ontstaan in die absolute zekerheid. Wiskundige bewijzen zijn in de loop van de tijd steeds complexer en langer geworden. Zo complex, dat collega-wiskundigen die een bewijs controleren, het soms ook niet meer zeker weten. Honderden pagina’s bewijs zijn geen uitzondering meer.

In 1998 gaf de Amerikaanse wiskundige Thomas Hales een bewijs voor een bijna vier eeuwen oud wiskundeprobleem: het Keplervermoeden (1611). De vraag is hoe je sinaasappels, tennisballen of knikkers zo efficiënt mogelijk op elkaar stapelt. Elke groenteboer heeft in de praktijk het antwoord al gevonden, maar hoe bewijs je dat die stapeling inderdaad de ruimte het meest efficiënt vult? Hales puzzelde het uit, en had daarvoor onder andere veertigduizend regels computercode nodig.

Nu is een bewijs pas een geldig bewijs als andere wiskundigen het er gezamenlijk over eens zijn dat het klopt. Vier jaar lang bogen twaalf experts zich over het bewijs van Hales, zowel de papieren berekeningen, als de computercode en de computerresultaten. Uiteindelijk concludeerden ze dat ze 99% zeker waren dat het bewijs klopt. Ze vermeldden uitdrukkelijk dat ze het niet voor de volle honderd procent hadden kunnen verifiëren. Een unicum in de wiskunde.

Hoe frustrerend. Want wat heb je aan een bewijs als er een kleine kans is dat het niet klopt? Een beetje fout bewijs bestaat net zo min als een beetje zwanger zijn. De Hongaarse wiskundige Gábor Fejes Tóth, projectleider bij de controle van het bewijs van Hales, meent dat het steeds vaker gaat voorkomen dat wiskundigen niet meer absoluut overtuigd kunnen zijn van de geldigheid van een bewijs, en dat ze daar maar aan moeten wennen.

Perfecte boekhouder
Maar er is een oplossing, zo denkt een groep van naar schatting tussen vijftig en honderd wiskundigen en logici. Een kleine minderheid in de wereld van wiskundigen, maar toch. Ze zijn sterk van hun missie overtuigd. Ze willen de computer gebruiken om bewijzen te controleren, en zo de absolute zekerheid terug winnen.

Een van die wiskundigen is dr. Freek Wiedijk van het Institute for Computing and Information Sciences van de Radboud Universiteit Nijmegen. Samen met een tiental Nijmeegse collega’s onder leiding van professor Henk Barendregt gebruikt hij een computersysteem om wiskundige bewijzen te controleren.

“Elke stap die een wiskundige in zijn hoofd maakt,” legt Wiedijk uit, “maken we expliciet en vertalen we voor een computer in een logische taal. Het vertaalde bewijs is dan gemiddeld zo’n viermaal langer dan het gewone wiskundige bewijs. Tussenstapjes die voor iedere wiskundige duidelijk zijn en die hij in het gewone wiskundige bewijs overslaat, moet je uitleggen aan een computer. Naarmate de technologie vordert, zijn er wel minder tussenstapjes nodig. De computer loopt vervolgens alle stappen na en controleert of ze voldoen aan de logische regels van het systeem. Klopt er iets niet in het bewijs, dan geeft de computer precies aan wat er mis gaat, en waar. Hij doet hierbij niets wat een mens niet kan, maar hij maakt geen fout in de boekhouding. Veel wiskundigen kunnen zich die perfectie niet voorstellen, maar het is een feit.”

Nieuw is het idee niet. De Nederlander Dick de Bruijn was een van de pioniers in de controle van wiskundige bewijzen door een computer. Sinds 1968 werkte hij aan het project Automath, dat hetzelfde doel had als Wiedijk, Barendregt en anderen nu hebben. Automath is geëvolueerd tot modernere, krachtigere opvolgers, met als voornaamste vijf: Coq (Frans), Isabelle (Engels/Duits), HOL Light (Engels), Mizar (Pools) en ProofPower (Engels). Elk systeem bouwt in zijn eigen logische taal stukje bij beetje een bibliotheek op van bewezen stellingen. Hoe groter de bibliotheek, hoe meer nieuwe wiskundige bewijzen het systeem aan kan.

Kan het computerprogramma dat een bewijs controleert niet een bug bevatten, zoals vaak bij ingewikkelde programma’s? Die kans wordt op twee manieren geminimaliseerd, vertelt Wiedijk. Allereerst hoef je bij het computerprogramma maar eenmaal na te gaan of het correct is. Daarna kun je het programma voor allerlei soorten bewijzen gebruiken. Ten tweede worden de programma’s zo geschreven dat de essentie in een klein deel van het totale programma zit. Als die kern bugvrij is, dan is de bewijsverificatie ook bugvrij. Wiedijk: “De kans dat er een bug optreedt die effect heeft op het bewijs, is op deze manier nihil. Het is ons nog nooit gebeurd. We zijn nu zelfs met de computer aan het ‘bewijzen’ dat het essentiële stukje van het programma bugvrij is. Als dat klaar is, hoeven we ons helemaal geen zorgen meer te maken over bugs in ons programma.”

Automatische bewijsverificatie is zeker niet alleen een universitair speeltje. Zowel softwarefabrikant Microsoft als chipfabrikant Intel hebben wiskundigen in dienst die bewijsverificatoren ontwikkelen. Intel gebruikt de bewijsverificator bijvoorbeeld om te bewijzen dat er geen bug in een nieuw type chip zit. In 1994 kostte een bug in de Pentiumchip het bedrijf veel geld, en dat mag niet een tweede keer gebeuren.

Wat heeft het ontwikkelen van automatische bewijsverificatoren tot nu toe opgeleverd? Wiedijk: “Aan het Poolse Mizar-systeem wordt het langst gewerkt, al sinds 1974. Het bevat inmiddels zo’n vijftigduizend stellingen die zijn geformaliseerd en die de computer heeft goedgekeurd. En als je de lijst van honderd mooiste wiskundige bewijzen neemt, dan zijn er daar inmiddels 81 van door een computer geverifieerd. Nu zijn computerbewijzen nog een soort kunst omwille van de kunst. Maar ik ben er van overtuigd dat dit de toekomst van de wiskunde wordt. Over enkele decennia zullen wiskundigen blij zijn met de computer als bewijsverificator. Er is namelijk geen fundamenteel obstakel om bewijzen zo te formaliseren dat computers ze kunnen checken. De technologie moet alleen verder ontwikkeld worden.”

Punt is echter dat geen enkele wiskundige ook maar de geringste twijfel heeft over de correctheid van de door de computer geverifieerde 81 bewijzen uit de lijst van honderd. Tot nu toe heeft een computer nog geen enkel bewijs gecontroleerd waarover geen honderd procent zekerheid bestaat, en dat kan nog wel even duren ook. Zo werkt Thomas Hales zelf al sinds januari 2003 aan het formaliseren van zijn eigen Keplerbewijs zodanig dat de computer het kan controleren en ook de laatste 1% onzekerheid wegneemt. Hij heeft berekend dat dit project twintig mensjaren gaat kosten. Hales gebruikt het HOL Light-systeem, maar hij richt zich alleen op het automatisch bewijzen van het Keplerprobleem.

Veel wiskundigen vinden dat Hales zijn tijd beter kan besteden aan het bedenken van nieuwe wiskunde, dan aan het formaliseren van zijn eigen bewijs. Maar Hales beschouwt het formaliseren van de belangrijkste bewijzen uit de wiskunde als ‘het ontrafelen van het wiskundige genoom’. Het is een oude droom van wiskundigen en logici: de hele wiskunde van onderaf helemaal uit de logica opbouwen, met zo min mogelijk aannames. Maar die droom is tot nu toe nooit uitgekomen.

Bureaucratische operatie
Hoewel Wiedijk er van overtuigd is dat computerbewijzen de toekomst hebben, geeft hij grif toe dat het gros van de wiskundigen het nog steeds anders ziet: “Wiskundigen zijn er niet in geïnteresseerd en geloven er nog niet in. Helaas.”

Eén van de wiskundigen die behoort tot de grote groep van critici van zo’n wiskundig-genoomproject, is de Duitse wiskundige en logicus professor Ulrich Kohlenbach van Technische Universiteit van Darmstadt: “In zekere zin klopt het wat Hales zegt over het ontrafelen van het wiskundige genoom. Maar het is net als in de biologie. Kennis van het genoom betekent niet dat je de biologie van de mens begrijpt. Evenzo is wiskunde meer dan een verzameling van geformaliseerde bewijzen die op een of andere server staan. Wiskunde is een uitwisseling van ideeën tussen mensen. Mensen moeten die ideeën begrijpen, anders bestaan ze niet.”

Kohlenbach zegt dat hij niets principieels heeft tegen bewijsverificatie door een computer, maar wel iets tegen automatische bewijsverificatie als een wereldwijd project voor de hele wiskunde: “Ik ben tegen het idee dat alle wiskundigen in de toekomst hun bewijzen zo moeten opschrijven dat een computer ze kan controleren. Allereerst denk ik niet dat dat zal gebeuren. Hoewel het in principe mogelijk is, is het een veel te arbeidsintensief project, en levert het conceptueel weinig tot niets nieuws. Ten tweede vind ik ook niet dat we die kant uit moeten gaan. Het zou de aandacht verschuiven van het bewijzen van nieuwe resultaten naar een bureaucratische operatie van het routinematig checken van wiskundige kennis. Dan moeten we wiskunde voor machines gaan schrijven in plaats van wiskunde voor mensen.”

Kohlenbach vindt dat er voor 99,99 % van de wiskundige bewijzen helemaal geen controleprobleem bestaat: “Daar werkt het traditionele refereeproces prima. Als er al een fout in een bewijs zit, dan vinden mensen deze vroeger of later wel.” Alleen in uitzonderlijke gevallen bestaat er volgens hem een behoefte aan geautomatiseerde bewijsverificatie. Dat is bijvoorbeeld het geval bij het Keplerbewijs en het bewijs van de vierkleurenstelling.
De vierkleurenstelling zegt dat je iedere landkaart met vier kleuren kunt inkleuren zodanig dat landen die elkaar in meer dan een punt aanraken verschillend gekleurd zijn. Kenneth Appel en Wolfgang Haken gaven in 1976 een bewijs dat zevenhonderd pagina’s papieren redenering combineerde met 1200 uur computerrekentijd, een gruwel voor veel wiskundigen in die tijd. De grap gaat dat wiskundigen boven de veertig niet overtuigd konden worden dat het computerbewijs klopt, en dat de wiskundigen onder de veertig niet overtuigd konden worden dat het zevenhonderd pagina lange papieren bewijs klopt.

Patroonherkenning
De Leidse wiskundige professor Hendrik Lenstra staat neutraal in de discussie over het computerbewijs. “Ik zie geen reden waarom de computer niet op grote schaal gebruikt zal worden om bewijzen te verifiëren. Maar de uitspraak dat het over enkele decennia gebeurt, is ongelofelijk zwak. In de jaren zestig dacht men dat de computer over tien jaar de wereldkampioen schaken zou verslaan. Dat is niet gebeurd. Idem dito in de jaren zeventig. Maar uiteindelijk is het wel gelukt. Hetzelfde kan gebeuren bij het computerbewijs.” Lenstra wil echter benadrukken dat wiskunde veel meer is dan bewijzen. “Weten of iets waar is, is niet de eerste bezigheid van wiskundigen. We willen weten waarom iets waar is. Ons vak is niet het controleren van bewijzen, maar het produceren van bewijzen.”

Het produceren van een bewijs is vooralsnog een menselijke bezigheid. Lenstra: “Als je een bewijs bedenkt, dan doe je voor een groot deel aan patroonherkenning. Je legt de associatie met iets wat je eerder bent tegengekomen, soms zelfs in een andere tak van de wiskunde. Je bent niet in eerste instantie geïnteresseerd in de inhoud van bepaalde stellingen, maar in de mechanismen die achter hun waarheid steekt. Als je dat begrijpt, dan kun je het ook in een andere situatie toepassen. Dan heb je weinig aan de mededeling dat die stelling correct is. Daarom houden wiskundigen niet zo van een computerbewijs. Ze kunnen niet zien of het correct is, en waar eventueel een fout zit.”

Opeens herinnert Lenstra zich een persoonlijke ervaring met computerbewijzen, die de scepsis van veel wiskundigen illustreert: “Ik stootte op een stelling, die niet uit mijn eigen vakgebied kwam, en ik wilde weten of de stelling waar of onwaar was. Ik zag dat een computer het antwoord moest kunnen berekenen. Ik heb het toen voorgelegd aan iemand uit de computeralgebra. Hij programmeerde het probleem, en na een dag rekenen gaf de computer het antwoord dat de stelling ‘waar’ was. Een tijd later kwam ik een expert tegen op het terrein waarover die stelling ging. Ik legde hem mijn probleem voor en hij zei: ‘dat reken ik zo voor je uit’. Hij pakte een servetje, mompelde wat, krabbelde wat op het servetje, en na een tijdje zei hij: ‘de stelling is onwaar’. Toen dacht ik: fijn, ik weet nu nog niet wie gelijk heeft, maar dat servetje kan ik goed gebruiken. Die expert kent de theorie, hij heeft zijn redenering opgeschreven, dus ik kan het narekenen.”

Lenstra nam het servetje mee, ging bestuderen welke redeneringen de expert had gebruikt, en hij ontdekte een onnozele rekenfout: “Dat betekende dat de stelling toch waar was. De computer had dus uiteindelijk gelijk. Maar belangrijker was dat ik nu begreep waarom, omdat ik de achterliggende theorie begreep. Toen ik de theorie voorlegde aan degene die mijn probleem had geprogrammeerd, kon hij het probleem veel handiger programmeren. In plaats van na een dag rekenen, kregen we na een halve minuut al het antwoord. Echte stappen voorwaarts maak je pas als je het in je hoofd begrijpt. Een computerbewijs voegt daar weinig aan toe.”

Darwiniaanse wiskunde
Wordt het dan wel wat met die computerbewijzen? Wiedijk denkt dat op het moment dat het formaliseren van een bewijs minder werk wordt dan het traditionele controlewerk door mensen, er een omslagpunt optreedt. “Dan zullen referees zeggen: Laat het maar door de computer controleren.” Maar hoe hij de grote meerderheid van sceptische wiskundigen überhaupt zover kan krijgen dat ze energie en geld willen stoppen in computerprogramma’s die bewijzen verifiëren is de grote praktische vraag.

Volgens Lenstra zijn de bewijsprogramma’s die worden geschreven, voor wiskundigen onbegrijpelijk: “Die programma’s zouden veel dichter bij de gebruikelijke wiskundige taal moeten aansluiten, liefst zelfs bij de natuurlijke taal.” Wiedijk is het daar helemaal mee eens en ziet dat ook als zijn persoonlijke doel bij de ontwikkeling van de computer als bewijsverificator. Maar ook dat is een project van de lange adem.

Samen met professor Henk Barendregt schreef Wiedijk in een artikel over het computerbewijs dat wiskundigen niet bang hoeven zijn dat de computer hun creativiteit afpakt, en dat het computerbewijs een logische overgang is van romantische wiskunde naar coole wiskunde. Het is vergelijkbaar met de overgang in de biologie van aandacht voor bloemen en vlinders naar die voor genen. Ze schrijven: “De romantische biologie blijft boeien, maar die van de genen heeft daar direct betrekking op, meer dan de romantici zouden willen. Een dergelijke verschuiving zal naar onze mening ook binnen de wiskunde plaats vinden. En net zoals bij biologie, zal menselijk vernuft en vakintuïtie hard nodig blijven.”

Hoewel het ontrafelen van het wiskundige genoom met de computer in principe mogelijk is, is het maar de vraag of de wiskundige gemeenschap er de menskracht en het geld voor over heeft. Wiedijk heeft uitgerekend dat het formaliseren van de belangrijkste bewijzen uit de wiskunde met het budget van een populaire Hollywoodfilm te doen is. “Maar ja,” voegt hij toe, “die film brengt daarna geld op, en onze bewijssystemen niet.”

Misschien gaat de wiskunde door de toenemende complexiteit van bewijzen wel meer op de exacte natuurwetenschappen lijken, waar absolute zekerheid ook niet bestaat. Het controleren van bewijzen wordt dan nog meer een sociaal en Darwiniaans proces dan het nu is: een survival of the fittest van wiskundige bewijzen. Toch blijft zelfs dan de wiskundige exactheid ongeëvenaard vergeleken met die van alle andere wetenschappen. “Maar,” besluit Wiedijk, “als ik gelijk krijg, en computerbewijzen gaan echt een grote vlucht nemen, dan wordt de wiskunde eindelijk echt ‘wis’.”


[kader:]
Kan de computer ook zelf nieuwe wiskunde ontdekken?

Wanneer de computer een bewijs controleert, controleert hij stapje voor stapje of de mens geen fout heeft gemaakt. Nog steeds is het de wiskundige die het bewijs heeft bedacht. Maar zou een computer ook zelf nieuwe wiskunde kunnen ontdekken? “In specifieke takken, zoals de computeralgebra, denk ik dat de computer zelf nieuwe wiskunde kan ontdekken”, zegt professor Ulrich Kohlenbach van de Technische Universiteit Darmstadt. “Dat is op bescheiden schaal ook al gebeurd in de computeralgebra. Maar ik geloof niet dat we de computer ooit voor de hele wiskunde beter wordt dan de mens.”

Ook Freek Wiedijk van de Radboud Universiteit Nijmegen denkt dat de computer nauwelijks zal bijdragen tot het ontdekken van conceptuele nieuwe wiskunde: “Automatische stellingenbewijzers zijn vreselijk interessant, maar kunnen vaak zelfs niet eens ‘makkelijke stapjes’ in een bewijs zelf doen. Laat staan dat ze met intelligente suggesties kunnen komen. De computer moet je volgens mij zien als een relatief domme maar zeer precieze en daarom zeer waardevolle boekhouder, niet als een geautomatiseerde versie van een menselijke assistent. Net zoals je een tekstverwerker ook niet moet zien als een assistent die je helpt een artikel te schrijven. Sommigen beweren dat computers de wiskundigen al hebben ingehaald. Dat geldt echter alleen voor specifieke puzzelbewijzen: problemen met veel mogelijkheden. Maar dat is niet conceptueel. De computer is natuurlijk wel enorm nuttig om allerlei voorbeelden door te rekenen. Zo verzamelt hij als het ware experimenteel materiaal waarop de mens zijn intuïtie kan loslaten.”

Professor Hendrik Lenstra van de Universiteit Leiden is iets optimistischer: “Ik zie niet waarom het principieel onmogelijk is voor de computer om nieuwe wiskunde te ontdekken, maar daar staan we wel nog ver van af. Wiskundigen zijn sterk in het conceptualiseren van een bewijs. Om dat te automatiseren, is een enorme dobber.”


Internet
Speciale editie van de Notices van de American Mathematical Society over computerbewijzen (december 2008):
www.ams.org/notices/200811/
De top 100 van wiskundige stellingen, en welke daarvan met welk computersysteem zijn geverifieerd:
www.cs.ru.nl/~freek/100/index.html
Bewijzen: romantisch of cool?:
ftp://ftp.cs.kun.nl/pub/CompMath.Found/euclides.pdf
Voor wie wil zien hoe een computerbewijs van een eenvoudige stelling (‘Er is geen grootste priemgetal’) eruit ziet, vergeleken met het gewone wiskundige bewijs: www.cs.ru.nl/~freek/pubs/pythagoras.pdf
Het Flyspeck-project van Thomas Hales om zijn eigen bewijs van het Keplerprobleem door een computer te laten verifiëren: http://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet
Het QED-manifest uit 1994 beschrijft een toekomst waarin alle wiskundige bewijzen in de computer zijn gecodeerd:
www.cs.ru.nl/~freek/qed/qed.html

Cyborg Kevin Warwick

Dit artikel is gepubliceerd in De Ingenieur 30 januari 2009

Zijn cyborgexperimenten zijn controversieel. Sommige collega’s vinden hem vooral mediageil. Maar hoogleraar cybernetica Kevin Warwick wil grenzen verleggen tussen mens en machine. Zijn droom: zijn eigen brein via een implantaat direct koppelen aan dat van een ander.

Naam: Kevin Warwick
Leeftijd: 54
Titels: prof. dr.
Opleiding: Op zijn zestiende verliet hij de middelbare school om bij British Telecom te gaan werken. In 1976 studeerde hij alsnog af in de elektrotechniek aan de Aston University in Birmingham. Hij promoveerde in 1982 aan het Imperial College in Londen.
Functie: Hoogleraar cybernetica aan de University of Reading, sinds 1987. In 2000 gaf hij de beroemde Royal Institution Christmas Lectures, een serie van vijf lezingen onder de titel ‘The rise of the robots’. Het bekendst werd hij in 2002 met zijn project Cyborg 2.0, waarbij zijn vrouw en hij via twee geïmplanteerde chips zenuwprikkels aan elkaar konden doorgeven.


Een goedlachse Kevin Warwick laat het litteken aan de binnenkant van zijn linkerpols zien: “Hier is het implantaat naar binnen gebracht”, zegt hij. Dat was in 2002. Een klein array van honderd elektroden werd na een urenlange operatie direct gekoppeld aan zijn polszenuwen. Warwick leerde vervolgens om met zijn zenuwprikkels een robotarm aan te sturen. Op bezoek in New York werd hij zelfs verbonden met een computer van de Columbia University, om van daaruit, via het internet, een robotarm te controleren bij zijn thuisuniversiteit in het Engelse Reading, aan de andere kant van de oceaan.

Toen dat allemaal was gelukt, volgde het spannendere tweede deel van het experiment. Warwicks vrouw Irena kreeg ook een chip geïmplanteerd. Beide chips konden zowel elektrische signalen van de zenuwen oppikken, als ook elektrische signalen aan de zenuwen doorgeven. Het opgepikte signaal werd verwerkt door een computer en vervolgens draadloos doorgegeven aan de geïmplanteerde chip van de partner.

“Dat was het opwindendste experiment uit mijn leven”, vertelt Warwick tijdens een interview in Tilburg. De plaatselijke universiteit had hem in december uitgenodigd op een congres over de maatschappelijke gevolgen van nieuwe technologieën. “Wanneer mijn vrouw haar hand samenkneep, voelde ik een soort stroompje naar mijn vingers lopen. Het was best aangenaam. Zij vond het pijnlijker. Wanneer ik mijn hand samenkneep, voelde zij dat er een soort bliksemflits door haar hand schoot.”

Het duurde trouwens zes weken voordat Warwicks hersenen het binnenkomende signaal juist wisten te interpreteren. In de eerste twee weken experimenteerden de onderzoekers met de amplitude en de frequentiecomponenten van het signaal, om te kijken op welke manier Warwick het aangeboden signaal het beste herkende. Daarna moest zijn brein leren om het ook te herkennen als een extern signaal, niet als een prikkel van zijn eigen arm. Pas toen Warwick in uitgebreide tests elk extern aangeboden signaal ook als extern herkende, werd hij op afstand verbonden met de chip van zijn vrouw.

Warwick: “Het was de eerste keer dat de gevoelens van twee mensen zo direct aan elkaar werden doorgegeven. Voor mij is dit de eerste stap op weg naar een directe uitwisseling van gedachten tussen twee mensen.”

Mens 2.0
Warwick wil de grenzen tussen mens en machine laten vervagen, en hij schuwt daarbij controversiële experimenten en grote uitspraken niet. In een essay voor het tijdschrift Wired schreef hij in het jaar 2000: “Ik ben als mens geboren, maar dat was een toevallig ongeluk. Ik geloof dat we de macht hebben om dat te veranderen.”

“Waarom zou ik me moeten beperken tot het lichaam dat ik heb?”, zegt hij ook nu nog vol overtuiging. “Ik zou mijn lichaam graag upgraden zodat ik bijvoorbeeld ook ultrasoon geluid of infrarood licht kan waarnemen. Het experiment samen met mijn vrouw was daar een eerste stap in. Zo’n upgrade is voor mij persoonlijk het meest uitdagend. Maar daarnaast heeft dit onderzoek een belangrijke medische relevantie. Je zou mensen die verlamd zijn, blind, of welke andere handicap dan ook hebben, via een machine-extensie van hun handicap willen verlossen.”

Warwick werkt op dit terrein samen met het Stoke Mandeville Hospital, dat wereldwijde bekendheid geniet op het terrein van dwarslaesieoperaties. Het nut van de medische toepassingen van mens-machine-interactie, is iedereen wel duidelijk. Maar gelooft hij echt dat mensen zichzelf willen upgraden om als cyborg verder door het leven te gaan? “Elke dag ontvang ik een paar e-mails van mensen die zich als vrijwilliger aanbieden voor een cyborgexperiment”, antwoordt de hoogleraar cybernetica. “Vooral jonge mensen willen de grenzen tussen mens en machine graag verleggen. Natuurlijk zijn er mensen die het niet willen, of er zelfs ethische bezwaren tegen hebben. En ja, ook ik neem risico’s. Maar als je als eerste een cyborgexperiment doet, dan weet je niet wat er gaat gebeuren. Het is dat pionieren dat mij drijft.”

Wetenschappelijk gekkenwerk
Warwicks implantaten staan inmiddels tentoongesteld in het Science Museum in Londen. En hij geeft lezingen over de hele wereld. Desalniettemin hebben veel collega’s grote twijfel over het wetenschappelijke nut van Warwicks experimenten. Peter Fromherz van het Max Planck Instituut voor Biochemie in Martinsried (Duitsland) zei in februari 2002 in het wetenschappelijke tijdschrift Science: “Warwick is een zeer interessante persoon. Maar het werk dat hij doet, is wetenschappelijk gekkenwerk.” En vragen als of de mens zijn eigen brein kan upgraden met een extern geheugen, noemt Fromherz veel te prematuur.

Toen Warwick in 2000 werd uitgenodigd om de prestigieuze Royal Institution Christmas Lectures te geven, wekte dat heel wat wrevel op bij Engelse collega’s. Blay Whitby van de Engelse Sussex University, een expert in de kunstmatige intelligentie, zei tegen de BBC over Warwicks uitspraak dat robots in de wereld uiteindelijk de macht van mensen overnemen: “De meeste mensen in het veld vinden dat hij valse verwachtingen wekt en valse angsten oproept. De meerderheid gelooft dat robots nog nauwelijks in staat zijn een opbergkast te ordenen, laat staan dat ze de wereld kunnen veroveren.”

Roboticaonderzoeker Inman Harvey van dezelfde Sussex University reageerde nog korter. Hij noemde Warwick een ‘hansworst’. Warwick laat zich echter niet afschrikken door zulke commentaren: “Ik wil iets met mijn leven doen. Ik wil een cyborg zijn.”

Robot met rattenbrein
Het jongste cyborgproject waaraan Warwick met collega’s aan de Universiteit van het Engelse Reading werkt, is ‘Gordon’: de robot met een rattenbrein. “Ons doel is in eerste instantie om te onderzoeken hoe herinneringen in een biologisch brein worden opgeslagen”, zegt de cyborgpionier.

Uit een rattenfoetus hebben de Engelse onderzoekers hersencellen gehaald die in een speciaal bakje van acht bij acht centimeter worden gecultiveerd. Waar een volledig rattenbrein zo’n miljoen hersencellen bevat, bevat het bakje er typisch honderdduizend. Het bakje is verbonden met een array van zestig elektroden. Dit array is het interface tussen de levende wereld van het mini-rattenbrein en een robot op wieltjes. De activiteit van het gecultiveerde klompje hersencellen stuurt de beweging van de robot aan. De robot kan rondrijden in een rechthoekige bak. Via een ultrasone sensor neemt hij de buitenwereld waar. Het idee is dat hij uit het teruggekaatste ultrasone geluid kan opmaken waar hij zich ten opzichte van de wanden bevindt, zoals een vleermuis zijn omgeving waarneemt. De robot heeft geen andere controle van mens of computer. De enige controle komt van het klompje rattenhersencellen.

In augustus 2008 kwam Warwicks onderzoeksgroep met het eerste persbericht naar buiten. Warwick: “We hebben het bakje een uur per dag met de robot verbonden. Langer lukt nog niet. Maar toch zagen we al binnen een week dat er een soort breinachtige activiteit ontstaat die vergelijkbaar is met wat in een echt rattenbrein gebeurt. En dat terwijl de enige stimulus van de ultrasone sensor komt. Het rattenbreintje stuurt de robot aan, en de robot rijdt rond.”
Maar dat is het dan ook. Van intelligent rondrijden volgens een of andere strategie is nog geen sprake. De vraag is zelfs of Gordon momenteel meer vertoont dan een willekeurig gedrag. Maar Warwick is optimistisch: “Aan de ene kant onderzoeken we nu hoe we het breintje langer kunnen laten leven, en aan de andere kant onderzoeken we hoe het herinneringen vormt, en hoe we het kunnen leren om op een slimme manier rond te rijden. We zouden de robot willen leren objecten te ontwijken en niet tegen een wand aan te botsen. Dat leren kunnen we bevorderen door elektrische of zelfs chemische beloningsprikkels te geven.”

In een column voor het Research Magazine van de Universiteit van Tilburg schreef de cyborgpionier eind 2008: “Momenteel zijn we bezig met het verbinden van audio in- en output naar Gordons elektroden, gedeeltelijk zodat we Gordon kunnen leren om in een richting te bewegen die wij hem willen laten opgaan, maar ook om de mogelijkheid tot een nieuwe vorm van communicatie te openen. Een van de eerste vragen die ik Gordon zou willen stellen, is: ‘Wie of wat denk je dat je bent?’” Waarna Warwick zijn column retorisch besluit met de vraag: “Zal ik dan al tevreden zijn als Gordon antwoordt: ‘42’?”

Van brein tot brein
Warwick wil de rollende Gordon binnen een half jaar voorzien van een breintje bestaande uit menselijke hersencellen, gehaald uit een menselijk embryo. “Ik wil graag weten of we een verschil zien met het gebruiken van hersencellen uit een rat. Ik ben ook benieuwd hoe de maatschappij tegen dat experiment zal aankijken. Vindt de maatschappij dat dit mag, of verwerpt men zo’n experiment? Het experiment zal allerlei filosofische vragen oproepen. Ongetwijfeld zullen er mensen zijn die het verwerpen, maar ik heb ook al e-mails gehad van mensen die hun hersencellen na hun dood wel ter beschikking wilden stellen voor zo’n experiment.”

De ultieme droom van de hoogleraar cybernetica is om zijn eigen brein via een implantaat direct met het brein van een ander te laten communiceren. Dat is het tweede project waaraan hij momenteel werkt. Samen met zijn Reading-collega’s onderzoekt hij wat de beste plek in het brein is om een array met elektroden te implanteren. Zelf wil hij wel een implantaat in zijn brein laten aanbrengen, iets wat in de vorm van Deep Brain Stimulation momenteel alleen maar een optie is voor patiënten met zeer ernstige epilepsie, Parkinson of dwangstoornissen. Een implantaat inbrengen in de hersenen is niet zonder risico.

Het is maar zeer de vraag of Warwicks droomexperiment iets zinvollers oplevert dan opwinding bij hemzelf. Gedachten en gevoelens zitten niet op één plek in het brein, maar hebben te maken met uitgestrekte netwerken, die we nog geheel niet in wetenschappelijke kennis kunnen vatten. “OK, gedachten en gevoelens zitten niet op één plek in het brein,” countert Warwick, “maar toch kunnen hersenimplantaten al iets van gedachten oppikken. Zo kreeg de bij een steekpartij verlamd geraakte Amerikaan Matthew Nagle in 2004 een brein-computerinterface geïmplanteerd. Door te denken kon Nagle de cursor op een computerscherm aansturen. Zo kon hij een tv bedienen of e-mail checken. Wat wel of niet praktisch mogelijk is, kunnen we alleen maar ontdekken door het uit te proberen.”


Internet
Homepage van Kevin Warwick: www.kevinwarwick.com/
You-Tube-filmpje ‘Cyborg Life’: www.youtube.com/watch?v=RB_l7SY_ngI
You-Tube-filmpje over de robot met een rattenbrein: http://www.youtube.com/watch?v=wACltn9QpCc