בתשובה לאלון עמית, 24/04/04 11:05
 |
|
 |
||
|
||||
 |
הפיסקה האחרונה שלך העלתה לי זיכרון נעים מהעבר. פעם הכרתי ברנש שעבד על תוכנה שמוכיחה משפטים בגאומטריה אוקלדית (לכל הפחות תת-קבוצה מכובדת שלהם). מה שמחתי שהזדמן לי לבקש ולקבל הדגמה אישית. כבוגר יסודי גאה, זכור לי היטב המאמץ האינטלקטואלי הדרוש בכתיבת שורה אחר שורה של טענות סדורות המובילות אל המשל המיוחל. כך שמובן שהסתקרנתי מאוד לראות אם תוכנה יכולה לעשות את אותו הדבר. בקיצור... בדחילו ורחימו ניגשנו אל התואם, והברנש בחר את אחד מהמשפטים המוכנים מראש והקליק על solve. דקה ארוכה ישבנו והמתנו לתוצאה. הציפיה היתה כה רבה, והשקט כה מתוח, עד כי ניתן היה לשמוע את זמזום המאוורר הפנימי. לבסוף, ברטינה, המחשב פתח message box ובו כתובה ההודעה הגורלית: YES. חצי שעה אחרי זה לא יכלתי להפסיק לצחוק. מי אמר שלאנשי מחשבים אין חוש הומור. ובמסגרת האופטימיות הכללית, כתבתי תוכנה שבודקת את השערת גולדבלך, עכשיו אני רק מחכה שהמחשבים יהיו מהירים מספיק. |
 |
 |
 |
|
|
|
||
|
||||
|
ועכשיו שני סיפורים שהזכרת לי. הראשון, בדיוק על תוכנה שמוכיחה משפטים בגיאומטריה אוקלידית: אחרי שהמתכנן (לא זוכר מי זה היה) הוסיף לתוכנה את היכולת החשובה של בניות-עזר, הוא רצה לבדוק אם זה עובד, ואיתגר את התוכנה להוכיח שבמשולש שווה-שוקיים, זוויות הבסיס שוות. הוא הניח שהמחשב "יוריד אנך" וימשיך עם חפיפת משולשים. למרבה הפתעתו התוכנה הסתדרה בלי שום בניית עזר, ופשוט הוכיחה שהמשולש כולו, ABC, חופף את משולש ACB. אני חושב שזה הובא כדוגמה נאה ליכולת של תוכנה משוכללת-מספיק להפתיע גם את מי שכתב אותה (ולכן הטענה המקובלת "מחשב לא יכול לעשות שום דבר שלא לימדו אותו" אינה מדוייקת). הסיפור השני הוא על הרצאה של סטיבן הוקינג שהגיע פעם לדבר באוני' העברית. כידוע, הוא נואם בעזרת סינתסייזר-קול, וההרצאה עצמה מוכנה מראש והוא רק שולט בקצב ע"י שהוא מקליק בשביל להתחיל את המשפט הבא. עוזר שלו עמד ליד הלוח ודאג לרישומים. בכל אופן, בסוף הגיע גם זמן לשאלות. מישהו שאל שאלה, ואז השתררה דממה ארוכה בעוד הוקינג משתמש בממשק המצומצם-מאוד שלו כדי לבנות את התשובה. כעבור כמה דקות כבר החלו רחשושים בקהל, ופתאום רעם הקול המתכתי: "Yes". כולם נשתתקו - מה, על זה הוא עבד כל-כך הרבה זמן? - ואז התשובה נמשכה; ה-Yes רק נועד לדאוג לכך שראשית המענה לא יאבד ברחש. |
|
|
|
|
|
|
||
|
||||
|
מזכיר את מחשב העל של הפנטגון, אשר היה אמור לספק פתרונות אופטימליים למצבים איסטרטגיים. בטקס ההשקה של המחשב, הציגו לו סידרת ארועים, ובקשו הנחיה האם לפעול בדרך א' או בדרך ב'. המחשב עבד במשך מספר שניות, כאשר כל הקהל מצפה בדריכות למוצא פיו(?). לבסוף יצא הפלט: "כן". מבוכה קלה השתררה בקרב מפתחי המחשב, ואז החליטו להוסיף שאלת הבהרה. "כן מה?" נשאל המחשב. שוב התחיל המחשב לעבוד במרץ, נקפו מספר שניות, ואז פלט המחשב את התשובה המתוקנת: "כן, המפקד!" |
|
|
|
|
|
|
||
|
||||
|
המתכנת היה E. Gelernter, וההוכחה התגלתה במקור ע"י Pappus (בשנת 300 לספירה לערך). | |
|
|
|
|
|
||
|
||||
|
תודה רבה על החצי הראשון. החצי השני היה ירידה מעודנת...? אגב, איפה זה סופר, ב-GEB מיודענו? | |
|
|
|
|
|
||
|
||||
|
לא ירידה, חלילה: סתם משהו שאכזב המון אנשים, כי פירוש הדבר שהתוכנה לא מצאה הוכחה "מקורית" (מבחינה זו שאף אחד לא גילה אותה לפניה). ע' 606. |
|
|
|
|
|
|
||
|
||||
|
תודה תודה. בשנים שחלפו כבר נתגלו הוכחות מקוריות, ואפילו בעיות פתוחות נפתרו. הזכרתי את השערת Robbins, ועכשיו כדאי שגם אוסיף סייג: ההשערה הזו מתאימה במיוחד להוכחה ממוחשבת. (אגב, מי שסבור שגיאומטריה אוקלידית זה קל מוזמן להוכיח שמשולש שבו חוצי-הזווית שווים באורכם הוא שווה-שוקיים.) |
|
|
|
| חזרה לעמוד הראשי | המאמר המלא |
| מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
 RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |