Äntligen kan matematiken stapla äpplen

Kan vi vara riktigt säkra på vilket sätt som är det allra mest effektiva för att stapla klot? Redan 1611 publicerade Johannes Kepler sin förmodan om hur det skulle göras så att det uppstår minst mellanrum mellan kloten. Det är precis så som de flesta av oss skulle göra: rada upp dem i ett lager sedan och fylla på med nästa lager i de gropar som bildas mellan de undre kloten. Det känns rätt.

Ett riktigt matematiskt bevis för Keplers förmodan presenterades dock först 1998, av en matematiker som heter Thomas Hales. Eller också [kom beviset 2005](http://annals.math.princeton.edu/2005/162-3/p01). Eller kanske [först nu](https://www.cambridge.org/core/journals/forum-of-mathematics-pi/article/formal-proof-of-the-kepler-conjecture/78FBD5E1A3D1BCCB8E0D5B0C463C9FBC).

– Det som har publicerats nu är ett bevis av ett bevis kan man säga, säger Warwick Tucker, professor i matematik vid Uppsala universitet.

Det låter konstigt att ett bevis behöver bevisas. Matematiska bevis anses ofta perfekt sanningsenliga. Ett bevis ska vara en vattentät kontroll av att en matematisk utsaga är riktig och inte innehåller några luckor eller motsägelser. Men samtidigt är matematik på många sätt en konstform. Matematiker arbetar mycket intuitivt, och det klassiska sättet att presentera bevis bygger på att andra matematiker känner igen hur matematik ska se ut. Enligt Warwick Tucker är det egentligen ganska vagt.

– När man sen släpper beviset till en dator, då kan det visa sig att man har tänkt fel. Datorn är hjärtlös. Den ifrågasätter allt som den inte kan bryta ner ända till de grundläggande axiomen.

Det första beviset för Keplers förmodan bestod av hundratals sidor, och dessutom en massa svårläst datorkod. Ett antal matematiker jobbade i flera år med att kontrollera beviset, och de hittade inga fel. Samtidigt kunde de inte vara säkra på att inga misstag dolde sig i det. Beviset publicerades till slut 2005, och Keplers förmodan upphöjdes till _Keplers sats_. Men Thomas Hales var frustrerad, och började ett stort forskningsprogram för att göra om det hela till ett så kallat ”[formellt bevis](http://www.maths.ed.ac.uk/~aar/papers/hales2.pdf)”, som kan kontrolleras av en dator. Nu har det nya beviset alltså antagits för publicering i en matematisk tidskrift.

– Det här är framtidens matematik, säger Warwick Tucker.

Formella bevis skulle kunna ersätta nästan hela behovet av att ha granskare som går igenom nya resultat inför publicering. Det skulle räcka att gå igenom artikeln på en grundläggande nivå, och resten kunde lämnas åt datorn.

Under tiden kan vi fortsätta stapla äpplen eller spelkulor i trygg förvissning om att vi gör det på det tätaste och mest effektiva sättet.