Om korta och långa matematiska bevis

Susanna Figueiredo de Rezende som ska disputera i datologi vid KTH 2019, har tack vare ett anslag från Knut och Alice Wallenbergs Stiftelse erhållit en postdoktoral tjänst hos professor Pavel Pudlák vid the Institute of Mathematics of the Czech Academy of Sciences, Prag, Tjeckien.

För vissa matematiska satser räcker korta bevis, medan andra kräver långa och invecklade. Matematiker föredrar korta och eleganta bevis av vackra satser. Men frågan har även en praktisk aspekt – ett kort bevis som är lätt att verifiera kan vara nödvändigt då det till exempel handlar om att visa att styrsystemet i ett kärnkraftverk aldrig kan förorsaka en härdsmälta.

De Rezendes forskning går ut på att förstå varför vissa matematiska satser tillåter korta bevis, medan andra kräver bevis som är så långa att inte ens en dator kan verifiera dem. Ett exempel där det inte verkar finnas ett kort bevis handlar om att hantera en lista på 100 personer, som var och en även har en vänlista. Frågan är om det går att dela upp personerna i 20 grupper så att ingen hamnar i en grupp tillsammans med någon av sina bekanta? Om det skulle vara möjligt att göra den här indelningen, då skulle en lösning vara ett kort bevis att det är möjligt. Men om det inte är möjligt, så är det inte klart hur man skulle kunna bevisa det.

Ett uppenbart sätt att lösa uppgiften är att skriva ner alla möjliga kombinationer att dela in personerna i 20 grupper och visa att ingen av dem ger en giltig lösning. Men det finns hela 461925547044215873829002327767063134987973369022473729540076955
3540316688341714252515748587739178140524570560271 olika sätt att göra det på. Till och med en dator som kollar en miljard förslag i sekunden skulle behöva räkna i 10⁹⁰ år. Det är mycket längre än hela universums ålder.

Går det då att hitta ett kort och elegant bevis för att uppgiften är omöjlig? De flesta forskare tror inte det. Men ingen vet säkert, och problemet är ett av de sex berömda millenieproblemen inom matematiken. En prissumma på en miljon amerikanska dollar väntar för lösningen till vart och ett av dem.