Wiskunde heeft altijd geleund op twee verschillende talen. De ene is de natuurlijke taal die we gebruiken om ideeën uit te leggen, verhalen te vertellen en inzichten te delen; het is flexibel, rijk aan context en slaat vaak stappen over die voor een menselijke lezer vanzelfsprekend lijken. De andere is de formele taal van bewijsassistenten, rigide computersystemen die elke enkele logische stap controleren om te garanderen dat een conclusie onbetwistbaar waar is. Decennialang hebben onderzoekers gewerkt aan het vertalen van de eerste taal naar de tweede, een proces dat autoformalizatie wordt genoemd. Het doel was simpel: een door mensen geschreven bewijs nemen en dit omzetten in code die een computer kan verifiëren. Maar een cruciaal probleem bleef bestaan. Een computer kon vaak een bewijs produceren dat technisch correct was, maar dat geen enkele gelijkenis vertoonde met het menselijke argument dat eraan ten grondslag lag. De computer kon het probleem oplossen via een totaal ander pad, waarbij de oorspronkelijke redenering werd verborgen achter een muur van geautomatiseerde afkortingen. Dit creëerde een kloof tussen waarheid en begrip. Als het bewijs van de computer de stappen van de mens niet volgt, kunnen we het niet gebruiken om te controleren of de menselijke redenering daadwerkelijk klopte, noch kunnen we erop vertrouwen dat het ons leert hoe het argument werkt.

Een team van onderzoekers heeft deze kloof nu aangepakt met een nieuw systeem dat ontworpen is om het bewijs van de computer trouw te houden aan het oorspronkelijke menselijke denkproces. Ze noemen hun systeem Pistis, een naam afgeleid van het oude Griekse woord voor geloof of vertrouwen. De onderzoekers pasten dit systeem toe op de eerste drie boeken van Euclides' Elementen, een fundamentele geometrische tekst geschreven meer dan tweeduizend jaar geleden. Hun werk demonstreert dat het mogelijk is om deze eeuwenoude argumenten te vertalen naar een moderne computertaal zonder de oorspronkelijke logica te verliezen, terwijl ze ook verborgen fouten in de tekst blootlegden die eeuwenlang onopgemerkt waren gebleven.

De kernuitdaging waar het team voor stond, was dat natuurlijke taal en computerlogica op verschillende ritmes werken. Een menselijk bewijs kan zeggen: "Laten we aannemen dat dit waar is," en vervolgens doorgaan, in de verwachting dat de lezer de kloof zelf invult. Een computer vereist echter dat elke enkele stap expliciet wordt benoemd en gerechtvaardigd. Eerdere pogingen om bewijzen te vertalen lieten de computer deze gaten vaak zelf opvullen met eigen logica, waardoor het argument effectief werd herschreven om het de machine gemakkelijker te maken. Het resultaat was een bewijs dat weliswaar succesvol compileerde, maar de intentie van de menselijke auteur niet weerspiegelde. Pistis werd gebouwd om dit te voorkomen. In plaats van de computer te vragen om elke mogelijke manier te vinden om de stelling te bewijzen, dwingt het systeem de computer om het specifieke pad van de mens te volgen, zin voor zin.

Om dit te bereiken, ontwikkelden de onderzoekers een methode die het vertaalproces opsplitst in twee afzonderlijke fasen. Eerst analyseert een mappingfase de natuurlijke tekst en splitst deze op in een sequentie van kleine, atomaire stappen. Het identificeert precies wat elke zin beweert en op welke aannames deze rust. Dit creëert een strikt sjabloon dat de computer moet volgen. Ten tweede probeert een invul-fase elke van deze kleine stappen afzonderlijk te bewijzen. Het systeem gebruikt een gespecialiseerde zoekstrategie die voorkomt dat de computer afsnijroutes neemt of vooruit springt. Als de computer een specifieke stap niet kan bewijzen met de exacte instrumenten en referenties die de menselijke tekst vermeldt, zoekt hij niet simpelweg naar een andere manier om het probleem op te lossen. In plaats daarvan geeft het systeem een melding, waarmee wordt onthuld dat het oorspronkelijke menselijke argument een gat of een ontbrekend onderdeel kan hebben.

Deze aanpak bleek opmerkelijk effectief bij het testen op de geometrie van Euclides. De onderzoekers genereerden formele bewijzen voor 92 proposities in de eerste drie boeken. Wanneer zij deze nieuwe bewijzen vergeleken met eerdere pogingen, was het verschil groot. De nieuwe bewijzen compileerden meer dan drieëndertig keer sneller, een significante verbetering in efficiëntie die suggereert dat de nieuwe methode de zware, trage berekeningen van oudere systemen vermijdt. Belangrijker nog, menselijke experts die de bewijzen beoordeelden, gaven de voorkeur aan de output van het nieuwe systeem met een grote marge. In een dubbelblind onderzoek vonden beoordelaars de nieuwe bewijzen veel transparanter en betere representaties van de oorspronkelijke tekstargumenten. Een artificiële intelligentie-rechter, getraind om de kwaliteit van de vertaling te evalueren, was het erover eens en gaf de voorkeur aan de nieuwe bewijzen boven de oude met een ratio van meer dan vijf tegen één.

Buiten het simpelweg vertalen van de tekst, fungeerde het systeem als een rigoureuze controleur die echte gebreken in het bronmateriaal blootlegde. Omdat het systeem erop staat de menselijke logica exact te volgen, kan het fouten niet verbergen. In één instantie identificeerde het systeem een citatiefout in een moderne vertaling van Euclides. De tekst verwees naar een propositie over het halveren van een lijn, maar de citatie wees naar een propositie over het delen van een hoek. Het systeem markeerde deze mismatch, waarmee werd aangetoond dat de vertaling de verkeerde idee aan de verkeerde stap had gekoppeld. In een ander geval vond het systeem een gat in de eigen redenering van Euclides, waarbij een specifiek scenario onbehandeld bleef. De onderzoekers waren in staat om formeel aan te tonen dat het oorspronkelijke argument incompleet was, een ontdekking die moeilijk te doen zou zijn geweest zonder een hulpmiddel dat zich strikt aan de oorspronkelijke structuur houdt.

Het succes van Pistis suggereert dat getrouwe formalisering niet alleen een technische oefening is, maar een krachtig instrument voor het verifiëren van menselijke kennis. Door de computer te dwingen hetzelfde pad te bewandelen als de mens, kan het systeem bevestigen of de redenering standhoudt of waar deze tekortschiet. De onderzoekers ontdekten dat hun methode geldige argumenten kon accepteren, ongeldige kon weerleggen en precies kon aanwijzen waar een bewijs fout ging. Deze capaciteit strekt zich uit buiten de antieke geometrie; het raamwerk is ontworpen om te werken met elk wiskundig argument dat in natuurlijke taal is geschreven. Het werk laat zien dat we niet hoeven te kiezen tussen de flexibiliteit van menselijke uitleg en de strengheid van machinale verificatie. Het is mogelijk om beide te hebben, mits de machine wordt gestuurd om de oorspronkelijke menselijke stem en logica te respecteren.

De studie benadrukte ook de grenzen van de huidige technologie. Hoewel het systeem goed werkte voor de eerste drie boeken van Euclides, kon het niet elke propositie in de latere boeken aan zonder aanvullende menselijke begeleiding. Sommige proposities vereisten geometrische concepten die het onderliggende computersysteem nog niet kende, zoals het meten van de lengte van een kromme lijn. De onderzoekers merkten op dat hun systeem afhankelijk is van een mens of een geavanceerde kunstmatige intelligentie om als een 'oracle' te fungeren, die verifieert of de initiële mapping van de tekst correct is. Dit betekent dat het proces nog niet volledig automatisch is, maar het vermindert de hoeveelheid handmatig werk aanzienlijk in vergelijking met eerdere methoden.

Uiteindelijk presenteert het artikel een nieuwe standaard voor hoe wij met wiskundige bewijzen omgaan in het tijdperk van kunstmatige intelligentie. Het gaat verder dan de vraag of een computer een stelling kan bewijzen, naar de meer diepgaande vraag of de computer het argument begrijpt. Door ervoor te zorgen dat het formele bewijs stap voor stap het natuurlijke taalargument spiegelt, hebben de onderzoekers een instrument gecreëerd dat de redenering achter een conclusie kan valideren, en niet alleen de conclusie zelf. Dit stelt wiskundigen en studenten in staat om erop te vertrouwen dat de computer niet alleen een oplossing vindt, maar ook werkelijk de logica volgt van de persoon die het bewijs schreef. Het werk biedt een pad voorwaarts waar menselijk inzicht en machinale precisie samenwerken, waarbij de integriteit van wiskundige ontdekkingen wordt bewaard terwijl de kracht van moderne verificatie wordt benut.