Er is weer een oud wiskundeprobleem opgelost, maar er is één probleem: de redenering en het bewijs controleren kost zoveel rekenwerk dat de uitkomst nooit door mensen te checken is. Het bewijs is met een computer gemaakt en kan nu dus ook alleen door een computer gecontroleerd worden… Ge...
Het bedenken van een nieuw wiskundig bewijs is nog voorbehouden aan een creatief brein. Maar controleren of een wiskundig bewijs klopt, daarvoor zijn al computerprogramma’s ontworpen. Inmiddels worden bewijzen echter zó ingewikkeld dat ze door mensen niet meer te toetsen zijn; slagen com...
In 1985 werd door twee wiskundigen een vermoeden geformuleerd over het symmetrisch stapelen van blokken. Een kwart eeuw later is er een bewijs. Computerrekenwerk was hierbij onmisbaar: uitgeschreven zouden alle berekeningen meer dan een miljoen volgedrukte A4-tjes in beslag nemen.
Het decembernummer van de Notices of the American Mathematical Society heeft als thema ‘formal proof’, met artikelen over de recentste ontwikkelingen van door computers gegenereerde en door computers geverifieerde bewijzen.
Volgens computers heb je maximaal vier kleuren nodig om een landkaart zó te kleuren dat buurlanden nooit dezelfde kleur hebben. Aan de juistheid van computerbewijzen werd vaak getwijfeld. Tot nu… hopelijk.
In 1998 heeft de wiskundige Thomas Hales met de hulp van computers het vermoeden van Kepler bewezen. Het vermoeden van Kepler is makkelijk uit te leggen – maar razend moeilijk om op te lossen! Kepler zei in 1611, dat de compactste manier om bollen van dezelfde grootte te stapelen, een piramide...