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
- Supercomputer efterprøver verdens største matematiske bevis, podcast-episode
- Podcasts om Supercomputing i Danmark på DeiC eScience Vidensportal
- Supercomputing i Danmark (RSS)
- Supercomputing i Danmark (iTunes)
- Supercomputing i Danmark (Player FM)