משפט ארבעת הצבעים (חלק ג')

בפוסט הקודם הצגתי את ההוכחה של קאמפ למשפט ארבעת הצבעים, והסברתי כיצד היא נכשלת. בפוסט הזה אני רוצה לסקור בצורה זריזה יחסית ובלי להיכנס לעומק הפרטים את ההוכחות למשפט ארבעת הצבעים שכן קיימות. למה לא להיכנס לעומק הפרטים? ראשית, כי אני לא מבין אותם; ושנית, כי הם מורכבים יחסית ואני לא חושב שאפשר להציג אותם בצורה טובה בבלוג. תחת זאת אקשר אל שלושת המאמרים הרלוונטיים כך שתוכלו לנסות ולקרוא אותם בעצמכם אם תרצו.

בואו נזכיר את לוח הזמנים. המשפט “נולד” בשנת 1852 כשפרנסיס גאתרי המציא אותו ואחר כך אחיו סיפר על כך לדה-מורגן. בשנת 1879 הציע קאמפ את ההוכחה שלו, ובשנת 1890 הייווד הראה מדוע היא אינה עובדת. כמעט 100 שנים עברו מאז, עד אשר בשנת 1976 הכריזו וולפגנג האקן וקנת אפל שיש ברשותם הוכחה (“Every planar map is four colorable”). הנה החלק הראשון של המאמר שלהם, והנה החלק השני. ב-1996 התפרסמה הוכחה חדשה, דומה לזו של אפל והאקן אבל פשוטה יותר, של רוברטסון, סנדרס סימור ותומס. הנה המאמר שלהם (A New” Proof Of The Four-Colour Theorem”). לבסוף, בשנת 2005 פרסם ז’ורז’ גונתייה מאמר שבו הוא מתאר הוכחה פורמלית למשפט ארבעת הצבעים - כלומר, הוכחה שניתנת לבדיקה באופן מלא על ידי תוכנת מחשב. במקרה הזה, המערכת Coq שהיא מערכת בדיקת הוכחות פורמליות מוכרת ומכובדת. הנה המאמר שלו (“Formal Proof - the Four Color Theorem”).

כל ההוכחות הללו מבוססות על אותו עיקרון בסיסי של קאמפ - למצוא קבוצה של קונפיגורציות (שאפשר לחשוב עליהן בתור תת-גרפים אבל זה קצת מטעה) שהיא

• "בלתי נמנעת", כלומר כל גרף שהוא דוגמא נגדית מינימלית למשפט ארבעת הצבעים חייב להכיל קונפיגורציה כלשהי מהקבוצה.
• "ניתנת לצמצום", כלומר אם קונפיגורציה כלשהי מופיעה בתוך גרף, אז הוא לא יכול להיות דוגמא נגדית מינימלית למשפט ארבעת הצבעים (כי אפשר להשתמש בקונפיגורציה כדי להחליף את הדוגמא הנגדית הזו באחת פשוטה יותר).

במאמר של קנת ואפל קבוצת הקונפיגורציות הייתה בת 1478 איברים. במאמר של רוברטסון ושות’, הם מצאו קבוצה אחרת בת 633 איברים, ובמאמר של גונתייה הוא השתמש באותה קבוצה כמו רוברטסון. זה בהחלט מעניין לשאול את השאלה איך מצאו את הקבוצות הללו, והתשובה היא פשוטה - המון, המון ניסוי וטעיה. נסו לקרוא את המאמר של קנת ואפל, שמבלים הרבה זמן בלהסביר את הנסיבות שהובילו לתוצאה שלהם - הם מפרטים כל צעד ושעל. ולמה לפרט כל כך? כי השאלה המתבקשת למראה המאמרים הללו היא - ההוכחות שלכם כל כך מסובכות, למה שנטרח בכלל להבין אותן? לא יכלתם לפשט אותן קצת? אז צריך להבין שהזוועות הללו הן מה שהתקבלו אחרי הפישוטים.

האופן שבו אפל והאקן הגיעו לקבוצה שלהם התבסס על נסיון ליצור מראש קבוצה של קונפיגורציות בלתי נמנעות, תוך בדיקה מה ניתן לצמצום ומה לא. אם התגלתה קונפיגורציה שלא ניתנת לצמצום, הם שינו קצת את הפרמטרים של השיטה שבה הם יוצרים את קבוצת הקונפיגורציות. הם נותנים קרדיט למתמטיקאי אחר, האש, על השיטה הבסיסית שנקראת “פריקה” (discharging): הרעיון הוא להקצות “מטענים” מספריים לצמתים של גרף מישורי כלשהו כך שסכום המטענים הוא חיובי, ואז לגרום לצמתים עם מטען חיובי לחלק אותו באופן שווה בין השכנים, ולהראות שרק במקרים ספציפיים יישארו בכלל מטענים חיוביים על הצמתים בגרף (וכל שאר המקרים נפסלים) ומזה כבר אפשר לשלוף קונפיגורציות. זה לא נשמע כל כך מסובך, אבל זו רק המוטיבציה; כשנכנסתי לפרטים של התהליך המדויק שבו אפל והאקן השתמשו הלכתי לאיבוד מהר מאוד.

לזכותי ייאמר שלא רק אני הלכתי לאיבוד! הנה מה שאומרים רוברטסון ושות’ על החלק הזה של המאמר של אפל והאקן:

Even the part of the proof that is supposed to be checked by hand is extraordinarily complicated and tedious, and as far as we know, no one has made a complete independent check of it.

זו, אגב, כנראה הבעיה המרכזית של המאמר של אפל והאקן, ולא ההסתמכות על מחשב שאוהבים לתאר בתור הסיבה שבגללה ההוכחה הזו היא “חריגה”. תגידו, גם ההוכחה של המשפט האחרון של פרמה היא ארוכה ומסובכת, וזה בוודאי נכון; אבל ככל הנראה (לא קראתי בעצמי) ההוכחה של המשפט האחרון של פרמה יותר מעניינת עבור מי שבקיאים בחומר, ולכן יש להם יותר מוטיבציה להבין אותה עד הסוף. ההוכחה של אפל והאקן היא פשוט… מסובכת. זו לא לגמרי אשמתם - ככה זו קומבינטוריקה.

החלק הידני אצל אפל והאקן הוא זה שמגדיר את הקבוצה המפלצתית בגודלה שלהם (שלא נכללת במאמר במפורש, היא אמורה להיות בנספח שלא טרחתי לחפש) ומוכיחה שהקבוצה הזו היא “בלתי נמנעת”. ההוכחה לכך שהיא “ניתנת לצמצום” כבר דורשת בדיקת מחשב שאני לא סגור על מה היא בדיוק עושה, אבל כנראה צריכה לבדוק הרבה סיטואציות אפשריות שמערבות כל קונפיגורציה (המאמר מפרט קצת יותר על זה, מציג כל מני סוגי צמצומים שונים וכן הלאה; לא הבנתי שום דבר שם מספיק כדי לתאר את זה בבלוג). השורה התחתונה היא שבדיקת המחשב הזו היא לא כזו שאחרי אפשר להוציא הוכחה קצרה יותר; הבדיקה היא-היא ההוכחה.

אני רוצה לחדד את הנקודה הזו. אם מביאים לנו מפה גדולה ומורכבת ואני טוען שאפשר לצבוע אותה בשלושה צבעים, אני יכול להוכיח את זה בצורה פשוטה - אני אומר באיזה צבע לצבוע כל מדינה במפה. את זה אפשר לבדוק בקלי קלות - רק צריך לבדוק שאין שתי מדינות שכנות עם אותו צבע, מה שיסתיים מיידית גם עבור מפות מורכבות מאוד. מה שקשה הוא למצוא את הצביעה הזו. מחשב יכול לשבור את הראש במשך חודשים ארוכים בחיפוש אחר צביעה שכזו, אבל אם מצא - הופס, ההוכחה מכאן ואילך היא שניות.

מה עדיין קשה לעשות? ובכן, להוכיח שמפה לא ניתנת לצביעה בשלושה צבעים. כאן אין לנו משהו שהוא משמעותית יותר טוב מאשר “להריץ בדיקה של כל האפשרויות”. צריך להסתייג כאן קצת - כן יש לנו שיטות מסודרות להוכחה שמשהו בסגנון הזה הוא בלתי אפשרי, וכן אפשר לפשט שם דברים וכדומה - אבל לא יותר מדי. דיברתי על זה כבר בהקשר של בעיה אחרת, של “צביעת שלשות פיתגוריות”. יש תחום שלם שנקרא Proof complexity שמתעסק בנושא הזה, כך שלא אכנס לכך יותר לעומק כאן. השורה התחתונה היא שהוכחת שלב ה”ניתנת לצמצום” היא קשה אינהרנטית, ברמה שמאלצת אותנו להשתמש במחשב. ואז לכו תסמכו על כך שלא נפלה טעות בתוכנית המחשב שמבצעת את החישוב הארוך והמסובך הזה (או שארעה תקלה באמצע החישוב ברמת החומרה של המחשב ואיזה ביט התהפך שם).

ההוכחה של רוברטסון ושות’ משתמשת באותו רעיון בסיסי - אבל כאמור, עבור קבוצה שונה של קונפיגורציות; הם לא ניסו לקחת את הקבוצה של אפל והאקן ולשפר אותה. התרומה הגדולה שלהם על פני אפל והאקן הוא שאת שלב ה”בלתי נמנעת” הם הצליחו לפשט ברמה שמאפשרת לבדוק אותו באמצעות מחשב. כפי שהם אומרים בבדיחות (?):

The first proof needs a computer. The second can be checked by hand in a few months, or, using a computer, it can be verified in a few minutes.

כאן “ההוכחה הראשונה” היא של ה”ניתנת לצמצום” והשניה של ה”בלתי נמנעת”.

במאמר של גונתייה לא התעמקתי עד הסוף (כן הורדתי את ההוכחה הפורמלית עצמה בשעתו והצצתי בה, אבל קשה לומר שהבנתי ממנה יותר מדי). נראה שהוא מתבסס על ההוכחה של רוברטסון ושות’, אבל עם וריאציות כלשהן על ההגדרות על מנת לפשט את הפורמליזציה של הבעיה בתוך Coq. כאן אני נתקע בשל חוסר ההיכרות שלי עם Coq (שלא עשיתי יותר מאשר לשחק בה קצת ואני לא מבין עד הסוף את הלוגיקה שעליה היא מבוססת); אם אני אכתוב פוסט על הוכחות פורמליות ועל Coq בוודאי שלא אתחיל דווקא מההוכחה הזו.

אז זהו זה. זה כל מה שאני יכול להגיד על ההוכחות שאני מכיר. עכשיו עולות מאליהן שתי שאלות.

ראשית, האם אין הוכחות אחרות? ובכן, בוודאי שיש! גיגול זריז יעלה עוד הוכחות שונות ומשונות, חלקן קצרות עד להפתיע. אני לא מאמין לאף אחת מהן מלבד השלוש שתיארתי כאן, אבל לא ניסיתי בכלל לחפש את הטעות בהוכחות האחרות (ואם אנסה, בכלל לא בטוח שאצליח; זוכרים כמה קשה היה לשים לב לטעות של קאמפ?) כמו במשפט האחרון של פרמה, אפשר בהחלט לשאול את השאלה אם קיימת גם הוכחה פשוטה למשפט שפשוט חומקת מאיתנו; כמו במשפט האחרון של פרמה, נראה שהתשובה היא “ככל הנראה לא” (אפל והאקן מרחיבים על כך במאמר שלהם) אבל לכו תדעו. אני לא רוצה לדכא את היצירתיות של אף אחד; מה שכן, אם יש הוכחה אחרת, כנראה שהיא תצטרך להיות שונה בסגנון שלה; לא וריאציה על הרעיון של קאמפ.

שנית, האם אני מאמין להוכחות שכן קיימות? ובכן, כן. גם כי קיום הוכחה פורמלית ב-Coq מרגיע אותי, וגם כי אני מאמין לדברים שאני הרבה פחות מבין (המשפט האחרון של פרמה! שוב!). אולי אני טועה, אבל אם כן, אז מה? המשפט לא חשוב במיוחד, בסופו של דבר. שאלה יותר מעניינת ופילוסופית משהו היא האם הוכחה שדורשת מחשב לבדיקתה היא אכן הוכחה, וכאן אני רוצה להחזיר אותנו שוב לכך שהבעיה הבסיסית בהוכחה של אפל והאקן היא הקושי שלה, לא הקטע עם המחשב. אני לא מבין עד הסוף אף אחת משלוש ההוכחות, גם ברמת “הטקסט שמופיע בתוך המאמר”; יותר סביר שתיפול טעות בקריאה שלי את המאמרים הללו מאשר בתוכנית מחשב שבודקת את מה שמופיע בהם. אני אמין פחות מאשר המחשב; אם פוסלים את המחשב בתור בודק הוכחות לגיטימי, מה יגידו אזובי הקיר.