ב־1852 שם לב סטודנט בשם שהוא מצליח לצבוע את מחוזות אנגליה בארבעה צבעים בלבד, בלי ששתי שכנות יקבלו אותו צבע. מאה ועשרים שנה איש לא מצא מפה שדורשת חמישה, ואיש גם לא הצליח להוכיח שזה בלתי אפשרי. ואז, ב־1976, הגיעה הוכחה. מה היה מיוחד בה?
סקרנות נחשבת. הנה התשובה.
ההוכחה נכונה, ואיש לא מצא בה פגם מתמטי. מה שהטריד הוא שחלק ממנה הוא בדיקה של כאלף תשע מאות מקרים שמחשב ביצע, ולכן האמון בה נשען גם על האמון בתוכנה ובחומרה. ב־2005 הועברה ההוכחה למוודא הוכחות אוטומטי, שבודק כל צעד לוגי בנפרד, וזה צמצם מאוד את החשש.
ארבעה צבעים אכן מספיקים תמיד, אבל ההוכחה הראשונה הורצה על מחשב ולא נקראה בעיניים. הרעיון היה להראות שכל מפה אפשרית מכילה בהכרח לפחות אחת מתוך רשימה סופית של , ושכל תצורה כזאת אפשר לצמצם למפה קטנה יותר. הרשימה מנתה כאלף תשע מאות תצורות, ובדיקה ידנית שלהן הייתה אורכת שנים. המחשב עבר עליהן בשבועות.
כדי להרגיש את הבעיה כדאי לנסות. קחו ארבע מדינות שכולן גובלות זו בזו, וקל לראות שצריך ארבעה צבעים. עכשיו נסו לבנות חמש מדינות שכל אחת גובלת בכל האחרות. זה לא יעלה בידכם, ולא בגלל חוסר מזל: במישור זה בלתי אפשרי. מכאן מתפתה לחשוב שההוכחה קצרה, ובדיוק כאן נכשלו עשרות אנשים במשך למעלה ממאה שנה.
הקושי הוא שאי אפשר להסיק מן המקרה הקטן על הגדול. מפה יכולה להיות מסובכת בלי גבול, עם מדינות ארוכות שמתפתלות ונוגעות בעשרות שכנות, ועדיין לא תכיל חמש מדינות שכולן שכנות הדדיות. ב־1879 פורסמה הוכחה שהתקבלה כנכונה, ורק אחת עשרה שנים אחר כך נמצא בה חור. היא כן הספיקה כדי להוכיח שחמישה צבעים מספיקים.
אפל והייקן שינו את השאלה. במקום לחפש טיעון יפה, הם בנו רשימה של תצורות שכל מפה חייבת להכיל לפחות אחת מהן, והראו לגבי כל אחת שאפשר לצמצם אותה. אם שני החלקים נכונים, המשפט נובע. החלק הראשון דרש עבודה אנושית ארוכה; השני היה בדיקה מכנית של כאלף תשע מאות מקרים, שאיש אינו יכול לעבור עליהם ביד.
התגובה בקהילה המתמטית הייתה מעורבת ונשארה כזאת. חלק קיבלו את התוצאה בשמחה, וחלק טענו שהוכחה שאי אפשר לקרוא אינה מסבירה דבר. ההוכחה של 1997 ענתה חלקית: היא קיצרה את הרשימה, סידרה את הטיעון, ועדיין נשענה על מחשב. ב־2005 הועבר הכול , וזה ענה על שאלת האמון אבל לא על שאלת ההבנה.
הבעיה הזאת שינתה את המתמטיקה יותר ממה שהתשובה שלה שימושית. איש אינו צובע מפות בעזרת המשפט, אבל הכלים שפותחו בדרך עובדים היום בתזמון משמרות, בהקצאת לאנטנות ובהקצאת אוגרים במהדר, וכולם אותה שאלה בתחפושת: לחלק דברים שמתנגשים לכמה שפחות קבוצות.
wat. ארבעה צבעים מספיקים לכל מפה מישורית, וההוכחה הראשונה לכך הייתה הראשונה שאדם אינו יכול לקרוא במלואה.
wat wat
עד 1976 הוכחה הייתה טיעון שאדם יכול לקרוא ולהשתכנע. כאן התקבלה תשובה נכונה שאף אדם אינו יכול לעבור עליה בעצמו בתוך חיים שלמים. זה פתח ויכוח שעדיין נמשך על מה בדיוק אנחנו קונים כשאנחנו קוראים למשהו הוכחה: ודאות, או הבנה.
איך יודעים?
שתי הוכחות עצמאיות. הראשונה של קנת אפל וולפגנג הייקן מאוניברסיטת אילינוי ב־1976, והשנייה, פשוטה ומסודרת יותר, פורסמה ב־1997 בכתב העת Journal of Combinatorial Theory בידי רוברטסון, סנדרס, סימור ותומאס. ב־2005 הועברה ההוכחה גם לשפה של מוודא הוכחות אוטומטי, מה שהסיר את החשש משגיאת תכנות.
מה עדיין לא יודעים?
המשפט מדבר על מפה שבה כל מדינה היא חתיכה אחת רציפה. מובלעת שמנותקת מן השטח הראשי, כמו אלסקה או קלינינגרד, שוברת את התנאי, ומפה כזאת יכולה לדרוש יותר מארבעה צבעים. המשפט גם אינו אומר איך למצוא את הצביעה, אלא רק שהיא קיימת.
למדתם משהו?
מכאן ממשיכים
כמה צבעים צריך כדי לצבוע כל מפה בעולם?הוכחה
למה דווקא משושה, ולמה לקח אלפיים שנה להוכיח את זה?הוכחה
איך הוכיחו לפני 2,300 שנה שאין סוף למספרים הראשוניים?הוכחה