Fyrafärgssatsen säger att vilken karta som helst ritad i ett plant plan kan färgläggas med högst fyra färger så att inga två regioner som delar en gräns har samma färg. Två regioner som bara möts i en enstaka punkt får dela färg. Satsen gäller för vilken karta som helst, oavsett hur komplex den är.
Regionerna 1, 2, 3, 4 gränsar var och en till flera andra. Region 4 till vänster och 4 till höger delar ingen gräns och kan därför dela färg. Exakt 4 färger behövs här.
Francis Guthrie formulerade satsen som en förmodan 1852 när han färglade en karta över engelska grevskap. Han noterade att fyra färger alltid verkade räcka men kunde inte bevisa det. Problemet satte stopp för matematiker i 124 år. Många falska bevis publicerades och motbevisades. Fem färger räcker alltid och kan bevisas för hand med Eulers formel för plana grafer.
Fyrafargssatsen tog 124 ar fran konjektur till bevis. 1976 ars bevis var det forsta stora teoremet verificerat av dator.
Beviset från 1976 av Kenneth Appel och Wolfgang Haken var det första stora teoremet bevisat med dator. Det reducerade alla möjliga kartor till 1 936 konfigurationer och lät en dator verifiera var och en under 1 200 timmars CPU-tid. Många matematiker var obekväma med ett bevis som inte kunde kontrolleras för hand. Ett för människor läsbart bevis, om ett sådant finns, är fortfarande oupptäckt.
Fem yttre regioner (ett udda antal) tvingar ringen att använda 3 färger: ingen 2-färgläggning av en 5-cykel existerar. Den centrala regionen gränsar till alla fem och berör alla tre ringfärger, och måste därför ha en fjärde färg. Detta visar att fyra färger verkligen ibland är nödvändigt.
Varje karta ritad i ett plant plan kan färgläggas med högst fyra färger så att inga två regioner som delar en gräns har samma färg. Förmodades av Francis Guthrie 1852. Bevisades av Appel och Haken 1976 med hjälp av en dator som verifierade 1 936 konfigurationer, vilket gör det till det första stora teoremet bevisat med datorhjälp. En kortare verifiering av Robertson, Sanders, Seymour och Thomas 1997 reducerade antalet till 633 konfigurationer. Satsen gäller inte på en torus, där sju färger kan krävas.