Een wiskundig bewijs correct bewezen: De meest effici?nte manier om bollen op te stapelen

摘要

Sommige bewijzen van wiskundige Stellingen zijn zo bewerkelijk dat ze alleen met compu-terondersteuning geverifieerd kunnen worden. Een voorbeeld is het bewijs van de vierkleu-renstelling, die zegt dat iedere landkaart met vier kleuren ingekleurd kan worden zonder dat aangrenzende landen dezelfde kleur krijgen. Een recent voorbeeld is het bewijs van het vermoeden van Kepler, dat zegt dat de meest voor de hand liggende stapeling van bollen in de ruimte (zoals de groenteman sinaasappelen stapelt) ook de meest effici?nte is. In dit artikel geven Freek Wiedijk, Herman Geuvers en Josef Urban een overzicht van het wiskundige deel van het bewijs en leggen uit op welke manier de computer bij de verificatie is gebruikt.