Podcast: Supercomputer efterprøver verdens største matematiske bevis

Supercomputeren Abacus 2.0 har på et par døgn løst en opgave, som det ville tage menneskelige matematikere 10 milliarder års koncentreret læsning at gennemføre.
Af
14/03/2017 10:03

Den seneste podcast på kanalen "Supercomputing i Danmark" fortæller om arbejdet med at efterprøve et matematisk bevis.

I 2015 lykkedes det et forskerhold fra University of Texas i Austin at løse et kompliceret matematisk problem. Resultatet var et bevis, der fyldte 200 terabytes.

Dermed var det så stort, at det ikke var muligt at efterprøve det matematisk.

Professor Peter Schneider-Kamp fra Institut for Matematik og Datalogi på Syddansk Universitet fandt sammen med to kolleger frem til en metode, hvor de kunne bruge DeiCs supercomputer Abacus 2.0 til at løse opgaven.

De oplærte Abacus til at fungere som en kunstig matematiker med meget høj kapacitet.

I podcast-episoden fortæller Peter Schneider-Kamp om sit arbejde med formel verificering af software – og om opgaven med det hidtil største matematiske bevis.

Links