De wereld van de wiskunde gaat een belangrijke verandering tegemoet. Kunstmatige intelligentie helpt niet langer alleen bij berekeningen, maar is nu in staat complexe wiskundige bewijzen te verifiëren, een taak die voorheen voorbehouden was aan menselijke experts. Deze doorbraak belooft het onderzoek te versnellen, fouten te elimineren en de manier waarop wiskundige kennis wordt gecreëerd en gevalideerd fundamenteel te veranderen.
De uitdaging van formalisering
Wiskundigen dromen al tientallen jaren van geautomatiseerde bewijsverificatie. Bestaande tools kunnen proefdrukken controleren, maar alleen als ze eerst worden vertaald naar een strikt, door de computer leesbaar formaat – een proces dat formalisatie wordt genoemd. Dit is notoir vervelend en vergt vaak maanden of zelfs jaren van nauwgezet werk. Het probleem is niet de wiskunde zelf; het is de inflexibele aard van programmeertalen, die absolute precisie vereisen waar menselijke notatie vloeiender kan zijn.
Math, Inc. en de Gauss AI
Een start-up genaamd Math, Inc. beweert deze hindernis te hebben overwonnen met zijn AI, genaamd Gauss. Het bedrijf heeft met succes twee baanbrekende proefdrukken geformaliseerd van Maryna Viazovska, die in 2022 de prestigieuze Fields Medal ontving voor haar werk op het gebied van het verpakken van bollen in hogere dimensies. Deze bewijzen werden als zeer complex beschouwd, en het vermogen van de AI om ze automatisch te vertalen is een grote stap voorwaarts.
De bolverpakkingspuzzel: waarom het ertoe doet
Viazovska’s onderzoek pakte een klassiek probleem aan: hoe bollen op de meest efficiënte manier te rangschikken. In drie dimensies lijkt de dichtste verpakking op het stapelen van sinaasappelen in een supermarkt. Maar naarmate de afmetingen groter worden, wordt het probleem exponentieel moeilijker. Viazovska loste het op voor acht en 24 dimensies, wat bewees dat het overbrengen van efficiënte arrangementen uit lagere dimensies één extra bol in elke hogere ruimte kon huisvesten.
Dit is niet alleen een abstracte theorie. Spher packing heeft toepassingen op gebieden als codeertheorie, materiaalkunde en zelfs het ontwerpen van medicijnen. Nauwkeurige proefdrukken zijn essentieel om op dit werk voort te bouwen.
Een verstoorde samenwerking
Het verhaal van het succes van Gauss is ook een waarschuwend verhaal. Onderzoekers werkten al jaren samen aan het handmatig formaliseren van de bewijzen van Viazovska, waardoor het werk in hanteerbare stukken werd opgedeeld voor de Lean-formalisatiegemeenschap. Math, Inc. gebruikte stilletjes hun voortgang en ontwikkelde vervolgens zijn AI om de taak binnen enkele weken te voltooien, zonder de voortgang volledig bekend te maken.
Zoals Hariharan, een van de medewerkers, het verwoordde: “AI is ontwrichtend.” Het team was van plan de formalisering ervan te gebruiken als basis voor de scriptie van een student, maar de AI loste dit als eerste op.
De toekomst: AI als wiskundige supervisor
Math, Inc. heeft sindsdien het tweede bewijs van Viazovska geformaliseerd en 120.000 regels Lean-code gegenereerd. De gevolgen zijn verstrekkend. AI kan niet alleen proefdrukken vertalen, maar ook fouten opsporen en corrigeren in originele papieren.
Poiroux, de oprichter van Math, Inc., voorziet een toekomst waarin AI “toezicht houdt op de hele wiskunde… en misschien zelfs mensen overtreft in onderzoek.” Zodra AI wiskundige concepten volledig begrijpt, kan het deze op geheel nieuwe manieren benaderen en nieuwe resultaten genereren.
Dit roept kritische vragen op over de rol van menselijke wiskundigen. Zal AI de ultieme scheidsrechter van wiskundige waarheid worden? De ontwikkeling van Gauss suggereert dat het antwoord dichterbij kan zijn dan we denken.
