יומיות 15.07.2021: ההוכחה המתמטית עוברת מהפיכה

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

מדברים הרבה על איך הקורונה שינתה את העולם, ואצלי השינוי הוא חברותי.

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

1. במהלך שנות לימוד המתמטיקה שלי (דוקטורט, כן?) פיתחתי את הפילוסופיה הבאה.

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

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

"הוכחה זאת דרך מבלבלת להראות את מה שכבר ידעתם מראש שהוא נכון."

(באנגלית זה נשמע יותר טוב, "A proof is an incomprehensible demonstration of a fact that you already know")

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

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

בעשור האחרון נבנה לו תת-תחום של מתמטיקה שעלול לעשות מהפיכה בהוכחות. קוראים לזה Computer-assisted Proof – הוכחות בעזרת מחשב.

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

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

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

אם פתאום יבנה סטנדרט של Computer-assisted Proof, יהיה הרבה יותר קל להשתמש בתוצאות של מתטיקאיים אחרים בבטחה.

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

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

שולץ עובד על משהו שהוא קורא לו 'condensed mathematics', ואמור לעשות מהפיכה בתחום המתמטיקה אם הוא יגיע לבשלות. אבל בינתיים הוא נתקל בבעיה: לא רק שההוכחות שלו מסובכות מדי בשביל קולגות לוודא אותן, אפילו הוא עצמו לא היה בטוח בנכונות שלהן.

לכן הוא השתמש ב-Computer assisted proof כדי לוודא כמה מההוכחות המרכזיות שלו.

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

בלי להיכנס לראש של שולץ, יש לי כמה השערות למה לא. הראשונה היא שלמרות הפלוסים של Computer-assisted Proof, בסופו של יום היא לוקחת את המשימה המייגעת והמשעממת של לכתוב הוכחה מתמטית, והופכת אותה לאפילו עוד יותר מייגעת ומשעממת.

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

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

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

— עם זאת אני מדבר מתוך בורות רבה ושומר לעצמי את הזכות לשנות דעתי בהמשך —

2. ב-1991 (בערך) פג הרשיון של חברת הסבארו לצעצועי מלחמת הכוכבים. חברת Playmates הגישה הצעה לקבל את הרשיון, שכללה קונספט לליין צעצועים של צבי הנינג'ה בעולם מלחמת הכוכבים.

Playmate בסוף לא קיבלו את הרשיון, ואחרי 30 שנה אנחנו סוף סוף זוכים לראות את ההצעה. הנה תמונה אחת מתוכה:

3. מחפשים מד"ב ופנטזיה לקרוא? Goodreads פירסמו את רשימת ספרי המד"ב הכי פופולריים ב-2021 (עד עתה), ואותו הדבר לגבי ספרי פנטזיה.

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

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

אצטט פה את המילים של לוי, שכתב:

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

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

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

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

Nothing was actually "available," as everything was made to order. In fact, there was a period where if someone wanted to order a dish they saw at a neighboring table, they were refused, partly because Kenny felt it showed a lack of imagination, partly so he didn't get bored.

— Scott Edelman (@scottedelman) July 13, 2021