Proof Assistants at the interplay of mathematical cultures: a semiotic-cultural analysis of proof in higher education

In de wereld van het universitaire wiskunde is het proces van het bewijzen van een stelling meer dan alleen het oplossen van een probleem; het is een culturele praktijk. Het is een specifieke manier van denken, schrijven en ideeën valideren die studenten moeten leren naarmate ze de overstap maken van de middelbare school naar het hoger onderwijs. Decennialang hebben docenten geobserveerd hoe studenten worstelen met de kloof tussen de intuïtieve, informele argumenten die zij eerder leerden en de rigide, expliciete standaarden die op universitair niveau vereist zijn. Recentelijk is er een nieuw instrument in dit landschap geïntroduceerd: de bewijsassistent (proof assistant). Dit zijn computerprogramma's die ontworpen zijn om wiskundige argumenten met absolute precisie te controleren, waardoor de schrijver wordt gedwongen om geen enkele stap onverklaard te laten. Terwijl sommigen deze hulpmiddelen zien als een manier om wiskunde rigoureuzer te maken, vrezen anderen dat ze de creativiteit kunnen smoren of studenten die al worstelen, verder in de war kunnen brengen. De vraag is niet simpelweg of deze programma's helpen of hinderen, maar hoe ze de essentie van de manier waarop een bewijs wordt geschreven en begrepen, veranderen.

Een team van onderzoekers aan twee Franse universiteiten besloot deze interactie nauwgezet te bestudelen. Ze vroegen niet alleen of studenten beter leerden; ze observeerden hoe het computerprogramma het denkproces van de studenten vormgaf. De studie richtte zich op een eerstejaars vak waar studenten een specifiek type bewijsassistent gebruikten genaamd Verbose Lean. In tegenstelling tot standaard programmeertalen die op code lijken, staat Verbose Lean studenten toe om in een gecontroleerde vorm van natuurlijke taal te schrijven, waardoor het dichter bij de manier ligt waarop wiskundigen spreken en schrijven op papier. De onderzoekers observeerden een duo studenten die werkten aan een klassiek probleem: het bewijzen dat als een reeks getallen steeds dichter bij een positieve waarde komt, de getallen in die reeks uiteindelijk ook positief moeten zijn. Door de gesprekken van de studenten, hun krabbels op papier, hun typen op het scherm en de feedback van de computer vast te leggen, creëerden de onderzoekers een gedetailleerde kaart van hoe een wiskundig idee van een ruwe gedachte naar een door de computer geverifieerd feit reist.

Wat de onderzoekers ontdekten, was dat de computer niet alleen het eindantwoord controleerde; het fungeerde als een spiegel die verborgen aannames onthulde die studenten gewoon als vanzelfsprekend beschouwen. In een normale wiskundeles zou een student kleine details kunnen overslaan of vertrouwen op een "gevoel" dat een stap voor de hand liggend is. De computer eist echter dat elk object, elke voorwaarde en elke logische sprong expliciet wordt benoemd en gerechtvaardigd. De studie toonde aan dat deze eis een soort culturele verschuiving afdwingt. De studenten moesten hun vloeiende, intuïtieve ideeën vertalen naar een rigide structuur die de machine kon begrijpen. Dit proces verliep niet zonder slag of stoot. Het hield een constante heen-en-weer beweging in tussen de aantekeningen van de studenten op papier, hun gesproken woorden, de foutmeldingen van de computer en de uitleg van de docent.

De onderzoekers volgden een specifieke wiskundige uitdrukking die gedurende het werk van de studenten verscheen. Aanvankelijk behandelden de studenten deze uitdrukking als een nuttig getal om in hun redenering te gebruiken. Echter, toen ze probeerden deze in de computer te typen, weigerde het programma. De computer zei niet dat het getal wiskundig gezien fout was; de computer zei dat het getal op de verkeerde plek stond. De studenten hadden geprobeerd het te gebruiken als een label voor een positie in een reeks, maar de computer had een geheel getal nodig voor die rol, terwijl hun uitdrukking een breuk was. Dit moment was een keerpunt. Het dwong de studenten in te zien dat in de wereld van de bewijsassistent de rol die een getal speelt even belangrijk is als het getal zelf. Ze moesten hun strategie heroverwegen en de uitdrukking verplaatsen van het ene deel van hun argument naar een ander deel, waar het uiteindelijk paste binnen de strikte regels van de computer.

