De correctheid van wiskundige stellingen verifiëren met een computer
Hoe correct zijn wiskundige stellingen? En klopt alle theorie daaromheen wel? Om daar achter te komen zette wiskundestudent Dominique Lawson een wiskundige stelling om in computertaal. ‘Een computer kan hierdoor de stelling begrijpen en nagaan of het bewijs erachter wel helemaal correct is.’ Dat onderzoek leverde hem een nominatie op voor de facultaire prijs Young Talent 2023.
Een computer laten controleren of een wiskundige stelling correct is, noemen we formaliseren, legt Dominique uit. ‘Je moet hiervoor heel precies te werk gaan, want het bewijs mag geen gaten bevatten.’ Dominique deed onderzoek naar een stelling binnen het vakgebied gerichte topologie. ‘Dit is een relatief nieuwe tak van wiskunde dat onder andere toepassingen heeft in concurrency. Dat is een onderdeel van informatica dat zich verdiept in de gelijktijdige uitvoering van programma's.’ De computer kon geen gaten vinden in de stelling van Dominique. ‘Het is nu volledig door een computer geverifieerd dat deze stelling klopt.’
‘Het zijn bewijsassistenten’
De afgelopen jaren is er steeds meer interesse in het formaliseren van wiskunde. ‘De computer kan helpen met het schrijven van bewijzen voor een wiskundige stelling. Het zijn dus bewijsassistenten’, zegt Dominique. ‘Wiskundigen hoeven dan alleen nog maar de grote lijnen te bedenken en de software werkt de details uit. Het is fijn als er al veel wiskunde geformaliseerd is, want dan kan je gebruik maken van eerdere resultaten.’
Een ander groot voordeel van formalisatie is de garantie dat het allemaal klopt. ‘Het komt namelijk wel eens voor dat iemand een bewijs publiceert, waar anderen de correctheid van betwijfelen. Een computergeverifieerd bewijs biedt dan een uitkomst.’
Wiskundige concepten vanuit een andere hoek
Het formaliseren van wiskunde was nieuw voor Dominique. ‘Ik was het nog niet eerder tegengekomen tijdens mijn bachelor. Deze verfrissende methode van programmeren met wiskunde vond ik enorm leuk. Je kijkt opeens vanuit een heel andere hoek naar veel wiskundige concepten. Heel is ook ontzettend fijn dat je zeker bent dat het resultaat klopt. Als er bugs of fouten zouden inzitten, slaat het programma namelijk meteen alarm.’
De student, die ondertussen in het eerste jaar van de master Mathematics zit, kijkt met veel plezier terug op zijn onderzoek. ‘Wanneer je een bewijs af hebt, verschijnt er een berichtje op je scherm dat zegt: goals accomplished met een confetti-emoji. Dat maakt het schrijven van bewijzen toch nog leuker. En toen het allerlaatste onderdeel van mijn onderzoek voltooid was, voelde die confetti-emoji erg verdiend.’