Bewijsassistenten begrijpelijker en bruikbaarder te maken
Wiskundigen maken veel gebruik van computerprogramma's om lastige of saaie berekeningen uit te voeren, omdat computers heel snel en precies met getallen kunnen werken. Maar er zijn ook programma's die helpen met logische redeneringen: bewijsassistenten. Anne Baanen zette hun ervaring als programmeur en wiskundige in om bewijsassistenten begrijpelijker en bruikbaarder te maken.
Bewijsassistenten lopen elke denkstap van een wiskundig bewijs na om vast te stellen of het klopt, want een klein foutje zou het hele werk al onderuit kunnen halen. Het gebruik van 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 kon hen op een andere verwoording komen die wel goed werkte, of de computertaal uitbreiden. 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 iedere keer opnieuw aan de bewijsassistent worden ‘uitgelegd’ waarom we eerdere resultaten mochten toepassen. Uiteindelijk vond hen een nieuwe manier om de situatie te beschrijven. Daarna had de computer het wel door.
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 steeds na wat er moeilijk was om aan de computer duidelijk te maken en hoe dit makkelijker kon worden gemaakt. Hierbij keek Baanen ook naar de logische grondslagen van de bewijstasistent 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.
Meer informatie over het proefschrift