Deze strijd werd niet door de computer alleen opgelost. De docent, die op hetzelfde moment bij het schoolbord stond, tekende een diagram om het concept visueel uit te leggen. Hij beschreef een "venster" van een bepaalde grootte dat de studenten hielp inzien waarom hun getal kleiner moest zijn dan de doelwaarde. Deze visuele uitleg, gecombineerd met de afwijzing van de computer voor hun eerste poging, hielp de studenten hun gedachten te reorganiseren. Ze realiseerden zich uiteindelijk dat het getal waarmee ze vochten niet de positie in de reeks was, maar de grootte van de kloof die ze moesten meten. Zodra ze deze overstap maakten, accepteerde de computer hun argument. Het uiteindelijke bewijs was geen rechte lijn van idee naar oplossing; het was een complexe reis waarbij de betekenis van een enkel symbool veranderde, afhankelijk van of het werd uitgesproken, op papier werd geschreven, door een docent werd uitgelegd of door een machine werd gecontroleerd.

De studie suggereert dat bewijsassistenten fungeren als "epistemische onthullers" (epistemic revelators), een term die de auteurs gebruiken om hulpmiddelen te beschrijven die het onzichtbare zichtbaar maken. Ze onthullen de "onuitgesproken gedachten" (unthoughts) van de wiskunde — de delen van een bewijs die experts en studenten gewoon onvermeld laten omdat ze vanzelfsprekend lijken. In een traditionele klaslokaal kunnen deze hiaten onopgemerkt blijven. In een klaslokaal met een bewijsassistent dwingt de computer de student om elke leemte op te vullen, waardoor de verborgen regels die de wiskundige geldigheid beheersen, worden blootgelegd. De onderzoekers stellen dat dit niet betekent dat de computer beter is dan de mens, of dat de mens beter is dan de computer. In plaats daarvan werken de twee systemen samen om een nieuwe ruimte te creëren waar verschillende manieren van het begrijpen van een bewijs samenkomen en versmelten.

De bevindingen wijzen erop dat de introductie van deze instrumenten de cultuur van het bewijs in het hoger onderwijs verandert. Het gaat niet alleen om het toevoegen van een laag technische strengheid; het gaat om het herconfigureren van hoe studenten begrijpen wat het betekent om gelijk te hebben. De studie laat zien dat studenten niet simpelweg leren programmeren; ze leren te navigeren tussen verschillende werelden van betekenis. Ze moeten leren hun intuïtieve begrip te vertalen naar een taal die een machine kan verifiëren, terwijl ze ook luisteren naar de menselijke uitleg van de docent. De foutmeldingen van de computer zijn niet slechts obstakels; het zijn signalen die de student vertellen waar hun begrip incompleet is. Door studenten te dwingen hun impliciete aannames expliciet te maken, bieden deze hulpmiddelen een unieke kans om te bestuderen hoe wiskundige kennis wordt opgebouwd en gevalideerd.

Uiteindelijk concludeert het artikel dat bewijsassistenten geen neutrale instrumenten zijn. Ze dragen specifieke ideeën met zich mee over wat een geldig argument is. Wanneer studenten ze gebruiken, leren ze niet alleen wiskunde; ze leren een nieuwe set culturele regels voor hoe te denken en te communiceren. De onderzoekers suggereren dat deze verschuiving een geprivilegieerde plek biedt om de continuïteit en de breuken te bestuderen tussen de manier waarop een bewijs wordt onderwezen, de manier waarop het door experts wordt beoefend, en de manier waarop het door machines wordt gecontroleerd. De reis van de studenten in deze studie, van hun aanvankelijke verwarring tot hun uiteindelijke succes, illustreert dat leren bewijzen met een computer een proces van vertaling is. Het is een proces waarbij de betekenis van een wiskundig idee wordt getest, hervormd en uiteindelijk gestabiliseerd door de interactie tussen menselijke intuïtie, menselijke begeleiding en machinale precisie.