تنص مبرهنة الألوان الأربعة على أن أي خريطة مرسومة على مستوٍ مسطّح يمكن تلوينها باستخدام أربعة ألوان على الأكثر بحيث لا تحمل منطقتان تشتركان في حدٍّ اللونَ نفسه. أما المنطقتان اللتان تتلامسان عند نقطة واحدة فقط فيجوز أن تشتركا في اللون. تنطبق المبرهنة على أي خريطة مهما بلغت درجة تعقيدها.
المناطق 1 و2 و3 و4 تتجاور كل منها مع عدة مناطق أخرى. المنطقتان اليسرى (4) واليمنى (4) لا تشتركان في حدٍّ، لذا يمكنهما مشاركة اللون. هنا بالضبط 4 ألوان مطلوبة.
خمّن فرانسيس غاثري المبرهنة عام 1852 أثناء تلوين خريطة للمقاطعات الإنجليزية. لاحظ أن أربعة ألوان تبدو كافية دائمًا لكنه لم يستطع إثبات ذلك. أعجزت المسألة علماء الرياضيات لمدة 124 عامًا، ونُشرت براهين خاطئة كثيرة ثم دُحضت. أما خمسة ألوان فتكفي دائمًا ويمكن إثبات ذلك يدويًا باستخدام صيغة أويلر للبيانات المستوية.
استغرقت مبرهنة الألوان الأربعة 124 عامًا من التخمين إلى البرهان. كان برهان 1976 أول مبرهنة كبرى يتم التحقق منها بالحاسوب.
كان برهان عام 1976 الذي قدمه كينيث أبل وفولفغانغ هاكن أول مبرهنة كبرى تُثبت بالحاسوب. اختزل جميع الخرائط الممكنة إلى 1,936 تشكيلًا وتحقّق منها الحاسوب خلال أكثر من 1,200 ساعة معالجة. شعر كثير من علماء الرياضيات بعدم الارتياح تجاه برهان لا يمكن التحقق منه يدويًا. ولا يزال البرهان القابل للقراءة البشرية، إن وُجد، غير مكتشف.
خمس مناطق خارجية (عدد فردي) تُجبر الحلقة على استخدام 3 ألوان: لا يوجد تلوين ثنائي لدورة من 5. المنطقة المركزية مجاورة للخمس جميعها وتلامس ألوان الحلقة الثلاثة، لذا يجب أن تكون بلون رابع. هذا يُظهر أن أربعة ألوان ضرورية فعلًا أحيانًا.
يمكن تلوين كل خريطة مرسومة على مستوٍ مسطّح بأربعة ألوان على الأكثر بحيث لا تشترك منطقتان متجاورتان في اللون نفسه. خمّنها فرانسيس غاثري عام 1852. أثبتها أبل وهاكن عام 1976 باستخدام حاسوب للتحقق من 1,936 تشكيلًا، مما جعلها أول مبرهنة كبرى تُثبت بمساعدة الحاسوب. اختصر روبرتسون وساندرز وسيمور وتوماس عام 1997 التحقق إلى 633 تشكيلًا. لا تصح المبرهنة على الطارة (torus) حيث قد تُحتاج سبعة ألوان.