איך לארוז תפוזים, שלב ההוכחה

יותר מ-400 שנה לאחר פרסומה נפתרה הבעיה העתיקה ביותר בגיאומטריה הדיסקרטית (בדידה). יוהנס קפלר, שהיה בין השאר אסטרונום, מתמטיקאי, ופילוסוף, ניסח אותה בשנת 1611 במאמרו "על פתית השלג בעל שש הפינות". מקור ההשראה לבעיה הגיע מהשאלה מהי הדרך היעילה ביותר לאכסן כדורי תותח על ספינת מלחמה.

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

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

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

פתרון אינטואיטיבי לכל מוכר בשוק, אבל להוכחה המתמטית נדרשו יותר מ-400 שנה | צילום: Science Photo Library
 

מגבלות המוח

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

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

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