Een team van onderzoekers heeft een formeel wiskundig kader voor origami ontwikkeld waarin klassieke vouwoperaties en stellingen zijn bewezen met behulp van de programmeertaal Lean 4.
De wiskunde achter het vouwen van papier, ook wel bekend als origami, is al geruime tijd onderwerp van studie. In een recent gepubliceerd onderzoek, getiteld "A Lean Paper About Paper: A Formal Framework for Origami", presenteren Celio Boulay, Alexander Chai, Anthony Chang en Thomas Moulin een methode om deze wiskunde te formaliseren. Het onderzoek is op 14 september 2026 ingediend bij arxiv.org, een platform voor wetenschappelijke preprint-artikelen.
Van axioma's naar bewijsbare stellingen
De kern van het project draait om de zogenaamde zeven Huzita-operaties. In de traditionele origami-wiskunde worden deze operaties vaak als axioma's beschouwd — uitgangspunten die als waar worden aangenomen zonder bewijs. De auteurs van het onderzoek hebben deze benadering gewijzigd door gebruik te maken van de tactieken van Lean 4 en de uitgebreide wiskundige bibliotheek Mathlib.
Volgens de zijn de zeven Huzita-operaties in dit nieuwe kader niet langer axioma's, maar zijn ze geherdefinieerd als stellingen waarvan het bestaan formeel is bewezen. Door deze formalisering kan de wiskunde van origami met computerondersteuning worden geverifieerd, wat de nauwkeurigheid van de constructies vergroot.
Constructies en wiskundige bewijzen
Het onderzoek beperkt zich niet enkel tot de basisoperaties. De onderzoekers hebben bewijzen ontwikkeld voor diverse belangrijke origami-constructies. Een prominent voorbeeld hiervan is het triseren van een hoek, een taak die met een traditionele passer en liniaal onmogelijk is, maar met origami-technieken wel kan worden gerealiseerd.
Daarnaast bevat het project de volgende technische prestaties:
- De implementatie van origami-construeerbare getallen.
- Het formele bewijs van de bijbehorende formule van Cardano.
- De formalisering van de stelling van Haga.
De volledige codebase die door de onderzoekers is ontwikkeld, bevat in totaal meer dan 100 stellingen en lemma's. Deze uitgebreide set aan bewijzen vormt een solide basis voor verdere computationele studies naar papiervouwen.
Visualisatie en fysieke toepassing
Om de brug te slaan tussen de abstracte wiskunde en de fysieke praktijk, hebben de auteurs een 'Crease Pattern Inspector' ontwikkeld. Dit instrument biedt een volledige pijplijn om modellen te creëren en te visualiseren. Deze modellen zijn strikt gebonden aan het formalisme van de Huzita-operaties, waardoor de theoretische bewijzen direct vertaald kunnen worden naar visuele vouwpatronen.
Context van de gebruikte technologie
Het project maakt gebruik van Lean, een interactieve stellingbewijzer. Hoewel de term 'Lean' in andere contexten, zoals in de bedrijfsvoering, verwijst naar een filosofie van waardecreatie met minimale verspilling — zoals beschreven door het lean.org — gaat het in dit wetenschappelijke artikel specifiek over de programmeertaal en logica in de informatica. Het onderzoek is gecategoriseerd onder de discipline 'Logic in Computer Science' op het .
Door de integratie van complexe geometrische operaties in een formeel systeem, opent dit onderzoek nieuwe wegen voor zowel de theoretische wiskunde als de praktische toepassing van computationele geometrie in de kunst van het vouwen.