هر نقشه دو بعدی را می‌توان با چهار رنگ بطوری رنگ کرد که هیچ دو قطعه‌ی مجاوری هم‌رنگ نباشند

مسئله چهار رنگ اولین مسئله بزرگ ریاضی است که با کمک کامپیوتر به اثبات رسیده است. اینکه برای رنگ کردن یک نقشه پنج رنگ همیشه کافی است و سه رنگ کفایت نمیکند از سال ۱۸۰۰ برای ریاضی دانان به اثبات رسیده بود ولی کافی بودن چهار رنگ علیرغم تلاش ریاضی دانان برای سالهای دراز تا سال ‍‍۱۹۷۶ به اثبات نرسیده بود. اولین بار در سال ۱۸۵۲ این ادعا بصورت یک حدس ریاضی معرفی شد.

اثباتی که توسط دو ریاضی دان آمریکایی در سال ۱۹۷۶ برای این قضیه ارائه شد، تا سال‌ها مورد قبول جامعه ریاضی دان قرار نگرفت. زیرا تایید صحت عملکرد برنامه کامپیوتری بصورت سیستماتیک در آن زمان ممکن نبود. در سال ۲۰۰۵ با تولید اولین نرم افزار مخصوص اثبات قضایای ریاضی (Coq) که امکان فرمول بندی منطقی را در زبان برنامه نویسی بدست میداد بالاخره این اثبات تایید شد. در مورد نرم افزارهای proof assisstant اینجا را ببینید.