Omdat computers snel en precies met getallen kunnen werken, maken wiskundigen er graag gebruik van om lastige of saaie berekeningen uit te voeren. Maar er zijn ook programma’s die helpen met logische redeneringen: bewijsassistenten. Anne Baanen verdedigt op maandag 29 januari in een dissertatie aan de VU Amsterdam om bewijsassistenten als ‘programmeur en wiskundige’ begrijpelijker en bruikbaarder te maken.
Bewijsassistenten lopen elke denkstap van een wiskundig bewijs na om vast te stellen of het klopt. Een klein foutje zou het hele werk al onderuit kunnen halen. Het gebruik van een ‘bewijsassistent’ is een moeilijk en tijdrovend proces: alle details moeten precies gemaakt worden en computers hebben niet het gezond verstand en intuïtie die wiskundigen gebruiken om bewijzen te begrijpen. Baanen zette de bewijsassistenten op ‘wiskundeles’ om ze begrijpelijker en bruikbaarder te maken.
Baanen heeft veel technieken geleerd en uitgevonden om wiskunde op papier te vertalen naar iets wat een bewijsassistent begrijpt. Net als bij een mensentaal kan iets wel correct zijn, maar raar klinken. Soms lukte het de jonge promovendus op een andere verwoording te komen die wel goed werkte, of de computertaal uit te breiden. Menselijke wiskundigen kunnen bijvoorbeeld beredeneren: wat we nu hebben, lijkt precies op iets wat we eerder tegenkwamen, dus we mogen hergebruiken wat we al hebben. De bewijsassistent kon die connectie eerst nog niet zien. Er moest elke keer opnieuw aan de bewijsassistent worden ‘uitgelegd’ waarom we eerdere resultaten mochten toepassen. Uiteindelijk vond Baanen een nieuwe manier om de situatie te beschrijven. Daarna had de computer het wel door.
Getaltheorie
Om het onderzoek uit te voeren, schreef Baanen met collega’s mee aan Mathlib, een ‘virtuele wiskundebibliotheek’. Ze keken naar algebraïsche getaltheorie. Daarvoor zetten ze boeken om in duizenden regels. In dat vertaalproces gingen ze doorlopend na wat er moeilijk was om aan de computer duidelijk te maken en hoe dit eenvoudiger is te maken. Hierbij keek Baanen ook naar de logische grondslagen van de bewijsasistent Lean.
Door dit onderzoek kunnen wiskundigen meer en moeilijkere resultaten met een bewijsassistent controleren. Vakken waar studenten voor het eerst kennismaken met logisch redeneren, kunnen nu al overstappen op bewijsassistenten. Ook zijn er toepassingen mogelijk om kunstmatige intelligentie te verbeteren, zoals ChatGPT, dat niet is ontworpen om logisch te redeneren.
