יומיות 24.9.2022: הוכחות ממוחשבות במתמטיקה

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

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

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

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

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

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

'אתה תמיד קורא הוכחה של כל משפט שאתה משתמש בו?' שאלתי. 'כן' הוא ענה לי לחשוב פעמיים. 'אפילו אם תשתמש בהשערת פואנקרה, תקרא את כל 600 העמודים של ההוכחה שלה?" הקשיתי. 'וודאי, הוא ענה, חייבים."

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

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

בסופו של דבר הבגרות המתמטית שלי הגיעה לבד, והיא אומרת משהו כזה:

כשמתמטיקה מסתכלת על תחום מסוים, היא שואלת שלוש שאלות.

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

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

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

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

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

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

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

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

בקונגרס המתמטיקה שנערך ביולי (הקונגרס נערך פעם ב-4 שנים), הציג קווין בזארד את הההתפתחויות האחרונות בתחום ההוכחות הפורמליות, וזה פיצוץ! הנה ההרצאה המלאה שלו:

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

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

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

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

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

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

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

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

2. Uncanny Island הוא Metaverse שנראה ככה וזה כל כך סייברפאנק שממש בא לי לבנות שם דברים. תנסו בעצמכם פה.

3. יש פודיז בקהל? בקטע של אנשים שאוהבים לקרוא ביקורות אוכל בעברית? ממליץ להם בחום לעקוב אחרי הבלוג מעבד מזון. ביקורות מצוינות על מסעדות בארץ ובחו"ל – כולל הרבה מסעדות מישלן.

4. אגב, מחפש המלצות לבלוגים עבריים חדשים מהשנים האחרונות. תרגישו חופשי להספים בתגובות.

5. אוסף של גרסאות אבסורדיות לבעיית הקרונית. זה הרבה יותר כיף ממה שזה נשמע. תנסו.