 |
|
 |
||
|
||||
 |
ההוכחה של Hales להשערת קפלר שנזכרה במאמר התקבלה לפרסום באורח יוצא-דופן במקצת: Annals of Mathematics, אחד העיתונים המתמטיים החשובים ביותר, קיבל לפרסום את החלק התיאורטי של המאמר, ואילו החלק החישובי יתפרסם בעיתון אחר, Discrete and Computational Geometry. הסיפור אף הגיע עד הניו-יורק טיימס: |
 |
 |
 |
|
|
|
||
|
||||
|
מוזר מאוד. אם הבנתי נכון, הרי שהם ניסו לבדוק את ההוכחה, קרי, לעקוב אחר פלט המחשב שלב-אחר-שלב, ולבדוק שההוכחה אכן נכונה – משימה סיזיפית, שלבסוף ויתרו על השלמתה. אבל... למה לא לבדוק *את התוכנה* במקום? לוודא שאין באגים בתוכנה ששימשה לבניית ההוכחה, ושהפלט שניתן לה תקין. אני מניח שבדיקת התוכנה תהיה מסובכת לא-פחות מבדיקת ההוכחה, *אבל* אם התוכנה נכתבה בצורה מודולרית, הרי שבדיקתה יכולה להיות שימושית לבדיקת הוכחות רבות בעתיד. למשל, אם התוכנה נכתבה עם MATLAB, הבדיקה חייבת לכלול הוכחת נכונות של תוכנת MATLAB עצמה. הוכחת נכונות מסוג זה היא אתגר כביר, אבל התוצאה – "ידוע כי גרסה x.y של MATLAB מהווה בסיס יציב להוכחות מתמטיות" – תהיה שימושית שוב ושוב, כלומר לא מדובר במאמץ למען מאמר אחד בלבד. לאחר שהושלם בסיס זה, מתמטיקאים יעדיפו לכתוב את התוכנות שלהם עבור אותו בסיס "מוצק", והבדיקה של כל הוכחה תכלול "רק" את התוכנה הספציפית שנכתבה עבור אותה הוכחה, ואת הקלט. עדיין הרבה עבודה, אבל הרבה יותר ריאלי מבדיקת הפלט, בעיקר כשזה הולך וגדל באורכו. (יש גם את עניין "נכונות הארכיטקטורה", קרי המעבד, מערכת ההפעלה והמהדר. כאן אפשר להסתמך על "נכונות הסתברותית", דהיינו, אם הפלט זהה על מספר ארכיטקטורות שונות מהותית, דיינו. זאת משום שלא הייתי רוצה לכבול את המתמטיקאים למעבד מסוים, שיהפוך מיושן תוך פרק זמן קצרצר). |
|
|
|
|
|
|
||
|
||||
|
לא הייתי סומך על התיאור בניו-יורק טיימס, אני לא בטוח שהתיאור הפשטני שם הוא מדוייק. נראה לי שדווקא תתעניין בתיאור של היילס עצמו את מרכיבי התוכנה - מסתבר שיש שם חבילה בשם cplex לתכנון לינארי, וכן תוכנות בג'אווה (כן!), ++C ואולי עוד. איני בטוח שזה תיאור מעודכן או סופי. אני מהמר שעיקר המאמץ הוקדש, כפי שתיארת, לבדיקת התוכנות, לא הפלט. כמובן שגם אם מישהו יוכיח ש-Matlab x.y היא חופשית מבאגים ואמינה לחלוטין (משימה אימתנית!), עדיין יהיה צריך לבדוק כל תוכנית Matlab שמישהו כותב כדי לראות שאין *בה* באגים. אני נוטה להסכים שקל להקטין את הסיכוי לבאג בתוכנה/חומרה לגודל כה קטן שהוא כבר נמוך מהסיכוי שבסתם הוכחה אנושית סבוכה לא יהיה איזה חור שה-referee פספס. בכל אופן, השימוש בתוכנות להוכחות מתמטיות כבר חרג משימוש בתכנה גנרית כמו Matlab, ויש ממש תוכנות-הוכחה ייעודיות. לגמרי במקרה גיליתי לאחרונה שתוכנה כזו הצליחה להוכיח השערה ישנה בתורה של אלגבראות בוליאניות. צריך לדעת מעט מאוד אלגברה כדי להבין את ההשערה ואפילו, עם המון סבלנות, לקרוא את ההוכחה המלאה שמישהו ערך תוך שימוש בתוכנה: אם המגמה הזו תימשך, ייתכן שהמתמטיקאים של העתיד ייתקלו בבעייה דומה לזו בסיפור של אסימוב: הם ידעו שיש הוכחות לעובדות מסויימות, אבל הם לא יבינו *למה* הטענה נכונה, *מדוע* ההוכחה עובדת. זה יהיה גם עצוב וגם בעייתי, אבל אנחנו עוד לא שם. |
|
|
|
|
|
|
||
|
||||
|
דורון זיילברגר טוען ש- הואיל והוכחות מתמטיות הן - בסופו של דבר - מניפולציה של סמלים, והואיל ומחשבים יכולים לעשות מניפולציות של סמלים מהר מכל אדם, והואיל ומחשבים יכולים כבר עכשיו להוכיח תוצאות מתמטיות, מכאן שבסופו של דבר מחשבים יוכלו להוכיח כל תוצאה מתמטית, ולעשות זאת מהר יותר מסתם מתמטיקאים. ולכן, מי שרוצה לקדם את המתמטיקה צריך להניח את כל ההוכחות החצי-גמורות שלו בצד, ולעסוק במרץ בתרגום המתמטיקה לשפה שמחשבים מדברים. צל חיוור של הטיעון הזה מצאתי ב עוד על הנושא אפשר למצוא ב- בעיקר "דעות" 37 ו- 47. למשל: 20th century mathematics ... will very soon be completely trivialized and superseded by computer-generated algorithmic mathematics. And much sooner than you think!
|
|
|
|
|
|
|
||
|
||||
|
נחמד שהזכרת את ציילברגר (נדמה לי שכך הוא הוגה את שמו), רציתי לדבר עליו והתעצלתי ואז ארנב אחד שלח לי דואל ועודד אותי לעשות כן. אני אף-פעם לא מצליח להבין בכמה רצינות הוא מתייחס ל-opinions שלו, אבל ברור שהוא אחד המאמינים הגדולים ביכולת של מחשבים לעזור למתמטיקאים מעבר לביצוע "חישובים גרידא". בהקשר שלנו, מעניין גם לראות את ספר הגיאומטריה מהעתיד שיכתוב האלטר-אגו שלו, Shalosh B. Ekhad, בשנת 2050: ספר זה כולל שלל משפטים בגיאומטריה המנוסחים ומוכחים במייפל. דעתי האישית היא שמחשבים אכן ישחקו תפקיד חשוב יותר ויותר בהוכחות משפטים (נדמה לי שכבר הבאתי כמה דוגמאות באייל), אך לא יוכלו "להחליף" את המתמטיקאי האנושי לפני שישיגו אינטליגנציה "אנושית" אמיתית באופן כללי. זה קשור גם לתהליכים אחרים העוברים על המתמטיקה החל מראשית המאה ה-20 לערך: גוף הידע גדל בקצב גבוה מאוד ומתפזר לשלל תחומים שקשה מאוד לאדם בודד לשלוט אפילו בחלק קטן מהם. פעם אפשר היה לפרוץ פריצות-דרך משמעותיות בגיל 17; היום קשה מאוד ללמוד את כל הדרוש כדי להגיע לחזית הידע לפני גיל 23, נניח - פחות או אף יותר, תלוי בתחום. |
|
|
|
|
|
|
||
|
||||
|
נראה לי שעלית כאן על משהו - הייתכן שהידע האנושי יחסם על ידי תוחלת החיים? עם הזמן ידרש יותר ויותר זמן כדי להקיף את הידע בתחום כלשהו והיכולת לחדש תידחה יותר ויותר, עד שתגיע לגיל בו החשיבה האנושית כבר לא תהיה אפקטיבית (במילים פחות מסובכות: סניליות) - ואז מאגר הידע האנושי יתחיל לשאוף אסימפטוטית לקבוע כלשהו? כמובן שאז יהיה ניתן להשקיע בהארכת משך החיים האפקטיביים וביעול טכניקות הלמידה ואיחזור המידע, ואז ניכנס למין מעגל קסמים שכזה. | |
|
|
|
|
|
||
|
||||
|
כן, זה באמת החשש עליו ניסיתי להצביע. יש כמה דרכי-מוצא אפשריות: 1. תוחלת החיים תגדל. 2. היכולת האינטלקטואלית הבסיסית תשתפר. אני מנחש שאם היית לוקח תינוק ממוצע של לפני 10,000 שנה ושם אותו מגיל אפס במסגרת חינוכית מודרנית, הוא היה מתקשה יותר מבן-גילו הממוצע דהיום. 3. היכולת האינטלקטואלית תשתפר באמצעים מלאכותיים, לא אבולוציוניים. מתמטיקאים יוכלו לעבוד מהר יותר עם גרסה חזקה ומהירה של Mathematica מושתלת במוח - שלא לדבר על תוכנות מתוחכמות יותר כמו שהזכרנו. אחת החוויות שאני משתוקק לחוות היא לראות את עולם המספרים הטבעיים דרך מוח המסוגל במבט פשוט אחד, רגעי, לבדוק את השערת גולדבך עד 10^10, או לתפוס באופן גרפי את הפירוק לגורמים ראשוניים של כל המספרים בתחום זה. אין כאן משהו מטפיסי הדורש תהליך אינסופי, סתם מהירות, אך אני מאמין שהעולם פתאום נראה אחרת בתנאים כאלה. 4. אפשרות שאינני אוהב, או אף מאמין בה במיוחד, הוא שהמתמטיקה (או תחומי-ידע אחרים, לא חשוב) לא "תגדל" אלא "תתקדם" כמו הנחש ב-Snake: ידע חדש ייתווסף, וידע ישן יימחק או יצטמצם. יש תחומים מתמטיים שהמתמטיקאי הממוצע במאה ה-19 שלט בהם יותר מהמתמטיקאי הממוצע של היום. האם ניתן לגדל דור של מתמטיקאים היודעים על-פה את כל התוצאות הבסיסיות באינפי, אבל לא מכירים את ההוכחות? זה יכול לחסוך זמן בדרך אל חזית הידע, אך כאמור - אינני מאמין שזה באמת אפשרי. בינתיים, דומה שהידע המתמטי גדל אקספוננציאלית, לא מאט ושואף לאסימפטוטה, אך נדמה לי שיש גם אחרים התוהים מה צופן העתיד. אחד הדברים היפים במתמטיקה הוא הלכידות שלה, הקשרים העמוקים והמסתוריים לעיתים בין תחומים שאין ביניהם לכאורה כל קשר. הילברט נחשב למתמטיקאי האחרון שהכיר לעומק את כל המתמטיקה של זמנו והצליח לגלות תגליות משמעותיות בכל התחומים שהיו קיימים אז. סביר על-כן להניח שהיכולת כיום להפעיל כלים מתחום אחד בתחום אחר היא כבר נמוכה משהיתה. |
|
|
|
|
|
|
||
|
||||
|
לגבי 2: אין שום סיבה שזה יהיה נכון. נראה כאילו המוח האנושי לא השתנה הרבה (אם בכלל) במאה אלף השנים האחרונות. | |
|
|
|
|
|
||
|
||||
|
באמת? איך יודעים? הרי לפני מאתיים אלף שנה או משהו הוא *באמת* היה אחר. אני מקבל שהיתה קפיצה, אבל זה ברור שמאז יש פחות או יותר מצב סטציונרי באזורים ה"מתקדמים"1? (קליפה וכאלה). 1 זה שהאזורים המפיקים סוגים מסויימים של אטימות, או טיפשות, לא השתנו כבר 10,000 שנה - לזה אני מסכים מיד. יש דוגמאות כל הזמן. |
|
|
|
|
|
|
||
|
||||
|
לפי צורת הגולגולת. ברור שזאת לא ראיה מספיקה, אבל זאת השערת האפס שלא הופרכה בינתיים. | |
|
|
|
|
|
||
|
||||
|
טוב, לא ברור לי איך ניתן להפריך את ההשערה הזו. להסתכל על צורת הגולגולת זה קצת כמו פנס-הרחוב ההוא, לא? כלומר, למה ששינויים עדינים אך מהותיים במורכבות של החיווטים ישתקפו בקופסה? הייתי מרחיק לכת ואומר שעצם העקרון האבולוציוני אמור להצביע על כך שיהיה שיפור הדרגתי ביכולת השכלית - בהנחה, כמובן, שיש איזושהי קורלציה תורשתית, ואת זה אפשר אולי כבר לבדוק (אם כי מסוכן משהו). | |
|
|
|
|
|
||
|
||||
|
אתה צודק בעניין החיווט, אלא שאפשר (אולי?) להניח שחיווט שונה יתבטא גם בשוני בצורה הכללית של המוח על מרכזיו השונים, ואלה נותנים את אותותיהם במבנה הגולגולת. לא מאד משכנע, אני מודה; בעצם, ציטטתי את הדעה המקובלת בלי לחשוב עליה יותר מדי. החלק האחרון של ההודעה שלך מניח אבולוציה רציפה של שינויים קטנים, בעוד המוח האנושי התקדם בקפיצות די גדולות שמתאימות יותר לשיווי-המשקל-המופרע של גולד ואלדריג' (שוב, תחת אותה הנחה ששינויים במבנה המוח מתבטאים בצורת הגולגולת). |
|
|
|
|
|
|
||
|
||||
|
איבדת אותי עם גולד ואלדריג'. אני מכיר קצת (ונוטה לקבל) תאוריות של קפיצות, אלא שנדמה לי שהן לא אומרות שאין גם שינויים הדרגתיים קלים. | |
|
|
|
|
|
||
|
||||
|
מה זאת אומרת שיהיה שיפור ביכולת השכלית? ממתי לאבולוציה יש שאיפות לשיפור איכותי? "שיפור" בהקשר של אבולוציה הוא התאמה מוצלחת יותר לסביבה. אולי הסביבה הקיימת "מעדיפה" דווקא שוטים? | |
|
|
|
|
|
||
|
||||
|
אולי. אני מנחש: לא (וסליחה, שכ"ג). או שהתבדחת? (יום ההולדת נגמר, זהו, אין יותר חוש-הומור לשנה). | |
|
|
|
|
|
||
|
||||
|
לא, לא התבדחתי1. מדוע שהסביבה *תמיד* תעדיף אנשים שמבינים מהר יותר מושגים בתורת הגרפים או באזרחות(למשל)? הניחוש שלי הוא כן (לפעמים), למה לא? אני לא מבין את האבולוציה כתהליך שמנסה לשפר משהו או מישהו (או שבו לחכמים יותר יש *בהכרח* יתרון). חוכמה (איך שאנו לא נגדיר אותה במדיוק) היא בסה"כ תכונה (כמו צבע ירוק או פני שטח מחוספסים של עלה) שלפעמים תהווה יתרון (בהקשר של התאמה לסביבה) ולפעמים לא. שיפור לינארי איכותי נראה לי כמו משהו שלא נובע מהתהליך הזה (כפי שאני מבין אותו). ________ 1 נו טוב. בעיקר לא התבדחתי. כמובן שהיתה שם התיחסות/הלצה מרמזת לכיוונו של השכ"ג. |
|
|
|
|
|
|
||
|
||||
|
אני בטח לא מבין את האבולוציה כתהליך ש"מנסה" שום דבר. הוא פשוט, כמו האוורסט, שם. ונכון שתכונות שונות תתאמנה למצבים שונים, ויש ערך גם לסכלות (נגיד, חוסר דמיון קורלטיבי לטפשות ועוזר לא לפחד בשדה הקרב). אבל, זה שאין קשר חד-משמעי בין פקחות לשרידה לא אומר שאין כזה קשר בכלל. אני נוטה להאמין ש, all other things being equal, יהיה לפיקחית יתרון להשיג בן-זוג מוצלח, או בן-זוג בכלל, על-פני חברתה האיטית משהו, ועוד מצבים שהם החריפות - יתרון. "להבין מהר יותר מושגים בתורת הגרפים" זו, מן הסתם, לא תכונה תורשתית מבודדת. היכולת ללמוד מהר, לזכור, להתרכז, להגות פתרונות יצירתיים - כל אלו נראים לי, בגדול, תכונות-מקנות-יתרון. (וכן, אני מסכים, גם השושלת של דן קווייל שרדה, מה לעשות). |
|
|
|
|
|
|
||
|
||||
|
"כִּי בְּרֹב חָכְמָה, רָב-כָּעַס; וְיוֹסִיף דַּעַת, יוֹסִיף מַכְאוֹב" -קהלת א' 18 ייתכן שיש אמיתות מסויימות שעדיף כאורגניזם חפץ חיים (להתרבות עוד ועוד) לא לדעת, וכאן יהנה הכסיל מהיתרון האבולוציוני. דוגמא (יהירה משהו) היא פיקוח הילודה המוּנַע מחשיבה בהירה על רמת חיים גבוהה יותר לתא משפחתי קטן, וכן ממשאביו הסופיים של הכוכב לכת הזה לכלכל אותנו (למשל, הגבלת הילודה בסין). והנה, אוכלוסיות נחשלות מתרבות ומתרבות בקצב גדול בהרבה. כאן, הנחשלות מנצחת את הנאורות. אותו הדין לגבי תובנות שונות אשר עשויות להביא אדם לבחור באורח חיים של נזיר, וכאלו ניתן למצוא במרבית הדתות. בודהא למשל היה נזיר אשר דחה את אהובתו ודיבר באריכות על הפירות של צורת חיים אידאלית זו (אם כי מתוך הבנה שלא הכל ילכו בדרך זו, פנה בדברים גם לבעלי המשפחות). ואם כבר בודהיזם, להבנתי הדלילה והפסימית משהו בנושא, הדבר הנשגב ביותר אליו אדם יכול וצריך לשאוף אליו הוא ההגעה לנירוונה. בהגעה למצב של נירוואנה יוצא האדם ממעגל החיים רווי הסבל וחדל להתגלגל לגלגולים נוספים. אפשר לראות בכך הטפה להתאבדות המושלמת והסופית. האבולוציה כנראה לא מצדדת בהתנהגות שכזו, נכונה ככול שתהה (?). והגיג אחרון בנושא, תיאוריה נושנה שלי בדבר הבסיס האבולוציוני לתחושת ההתאהבות (אזהרה- לא רומנטי במיוחד): זכרים ונקבות שונים אחד מהשני. לא רק במבנה החיצוני אלא גם באופן החשיבה ותפיסת המציאות. למעשה, הם כה שונים זה מזה עד שיש זרות ואף ניכור טבעי מסוים בין המינים. ניתן לראות זאת יפה בילדים, בהם הרב מקובצים בקבוצות מגדר של חבורות בנים וחבורות בנות, או מודעים היטב לשוני באמירות כמו "הבנים על הבנות". החל מגיל הבגרות המינית נוספת בלבלת הורמונלית לחשיבה שלנו והניכור עולה לשיאים חדשים. המינים מגלים שוב ושוב עד כמה "חוּצַן" ולא מובן עבורם המין האחר ומגיבים בתסכול. הניכור הזה בא מההכרה בשוני ונובעת מהכושר המיוחד המאפיין בני אדם בהשוואה לחיות: יכולת חשיבה מפותחת ומופשטת. יוצא איפה, שיכולת זו אשר בדר"כ מסייעת לאדם לייצר כלים, לצוד מזון ולאפשר לו ליישב בתי גידול מגוונים, אותה יכולת גם עשויה להמיט עליו הכחדה ע"י המנעות ממגע מיני 1. כאן בא כפתרון אבולוציוני מנגנון ההתאהבות אשר במכוון משבש את יכולת החשיבה הצלולה שלנו, מסמא אותנו מלתפוס את המציאות באור הרגיל לנו וטורף את החושים שלנו. במצב כזה, אנו חדלים להסתמך על שכלנו ומאפשרים לטבענו הקדום להוביל. אנו באים במגע מיני עם מושא ההתאהבות שלנו מספיק פעמים בכדי לאפשר צאצאים ואז מתפכחים מהחוויה 2, עוזבים את התא המשפחתי, ויוצאים להפיץ את המטען הגנטי שלנו עם פרטנרים חדשים. 1 יפן בצרות (וגם איטליה): http://news.walla.co.il/?w=/18/696351 2 יש מספר מחקרים על הבסיס הכימי במח להתאהבות (אאל"ט - מולקולה בשם f.a.t) ועל פרק הזמן הקצוב שלה (עד שנתיים) |
|
|
|
|
|
|
||
|
||||
|
דיון 1601 (החלק השני) | |
|
|
|
|
|
||
|
||||
|
|
|
|
|
|
|
||
|
||||
|
יחסית להסבר מדעי על התאהבות, דווקא נשמע לי די רומנטי (לפחות עד החלק של ההתפכחות): "היית יכולה להיות כמו חוצן בשבילי; מזל שאני אוהב אותך". | |
|
|
|
|
|
||
|
||||
|
לא הייתי ממליצה לך לנסות את המשפט הזה על נשים. מושגיך על רומנטיקה נשמעים לי בעייתיים משהו. | |
|
|
|
|
|
||
|
||||
|
זה בסדר, ירדן כבר נשוי, ועם נישואיו אימץ את שם משפחתה של אשתו במקביל לשם משפחתו (מקודם זה היה רק ירדן ניר), כך שיש לא מעט אנשים שיסיקו שהמושגים שלו על רומנטיקה הם בריאים ונכונים. | |
|
|
|
|
|
||
|
||||
|
חדשותיך ידועות לי. נדמה לי שדבריי נאמרו באותה רוח שבה נאמרו דבריו של ירדן. | |
|
|
|
|
|
||
|
||||
|
טוב, אז שוב יצאתי גולם. הרי מישהו צריך לצאת. | |
|
|
|
|
|
||
|
||||
|
"הוכחות מתמטיות הן - בסופו של דבר - מניפולציה של סמלים" וזה בניגוד למוזיקה או ספרות? |
|
|
|
|
|
|
||
|
||||
|
למרבית הפליאה ( לכאורה) הרבה יותר *קל* לפרמל ולמכן את המניפולציות הדרושות כדי להוכיח משפטים מאשר לפרמל ולמכן את המניפולציות הדרושות ליצור סיפור(אם כי גלילה רון-פדר-עמית כנראה הצליחה) או נעימה. | |
|
|
|
|
|
||
|
||||
|
אף אחד לא אמר (בטח לא אני :-) ) שלא ניתן לשכנע מחשב לבצע מניפולציות של סמלים שיהיו, או ייראו כמו, ספרות או מוזיקה. עם זאת, קצת יותר קל להניע מחשב לייצר מתמטיקה "טובה" מספרות טובה או מוזיקה טובה. לא *הרבה* יותר קל, אגב. הזכרתי קודם את תחושתי שמחשב שיוכל לגלות לבד את המספרים המרוכבים, נניח, ולהוכיח את משפט קושי, יכול כנראה גם לכתוב שיר קצר. | |
|
|
|
|
|
||
|
||||
|
צריך להיות "מניפולציות *סופיות* של סמלים", במובן האלגוריתמי. אנחנו לא יודעים מה זה שיר, אבל הוכחה היא סדרה סופית של טענות, שאפשר לבדוק את הנכונות שלה בקלות. למשל, בלוגיקה מסדר ראשון אפשר לעבוד כך. תהי A קבוצה של אקסיומות. "הוכחה" היא סדרה של טענות, כך שעבור כל טענה a שאינה אקסיומה, מופיעות מוקדם יותר ברשימה הטענות "b גורר a" ו- "b" לאיזשהו b. אם מספר האקסיומות סופי (כמו בלוגיקה פסוקית או לוגיקה מסדר ראשון), המחשב יכול לעבור על כל ההוכחות באורך 1, אחר-כך כל ההוכחות באורך 2, וכן הלאה - עד להוכחת כל טענה שאפשר להוכיח. |
|
|
|
|
|
|
||
|
||||
|
(כמובן שגם אם מספר האקסיומות הוא אינסופי אך בן-מנייה, כמו בניסוח מסדר ראשון של תורת המספרים, אפשר לייצר סדרתית את כל ההוכחות). | |
|
|
|
|
|
||
|
||||
|
וגם אפשר לייצר את כל השירים באורך תו, שני תווים וכולי. הבעיה בשני המקרים זה לזהות מתי המשפט מעניין והשיר שווה. בשני המקרים העניין דורש התערבות אנושית. היתרון במשפטים זה שאפשר לשאול " האם אפשר להוכיח או להפריך טענה X בפחות מ N צעדים", להציב בתור X משהו "מעניין" וללחוץ על כפתור ה"RUN". בקיצור, התוכנית (המדכאת לטעמי) זה להפוך את המתמטיקה לפיתרון בעיות שחמט באמצעות מחשב. ספקולציה: בעתיד יתפתח ענף במתמטיקה שיעסוק בבנית היוריסטיקות ניפוי טובות למכונות ההוכחה. |
|
|
|
|
|
|
||
|
||||
|
אין סיבה להיכנס לדיכאון, אין באמת תכנית (או אפשרות מעשית) להפוך את המתמטיקה לפתרון בעיות-שחמט באמצעות מחשב. למעטים העוסקים בבניית מערכות-הוכחה יש, בינתיים, יומרות מצומצמות בהרבה. | |
|
|
|
|
|
||
|
||||
|
מעניין איזו השפעה תהיה למערכות כאלה על המתמטיקה (כמו ההשפעה של המצאת המצלמה על הריאליזם?) | |
|
|
|
|
|
||
|
||||
|
אני חושב שכבר יש ענף כזה במתמטיקה, למעשה אחד הענפים הלוהטים-מסחרית שלה: הוכחת נכונות אוטומטית של מעבדים (ושל תוכנות; קצת פחות לוהט). אני לא יודע על זה בדיוק, למרות שבמשרדים מסביבי יושבים הרבה אנשים שזה בדיוק מה שהם עושים, אבל אאל"ט הם בונים טענות בלוגיקה טמפורלית, ואז מנסים (לגרום למחשב) להוכיח או להפריך אותן. ומכיון שהבעיה היא קשה חישובית, משתמשים בהיוריסטיקות, ושם המשחק הוא חידוד ההיוריסטיקות. יכול להיות שטענות כלליות במתמטיקה, ולא כל שכן טענות מעניינות, שונות באופיין מטענות הנכונות של מעבדים, ושלכן הן דורשות היוריסטיקות שונות; אבל במחשבה ראשונה נראה לי שלא, שלאחר תרגום לשפה הפורמלית היבשה אלה וגם אלה יראו סתם כמו רצף משמים וטכני של סמלים, אותו דבר עבור המחשב. בעצם, לאור תגובה 214540 (המשפט האחרון בה), אני כנראה מחמיץ משהו. מה? |
|
|
|
|
|
|
||
|
||||
|
זה שטענות מתמטיות "נראות אותו דבר", אחרי פירמול, כמו טענת נכונות של מעבדים ותוכנות, זה לא אומר שיש להן (כיום) אותו עומק - אם תרצה, מורכבות ההוכחות שונה מהותית בין המקרים. כמו כן, יש להבדיל בין תהליך גילוי המשפטים והמבנים העמוקים, להוכחות עצמן; ראובן חשש מרדוקציה של המתמטיקה לחידת-שח, וגם זה הבדל שכדאי להביא בחשבון. התהליך שמתחיל מאקסיומות ומייצר הוכחות יוכיח אמנם בסופו של דבר את כל המשפטים ב(נניח) תורת המספרים, לפחות את אלו היכיחים במסגרת הפורמלית בה הוא עובד. אבל זו טענה דומה קצת לטענת הקופים ומכונות-הכתיבה - נכון, ברם ממש ממש ממש לא מעשי. את ההיוריסטיקות הדרושות כדי להפוך מוכיח עיוור כזה למתמטיקאי אנחנו עוד לא מבינים, ותחושתי היא (שוב) שנבין אותן בערך באותה שנה בה נדע לבנות אינטליגנציה-מלאכותית על באמת. גיאומטריה של המישור היא דוגמה מטעה קצת. לא ידוע לי על מערכת הוכחה שמתחילה ממעט מאוד ומסוגלת להוכיח אפילו טענה פשוטה כמו (נניח, סתם) שיש פערים גדולים כרצונך בין ראשוניים עוקבים, שלא לדבר על "כל ראשוני המשאיר שארית 1 בחלוקה ל-4 הוא סכום של שני ריבועים" ומשפטים פשוטים-יחסית שכאלה, הדורשים קפיצה מחשבתית רצינית. וזו באמת רק ההתחלה... |
|
|
|
|
|
|
||
|
||||
|
מקבל (שכאתה אומר "מערכת הוכחה" בפסקה האחרונה אתה מתכוון למחשב + תוכנה, נכון? לא למערכת פורמלית מופשטת.) | |
|
|
|
|
|
||
|
||||
|
(כן, ודאי). | |
|
|
|
|
|
||
|
||||
|
אני רק רוצה להוסיף "הערת אזהרה" כאן. האמירה "את ההיוריסטיקות הדרושות כדי להפוך מוכיח עיוור כזה למתמטיקאי אנחנו עוד לא מבינים, ותחושתי היא (שוב) שנבין אותן בערך באותה שנה בה נדע לבנות אינטליגנציה-מלאכותית על באמת" נשמעת לי בדיוק מה ששחמטאי טוב היה אומר לפני 30 שנה לגבי תוכנות שח, והנה, תוכנות שח שמנצחות רבי אמנים הן דבר כמעט יום יומי, ובכל זאת אנחנו די רחוקים מהשנה בה נוכל לבנות א"מ *על אמת*. בקיצור, יש משהו שובניסטי בדעה שיש ב*מתמטיקה* משהו קווזי מיסטי, וכש*נבין* אותה *באמת* , נבין מה זה אינטלגנציה. אני חושב שמקור התחושה שלך היא שיש משהו "יצירתי" במתמטיקה, וכשנדע לפענח את היצירתיות הזאת נהיה על הסוס לקראת יצירתיות בכל תחום. השאלה הגדולה היא האם כל מה שמייצר פיתרונות יצירתיים אכן נחן ביצירתיות? אין עוררין שתוכנות שח 1 מייצרות לעיתים מהלכים יצירתיים, אבל כולנו מבינים שהתהליך שהמכונה עושה שונה בצורה מהותית ממה ששחמטאי עושה. ועוד עניין קטן, מכיוון שדנים כאן בענייני אבולוציה ואינטלגנציה, לעניות דעתי, כישרון מתמטי ויצירתיות מתמטית הם סרח עודף אבולוציוני והמוח האנושי הוא לא מי יודע מה מותאם לזה, פשוט יצא ככה. למה שמכונה לא תיטיב לייצור מתמטיקה (ומתמטיקה טובה)? 1 דיסכליימר, הפעם האחרונה ששיחקתי שח היה בגיל 10 וגם אז הפסדתי. |
|
|
|
|
|
|
||
|
||||
|
היה באמת מישהו שחזה שמחשב לא יוכל אף-פעם לשחק שח ברמה סבירה, ומזכירים זאת לפרקים בתור אזהרה לפסימיים. אבל אני מאמין שמעט אנשים שיודעים משהו על שח ומחשבים היו צופים את מה שאמרת לפני 30 שנה. שח זה מסובך, יצירתי ויפה, אבל מוגבל מאוד מאוד בהשוואה למתמטיקה (או שירה, או אפילו תרגום). את ההאשמה בשוביניזם ובקוואזי-מיסטיות אני מוכרח ממש לדחות :-) הדגשתי שמדובר בתחושה שלי, וייתכן שאני טועה, אבל אני סבור שאני מכיר מתמטיקה (ושח) טוב מספיק כדי לטעון זאת ברמת-ביטחון סבירה. "מכיר מתמטיקה" לא מתייחס לידיעת החומר, אלא לתהליך בו מתמטיקאים ממציאים ומגלים ומוכיחים; קטונתי כנמלה (באמת), אבל יש לי מושג לגבי איך זה קורה. וכשיש שם יצירתיות, אני מתקשה לראות מדוע זו יצירתיות "אחרת" מסוגים אחרים של יצירתיות אנושית. "האם כל מה שמייצר פיתרונות יצירתיים אכן נחן ביצירתיות" זו שאלה בעייתית קצת, בעיני. מי קובע שהפתרון הוא יצירתי? אולי הניסוח הזה מצביע על אחד הקשיים שאני רואה ב-AI, ונדמה לי שכבר הזכרתי אותו פעם: מי שירצה להתעקש ולטעון שמחשב אינו יצירתי ואינו מרגיש ואינו אינטליגנטי, יוכל תמיד להמשיך להתעקש ואין דרך להוכיח לו אחרת. אני ממש לא מסכים שכישרון מתמטי ויצירתיות מתמטית הם סרח עודף - כפי שציינתי, אלו לא דברים שבאים לבד אלא קשורים לתכונות כלליות יותר בעלות השפעה שרידתית משמעותית. (שוב, רק תחושה, לא משפט מתמטי). "למה שמכונה לא תיטיב לייצור מתמטיקה (ומתמטיקה טובה)?" - מי אמר שלא? אני מאמין ש"מכונה" (לא יודע איך להגדיר זאת, תינוק-מבחנה שגדל ברחם מברזל זו מכונה?) תיטיב יום אחד גם לקפל כביסה וגם להוכיח משפטים. למה לא? |
|
|
|
|
|
|
||
|
||||
|
תהליך מחשבתי של שחקן שח, יצירתי ונשגב ככל שיהיה, נגמר בסוף בפרש לגימל ארבע. מחשב יכול לחקות את התשובה הסופית הזו, ולך תסביר אם הוא הבריק או שסתם בדק מיליארד אפשרויות. במתמטיקה, בשביל הוכחות קשות באמת המתמטיקאי ממציא לעיתים תורות שלמות שפשוט לא היו שם קודם (Kummer, אחד מגיבוריי, הוא דוגמה מופלאה). כשמחשב יעשה את *זה*, לא יהיה לי אכפת "איך" הוא הגיע לזה - בעיניי הוא עבר את מבחן טיורינג. |
|
|
|
|
|
|
||
|
||||
|
אל"שחמטאי אבל תהליך המחשבה של שחקן שחמט לא מסתיים במהלך בודד אלא מתבטא לאורך כל המשחק, ממש כמו שהוכחה *יפה* מתבטאת באוסף כל השלבים. כבר היצעתי בתגובה אחרת מבחן טיורינג לשחמטאים. אני מאוד מופתע שאתה דורש ממכונה דברים שאתה לא דורש ממתמטיקאי אנושי. "להמציא תורה שלמה שפשוט לא היו שם"? כמה מהמתמטיקאים הפעילים היום עושים יותר מאשר ארטיקולציה אינפינטסימלית של פרדיגמה זו או אחרת? וכל האחרים אינם אינטלגנטים? |
|
|
|
|
|
|
||
|
||||
|
לא הובנתי כהלכה, והאנלוגיה בין סדרת מהלכים בשח לסדרת צעדים בהוכחה אינה מדוייקת. אם אתה ניצב מול מסך שמשחק שח ותוהה עם מאחוריו אדם או מכונה, התוכן שאתה מביט בו הוא סדרה של צעדים כמו Nf3 O-O וכאלה. אם אתה ניצב מול מסך שמוכיח משפט במתמטיקה, אתה רואה פרוזה, ולא בכדי. אם תראה סדרה ארוכה של סמלים לוגיים, תדע מיד שמדובר במחשב (פרימיטיבי). העובדה שלמדנו כבר כיצד לפרמל טיעונים מתמטיים, אין דבר בינה לבין הדרך בה אנשים באמת חושבים על בעיות מתמטיות, וזה שורש הפער בין מערכות-הוכחה-ממוחשבות דהיום לבין אינטליגנציה מתמטית אמיתית. קח לדוגמה את החידה ששאלתי פה לא מזמן, על הצפרדעים. האיילים שפתרו אותה הפגינו יצירתיות, משהו שונה מהותית מהיכולת לעשות מניפולציה של שרשראות של סמלים. אם מישהו היה מנסה לפתור את החידה ע"י שהיה מפרמל את הנתונים ומתחיל לעשות תחשיב פסוקים ומודוס-פוננסים, הוא גם היה נכשל (מסיבות פרקטיות) וגם, אילו הצליח, ההוכחה שלו היתה משהו שאף בן-אנוש לא יכול להבין. איני יכול למצוא אנלוגיה למצב הזה בשחמט - ומבחינה מתמטית, מדובר בחידונת קטנטונת עם פתרון קצרצר ביותר. לכן גם אינני דורש מהמכונה דברים שאיני דורש מאנשים. אולי הדוגמה של קומר היתה נשגבת מדי: כל מתמטיקאי, בכל מאמר שהוא מפרסם (כמעט) ובכל חידה שהוא פותר (כמעט), ממציא המצאות (קטנות או גדולות) שאינן "מכניות", במובן שהן אינן גיזום היוריסטי מחוכם של עץ-כל-ההוכחות-הפורמליות-האפשריות. לא ברור לי למה כוונתך ב"ארטיקולציה אינפינטסימלית של פרדיגמה זו או אחרת", אבל אם אני מנחש נכון, אז לא - זה לא המצב, כלל וכלל לא. נכון, לא כולם ממציאים כל יום את תורת האידאלים, אבל בפירוש גם לא מתקדמים באופן מכני או חצי-מכני לאורך איזו פרדיגמה נתונה. אילו זה היה המצב, היה אפשר להתחיל לבנות מחשב-מתמטיקאי; אי-אפשר, לא כי חסר כוח חישוב או איזו היוריסטיקה, אלא כי הבנה של תהליכי המחשבה הנחוצים *באמת* לצורך זה אינה בנמצא, אפילו לא בחיתוליה. וכשההבנה הזו תגיע, אני לא מאמין שהיא תגיע במבודד מהבנה של חשיבה יצירתית באופן כללי. זה כל מה שאני טוען. הקשר בין מכונות-ההוכחה הפורמליות של היום להוכחות של מתמטיקאים אנושיים הוא דומה מאוד לקשר בין תוכנות מחשב שכותבות שירה למשוררים אנושיים. למעשה, השני אפילו יותר מוצלח: הפלט של תוכנות השירה נראה כמו שירה. הפלט של תוכנות ההוכחה נראה כמו פלט של תוכנת הוכחה, וכשמחשב יוכל להסביר בעברית פתרונות לחידות, אני אומר שוב - הוא יהיה מוכרח להיות אינטליגנטי "באמת". |
|
|
|
|
|
|
||
|
||||
|
כתבתי תגובה מאוד ארוכה, אבל ראיתי שאני מסתבך ושמתי את זה בצד. במקום זאת אגיד משהו קצר על יצירתיות. אני מסכים שיצירתיות במתמטיקה נובעת מאותו מקור של יצירתיות בכל תחום. העניין הוא שבנוסף ליצירתיות, צריך גם סוג מסויים מאוד של מיומנות טכנית. השאלה היא האם אפשר להפריד בין היצירתיות לבין המיומנות. נדמה לי שהגישה שלך היא שגם את המיומנות אי אפשר להעביר למכונה, ושהתסריט של דיליטנט מקורי ויצירתי שמעלה השערות אבל המכונה "מוודאת" אותם הוא לא סביר ( ע"ע השערת X והשערת Y). את הדאגה שלך על הוכחות מסובכות שאי אפשר להבין, תן לי לנסח ( ותוך כדי כך, לעוות לצרכי) בצורה אחרת: יש דיליטנט מקורי ששואל שאלה מרתקת בתורת המספרים ( נניח), ולאחר כעשרים שנה, זוכה אדם במדלית פילדס בזכות ההוכחה המבריקה שהוא נותן לשאלה הנ"ל, תוך כדי זה שהוא פותח אופקים מדהימים בתחומי מתמטיקה מגוונים. אותו מתמטיקאי נותן כאות הוקרה את עותק ההוכחה שלו לדיליטנט ששאל את השאלה במקור, ואותו דיליטנט חלשה דעתו מהקריאה, ונאלץ להודות שהוא אינו מבין דבר1. עכשיו מה? האם נכשל זוכה המדליה מכיוון שלא הצליח לתת הוכחה ברמה של האדם שניסח את השאלה? האם ההוכחה שלו פחות שווה משום כך? ועוד משהו בקשר לשובניזם: לא התכוונתי במלא הרצינות חלילה ( אני מתבדח גם שאין לך יום הולדת:)) .אבל שקול את הדוגמא הבאה: נדמה שאיזה מתמטיקאי אמר פעם על בעיה מפורסמת עם הוכחה "מכוערת" -" מסתבר ככלות הכל,שזאת לא היתה בעיה טובה". למזלם של המתמטיקאים הטהורים יש להם את הלוקסוס של להגדיר כל בעיה שההוכחה שלה לא מוצאת חן בעיניהם כ "בעיה לא טובה ככלות הכל". 1 הכנס כאן את האגדה על משה ועקיבא. |
|
|
|
|
|
|
||
|
||||
|
אינני טוען שאי-אפשר להעביר לפחות חלק מן המיומנות הטכנית למחשב, עושים זאת כבר היום. להמציא הוכחה (וגם לשער השערה מעניינת) דורש סוג של יצירתיות החורג מן המיומנות הטכנית הזו. את הדוגמה עם הדילטנט ממש לא הבנתי. איפה העליתי את הצורך לדאוג שפתרון של בעייה יהיה מובן למי שהמציא אותה? נהפוך הוא - הוכחות יפות הן בד"כ עמוקות הרבה יותר מהשאלה. אני זוכר במעורפל את הסיפור שהזכרת בסוף, אך איני סבור שפירשת אותו נכונה. בעיות אפשר להמציא בקלות, אך רובן "אינן טובות" לא כי הן קלות, או כי ההוכחה שלהן מכוערת, אלא כי הן מבודדות ולא תורמות להבנתנו הכללית של היקום המתמטי. יש, לעומתן, בעיות המנסות לתפוס איזושהי הבנה עמוקה שחסרה לנו, שדי ברור שאם נפתור אותן - נתקדם באמת. גם את עניין ה"לוקסוס" לא הבנתי... "לא מוצאת חן" בעיני מי? ברוב המקרים יש די הסכמה לגבי היופי או החשיבות של תוצאה מתמטית, וגם נדמה לי שהזכות לשפוט יופי שמורה גם לפיזיקאים ולמלחינים, בתחומם. דווקא את התגובה הארוכה שהשמדת אני סקרן לראות, כי נראה לי שאני מפספס משהו שמפריע לך. |
|
|
|
|
|
|
||
|
||||
|
העניין עם הדיליטנט הוא פשוט: כמו שהדיליטנט לא מבין את ההוכחה, למרות שהיא "יפה" למבינים בהוכחות, גם הוכחה ממוחשבת לא צריכה להיות נהירה (או אפילו "יפה") למתמטיקאים אנושיים. מספיק שהיא נכונה. שפת מכונה היא קשה להבנה, אבל בכל זאת אפשר לעשות איתה דברים יפים. הלוקסוס זה לא להחליט אם תוצאה היא "יפה" או לא, אלא אם הבעיה "טובה" או לא. אולי זה עניין של דרגות- אני מודה שבמדעים שאני יותר מכיר יש מושג של בעיה "טובה" במובן של פוריה מבחינת יכולת ההתקדמות בה, אבל יש גם מקרים אחרים. אני מתקשה לדמיין חוקרים רפואיים אומרים משהו כמו "סרטן? אה, זה בעיה לא טובה, לא תורמת להבנת היקום, עדיף להתמקד בפצעי בגרות". אם אני כבר מלהג, עוד עניין קטן וקצת לא קשור בקשר ל"יופי" ו"פשטות" של תאוריות כקריטריונים. נהוג להצהיר על שתי התכונות הללו כקווים מנחים בפיתוח תאוריות. אני חושב שיש להיזהר כאן.תלמיד שנה א בפיסיקה עלול לחשוב שיחסות כללית זה חשבון טנזורים מכוער ומסובך לעומת הפשטות הניוטונית. הרבה תאוריות הם מאוד מסובכות "טכנית" ודווקא בכך היופי שלהם, אבל כדי להעריך את היופי צריך הבנה טכנית מאוד עמוקה, והרבה פעמים ההצהרה על "פשטות" באה מאנשים כל כך מוכשרים שמה שבעיניהם פשוט, הוא בלתי מובן לאחרים. מה אני מנסה להגיד? שלא רק יופי הוא בעיני המתבונן, אלא גם פשטות, ולנסות להשתמש בשני הקריטריונים הללו בבואנו לבחור בין תאוריות "מתחרות" כמו שכתוב בספרים המפארים את השיטה המדעית, הוא לא טריוויאלי. לא צריך יותר מדי לדאוג שמה שמצאנו הוא מסובך או "מכוער". אולי פשוט צריך להתרגל לזה. |
|
|
|
|
|
|
||
|
||||
|
דילטנט: עכשיו הבנתי, אבל יופיה של ההוכחה לא עומד אצלי במרכז הטיעון. כתבתי "אם מישהו היה מנסה לפתור את החידה ע"י שהיה מפרמל את הנתונים ומתחיל לעשות תחשיב פסוקים ומודוס-פוננסים, הוא גם היה נכשל (מסיבות פרקטיות) וגם, אילו הצליח..." - החלק הראשון הוא באמת העיקר. רופאים לא עוסקים בהבנת היקום, אלא בהבנת גוף-האדם וריפוי מחלות. בהקשר הזה, אני מאמין שהם בהחלט מעדיפים בעיות עקרוניות על-פני תופעות שוליות וספציפיות, ומסתמא עוד קריטריונים שהופכים תחום-מחקר ל"יפה" בעיניהם. בעניין היופי והפשטות, אני מסכים: אין קריטריון טריוויאלי להכרעה. אבל לפעמים יש מדדים מאוד אובייקטיוויים לפשטות - נפח ההצגה, מספר המשוואות, מספר הקבועים השרירותיים, וכאלה. נכון שבעל הבנה טכנית עמוקה יראה את זה אחרת מסטודנט בשנה א'. ויותר מזה, אף אחד לא הבטיח לנו גן של תאוריות פיסיקליות יפות ופשוטות: ייתכן שהיקום הוא באמת מכוער ומסובך. אם כך, חבל. |
|
|
|
|
|
|
||
|
||||
|
(רקע קצר: בנסיון להוכיח את משפט פרמה, Kummer הבחין שמספר שלם אפשר לאפיין באמצעות אוסף המספרים שהוא מחלק; אם כך, הוא הציע, אפשר לטפל ב"מספרים אידיאליים"1, האוספים האלה, במקום המספרים המקוריים. האבחנה הקריטית כאן היא שישנם אוספים של מספרים שמתנהגים בדיוק כמו "מספרים אידיאליים", אבל אין להם מספר "אמיתי" שמחלק את כולם.) ממבט ראשון חשבתי ש- Kummer הוא דוגמא לא מוצלחת, משום שהרעיונות שלו (בדיעבד, כמובן) הם מאד טבעיים. הוא "בסך הכל" ניסה לענות על שאלות קלות הקשורות למספרים הטבעיים, עבור מספרים שלמים "אחרים". במקום זה, אפשר לבחור דוגמא מבין המספר העצום של תאוריות שלא מכלילות שום דבר, הן *באמת* לא היו שם קודם. למשל, פולינומי Jones, שמדביקים פולינום לכל קשר2, ומאפשרים לנו להוכיח שקיימים קשרים השונים זה מזה. אבל במבט שני, Kummer הכניס לתאוריה רק אטום אחד חדש, והגיע לתוצאות מדהימות. צריך להתחיל בקטנות... 1 שאחר-כך הפכו ל"אידיאלים". 2 קשר = שרוך ששני קצותיו מחוברים. 3 נסו *להוכיח* ש"תלתן שמאלי" ו"תלתן ימני" הם שונים, דהיינו שאי אפשר לעבור מאחד לשני בלי לצאת מהמרחב שלנו או לקרוע את השרוך. |
|
|
|
|
|
|
||
|
||||
|
הפולינומים של ג'ונס הם באמת דוגמה יפה, אבל הרקע להופעתם הוא יותר מורכב; ג'ונס בכלל לא הסתכל על קשרים, אלא על אלגבראות פון-נוימן, ועשה סדרה מופלאה של המצאות וקפיצות מחשבתיות. אני לא מבין מספיק (קרי: אני לא מבין כלום) בשורש האלגברי של המצאתו כדי לקבוע אם זה היה "טבעי, בדיעבד" כמו התורה של קומר. | |
|
|
|
|
|
||
|
||||
|
אם כבר, הפולינומים של ג'ונס מכלילים את הפולינומים של אלכסנדר, כך שגם הם לא ממש נולדו יש מאין. בכל אופן נראה לי שהבהרנו את הנקודה העיקרית (שהיא: מתמטיקאים יכולים לדבר שעות על משהו שמעניין רק אותם). | |
|
|
|
|
|
||
|
||||
|
אני מקווה שבאמת הבהרנו את הנקודה העיקרית (אבל צריך לשאול את ראובן). (ואת הנקודה שהזכרת בסוגריים הבהרנו כבר מזמן, ועוד לא באמת התחלנו...) | |
|
|
|
|
|
||
|
||||
|
אם כבר שוב שורבבתי לדיון, אני רוצה להגיד שמלכתחילה הבנתי את ההערה של עוזי על פירמול המתמטיקה כהערה שנאמרה בבדיחות הדעת, ושברור לי שהמתמטיקה רחוקה מאוד ממצב של סריקת כל הביטויים שאפשר לגזור מאקסיומות נתונות. יחד עם זאת, הרעיון הבסיסי הצית את דמיוני ולכן הפלגתי בכיוון של מכונות הוכחה ושובניזים של מתמטיקאים. | |
|
|
|
|
|
||
|
||||
|
כל אחד יכול לדבר שעות על מה שמעניין (רק) אותו. המתמטיקאים מצטיינים בכך שהם יכולים גם לשתוק שעות (או שנים, ראה ווילס) על משהו שמעניין אותם. ______________ שכ"ג מלמד את עוזי דבר או שניים על מתמטיקאים :-) |
|
|
|
|
|
|
||
|
||||
|
ווילס הוא לא חריג? אני חושב שבספר יחסי הציבור שלו (סליחה, "המשפט האחרון של פרמה") דווקא מדברים על המתמטיקאים כדברנים יחסית (ברמה המקצועית) כי אין אצלם חשש מגניבת פטנטים. הממ, RSA זה לא פטנט? |
|
|
|
|
|
|
||
|
||||
|
"ספר יחסי הציבור שלו"? העובדה שויילס בחר לעבוד בבידוד היא אכן יוצאת-דופן, אבל הנסיבות היו לא שגרתיות. אני לא סבור שמתמטיקאים הם יותר דברנים מאקדמאים אחרים, והסיבה העיקרית להיות בשקט, אם כבר, זה לא פטנטים אלא החשש מלהיות scooped. |
|
|
|
|
|
|
||
|
||||
|
בדיחה, בדיחה. מאוד אהבתי את הספר, וגם את "סודות ההצפנה". מה זה scooped? |
|
|
|
|
|
|
||
|
||||
|
נגנב. יענו, רגע לפני שאתה מסיים, מישהו אחר שעקב אחר צעדיך כותב יותר מהר את המ.ש.ל., מפרסם וזוכה בתהילה (כמו מישהו שגונב לך איזה סקופ בעיתון). | |
|
|
|
|
|
||
|
||||
|
לא, סקופ זה לא גניבה, זה פשוט מישהו שהקדים אותך, לאו דווקא בשל משהו לא הוגן. נניח ששני מדענים פותרים אותה בעיה ושולחים לפרסום בעיתונים שונים, מבלי שאחד יודע על השני או מבלי לדעת שהאחד כבר פתר את הבעיה ששניהם עובדים עליה. | |
|
|
|
|
|
||
|
||||
|
למה אתה מתכוון ב-"אינטליגנציה-מלאכותית על באמת", או בניסוח אחר, מה אתה תופס כ- "אינטליגנציה אמיתית"? חבר שלי (המביא לכך דוגמאות למכביר) טוען שברגע שמחשב מצליח לבצע פעולה מסויימת שקודם לכן רק בני-אדם יכולים היו לבצע, אוטומטית אותה פעולה כבר לא נחשבת כ"בינה". ואם זה כך, אז יוצא שכל הדיבור על "בינה אמיתית", המצויה כביכול אצל בני-אדם, היא בעצם סוג של מס-שפתיים, או לפחות סוג של בלבול מושגי מבחינה פילוסופית. | |
|
|
|
|
|
||
|
||||
|
הטענה הזאת מוכרת, אבל אפילו אם נקבל אותה כפשוטה בסופו של דבר ניאלץ להכיר בכך שיש בינה מלאכותית או שאין ''בינה'' בכלל. זאת בהנחה שהמחשב יוכל, בסופו של דבר, לעשות כל מה שהאדם עושה (לי אין ספק שזה יקרה מתישהוא, אבל חוששני שלא אהיה בסביבה לאנשלבץ אתכם). | |
|
|
|
|
|
||
|
||||
|
החלוקה הזו בין "מחשב שמבצע פעולה מסוימת" לבין "בינה" הזכירה לי את ג'והן וואטסון, האבא "הרשמי" של התורה ההתנהגותית (ביהייויוריסטית). וואטסון, שהיה חוקר התנהגות בעלי חיים, כתב בשנת 1913 את מה שנחשב למניפסטו המייסד של הזרם ובו הוא טען שעפ"י הראיה הביהייויוריסטית היא "ענף אובייקטיבי של מדעי הטבע... לאינטרוספקציה אין שום ערך מדעי... [ולכן] אין שום קו מהפריד בין אדם לחיה". עפ"י השיטה, יש ערך ומשמעות רק להתנהגות החיצונית של האובייקטים - אדם, חיה, ומקרה שלנו - מכונה - ולכן אסור "לעולם להשתמש במונחים כמו תודעה, מצב מנטלי, נפש, תוכן [המחשבות], אישור אינטרוספקטיבי, דמיון וכיוב"'. הדברים היחידים שניתן ושצריך לבדוק הם "גירוי ותגובה, עיצוב מערך של הרגלים, שילוב הרגלים וכדומה", משום שרק אותם ניתן למדוד. |
|
|
|
|
|
|
||
|
||||
|
בהקשר הנוכחי, ב"אינטליגנציה אמיתית" התכוונתי לומר משהו שמקיף עוד מתחומי המחשבה האנושית, למשל יכולת לנהל שיחה, למצוא מטפורות וכו'. כלומר, ניסיתי לטעון שלא ניתן לבודד את היכולת לחקור תחום מתמטי ולדון בו עם בני-אדם מ"סממנים" אחרים של אינטליגנציה. העמדה שמציג החבר שלך מוכרת לי היטב, וכבר הזכרתי אותה כמה פעמים מעל דפי האייל - מי שירצה להיות "שוביניסט אנושי" יוכל תמיד לטעון שכל מה שאינו ילוד-אישה אינו "באמת" מרגיש, אינו "באמת" חושב, או אף אינו "באמת" רואה. אי אפשר כמובן להוכיח את ההיפך. כל אחד מאיתנו מאמין שהוא עצמו בעל התכונות הללו, ואנו מוכנים להשליכן על חברינו בשל היותם דומים לנו חיצונית ונראים מתפקדים באופן דומה. אין לנו, ולא תהיה לנו עד כמה שאני מסוגל לראות, עדות אחרת. הגישה הזו באמת מעקרת את התוכן משאלת ה"בינה", ולכן לדעתי היא לא גישה מעניינת במיוחד. אני חושב שדבר דומה ניסה לומר Dijkstra בציטוט שכבר הבאתי פעם: "השאלה אם מכונות יכולות לחשוב דומה לשאלה אם צוללות יכולות לשחות". (אגב, אני גם סבור שה"איש ברחוב" שיישאל האם מכונה מסויימת היא אינטליגנטית או בעלת רגשות, ייתן את רוב המשקל למראה החיצוני, ומשקל נמוך יחסית למבחן-טיורינג. צור רובוט הנראה כמו נערה צעירה, מתנועע כמו נערה צעירה, מסוגל לדמוע ולצעוק אך בקושי לדבר, ותמצא הרבה פחות אנשים שיהיו מוכנים להתעלל בו פיזית מאשר במשהו שנראה כמו ארון בגדים אבל מנהל שיחה אינטליגנטית. על-כן אין ברירה, בעיני, אלא להשתמש במשהו דמוי מבחן-טיורינג כדי לקבוע הימצאותה של בינה, אם כי המבחן המקורי גם הוא יש בו פגמים). |
|
|
|
|
|
|
||
|
||||
|
ספר נחמד מאוד על זהויות מתמטיות ואיך להוכיח אותן באמצעות מחשב ( רק רפרפתי אבל מה שראיתי מאוד מצא חן בעיני): |
|
|
|
|
|
|
||
|
||||
|
דורון ציילברגר כבר הוזכר כמה פעמים בדיון (למשל, בתגובה 214282). ותיקון קטן לתגובה ההיא: שלוש ב. אחד אינו האלטר אגו שלו אלא המחשב/תוכנה שלו. יש לו כמה וכמה מאמרים עליהם הם חתומים במשותף וכמה של אחד בלבד. |
|
|
|
|
|
|
||
|
||||
|
נדמה לי שאני זוכר שאלה ב-Monthly שפורסמה ע"י שלוש ב. אחד לבדו. לא נראה לי כמו משהו שהתוכנה עשתה לבד, אבל מי יודע. הספר A=B הוא אכן מצויין, ואני נוזף בעצמי שלא הזכרתי אותו קודם - האמת שלא ניחשתי שהוא יעניין את ראובן. |
|
|
|
|
|
|
||
|
||||
|
אני מסכים שכנראה מתמטיקה היא קצת יותר פָרמילה ממוזיקה או ספרות (עד כמה? הנה כבר התפתח פתיל בעניין). רק רציתי לעדן את הניסוח: "הואיל והוכחות מתמטיות הן ... מניפולציה של סמלים ... מכאן ש...מחשבים יוכלו להוכיח כל תוצאה מתמטית". | |
|
|
|
|
|
||
|
||||
|
הבאתי את ראשי הפרקים של הנימוק מציילברגר, ולא התכוונתי לטעון שהמבוא ("הואיל ו...") גורר את המסקנה (טוב, גם בחוזים זה לא כך). אבל זה כמו השדונים של סטניסלב לם: מכיוון שכל הוכחה היא סדרה סופית של סמלים, כל מה שצריך הוא שדון שייצר המון מועמדים-להוכחה, שדון שיסנן את ההוכחות הנכונות (ושדון שיקרא את המשפטים ויחליט איזה מהם מעניינים). |
|
|
|
|
|
|
||
|
||||
|
מה מסמלים קטעים מוזיקליים או ספרותיים? | |
|
|
|
|
|
||
|
||||
|
מה מסמלים משפטים במתמטיקה? אני חושש שלא הבנת את כוונתי ב"מניפולציה של סמלים" (וכוונתם של עוזי ושל ציילינגר). מתמטיקאי עושה "מניפולציה של סמלים" במובן זה שהוא "רק" רושם סימנים על דף בסדר מסוים. אותו דבר עושים המלחין והסופר. הסמלים האלו אחר כך גורמים לתגובות מרתקות במוחם של המאזינים והקוראים; אבל יש מקום לפחות לדון באפשרות שגם מחשב "טיפש" ידע יום אחד לרשום סמלים בסדר כזה שיגרום לנו להתרגש. וכשם שיש מקום גם לפקפק באפשרות כזו, כך יש מקום גם לתהות האמנם מחשב ידע לעשות כל מה שיש לעשות עם הסמלים המתמטיים (בפרט, כפי שנאמר כאן, לדעת מה מעניין). לא, אין לי דעה מעניינת במיוחד בשאלות האלו. |
|
|
|
|
|
|
||
|
||||
|
אני (חושב שאני) מבין את כוונתך. בכל זאת, נראה לי שיש קשר בין האפשרות שהסמלים האלה הם ייצוגים של משהו מחוץ למערכת עצמה, לבין האפשרות שמחשב יוכל לעשות את כל מה שאדם יכול לעשות עם הסמלים האלה. בפרט, נראה לי שאולי כאן יש הבדל בין מוזיקה וספרות לבין מתמטיקה - במיוחד אם נחשוב שהמתמטיקה היא מערכת חוקים שרירותית (אני יודע שאף אחד כאן לא טען את זה). (גם לי אין משהו מיוחד נוסף לומר בעניין, ואפשר לסיים את זה כאן). |
|
|
|
|
|
|
||
|
||||
|
(בכל זאת, עוד תגובונת) אפשר גם לטעון שמוזיקה וספרות הן מערכות חוקים שרירותיות. מי שטוען זאת לגבי מתמטיקה יצטרך להסביר (ואני לא בטוח שאי-אפשר) איך זה שמתמטיקאים נוטים להסכים מה מעניין ומה יפה בתחומם. |
|
|
|
|
|
|
||
|
||||
|
איך ספרות יכולה להיות מערכת חוקים שרירותית? | |
|
|
|
|
|
||
|
||||
|
רציתי להתחיל מלהסביר לגבי מוזיקה, ואז לטעון שבספרות זה יותר קשה, כי שם הרגשות שמתעוררים בנו קשורים הרבה יותר מאשר במוזיקה לתפיסת העולם והידע שלנו. אבל גיליתי שאפילו במוזיקה אני לא מצליח לטעון זאת. לא חשוב איך תופסים את הנפש האנושית, ומה המנגנונים שגורמים לה לתגובות רגשיות למוזיקה; ברור שרצפי סמלים מוזיקליים מסוימים גורמים לתגובות מסוימות, ואחרים לא, בגלל התאמה כלשהי לנפש שלנו (דרך התאמה לנויריופיזיולוגיה, למי שמעדיף). ואז מוזיקה היא שרירותית לכל היותר במידה שהניורופיזיולוגיה שרירותית; וזה כבר מרוקן מתוכן את המילה "שרירותי". ועוד לא נכנסנו בכלל לקשר בין יופי מוזיקלי למתמטיקה (הא!), כפי שלמדנו בדיון 1777. בקיצור, אני חוזר בי מהחלק הזה. | |
|
|
|
|
|
||
|
||||
|
אני חושב שאתה משתמש במובן חזק מדי של המילה "שרירותי". במובן זה, שום מושא נתפס אינו יכול להיות שרירותי (כי הוא מתאים לחושים שלנו או למכשירים שלנו). אני חשבתי על שרירותי במובן של מערכת סמלים כייצוגים של דברים אחרים, חיצוניים למערכת עצמה. ספרות (הן המשפטים עצמם והן מבנה היצירה) נראית לי כמעט-לחלוטין מייצגת מציאות חיצונית, ומכאן הכוח שלה. לגבי מוזיקה, אני לא יודע. אפשר גם לחשוב על מבחן של המרה של הסמלים: אני חושב שאפשר להחליף את הסמלים המתמטיים באופן שרירותי באחרים בלי לאבד דבר מהמשמעות שלהם. אני לא חושב שאפשר להחליף צלילים מסויימים באחרים במקטע מוזיקלי באותה צורה, או מילים במילים נרדפות בספרות טובה. |
|
|
|
|
|
|
||
|
||||
|
מה שמקביל להחלפת הסמלים המתמטייים באחרים הוא, נראה לי, החלפת הצורה הגרפית של האותיות בצורות אחרות (אבל בהחלפה של אחד לאחד, כך שהמילים עצמם תשארנה), והחלפת שיטת הרישום לתווים מוזיקליים. אלה, נראה לי, בהחלט משמרים את המוזיקה ואת הספרות (לאחר שנתרגל לקרוא אותם). זו היתה תגובה נקודתית לפסקה האחרונה שלך; שאר מה שכתוב בתגובתך נראה לי הגיוני, אבל האמת היא שכבר איבדתי את חוט הפתיל. סליחה. |
|
|
|
|
|
|
||
|
||||
|
הפיסקה האחרונה שלך העלתה לי זיכרון נעים מהעבר. פעם הכרתי ברנש שעבד על תוכנה שמוכיחה משפטים בגאומטריה אוקלדית (לכל הפחות תת-קבוצה מכובדת שלהם). מה שמחתי שהזדמן לי לבקש ולקבל הדגמה אישית. כבוגר יסודי גאה, זכור לי היטב המאמץ האינטלקטואלי הדרוש בכתיבת שורה אחר שורה של טענות סדורות המובילות אל המשל המיוחל. כך שמובן שהסתקרנתי מאוד לראות אם תוכנה יכולה לעשות את אותו הדבר. בקיצור... בדחילו ורחימו ניגשנו אל התואם, והברנש בחר את אחד מהמשפטים המוכנים מראש והקליק על solve. דקה ארוכה ישבנו והמתנו לתוצאה. הציפיה היתה כה רבה, והשקט כה מתוח, עד כי ניתן היה לשמוע את זמזום המאוורר הפנימי. לבסוף, ברטינה, המחשב פתח message box ובו כתובה ההודעה הגורלית: YES. חצי שעה אחרי זה לא יכלתי להפסיק לצחוק. מי אמר שלאנשי מחשבים אין חוש הומור. ובמסגרת האופטימיות הכללית, כתבתי תוכנה שבודקת את השערת גולדבלך, עכשיו אני רק מחכה שהמחשבים יהיו מהירים מספיק. |
|
|
|
|
|
|
||
|
||||
|
ועכשיו שני סיפורים שהזכרת לי. הראשון, בדיוק על תוכנה שמוכיחה משפטים בגיאומטריה אוקלידית: אחרי שהמתכנן (לא זוכר מי זה היה) הוסיף לתוכנה את היכולת החשובה של בניות-עזר, הוא רצה לבדוק אם זה עובד, ואיתגר את התוכנה להוכיח שבמשולש שווה-שוקיים, זוויות הבסיס שוות. הוא הניח שהמחשב "יוריד אנך" וימשיך עם חפיפת משולשים. למרבה הפתעתו התוכנה הסתדרה בלי שום בניית עזר, ופשוט הוכיחה שהמשולש כולו, ABC, חופף את משולש ACB. אני חושב שזה הובא כדוגמה נאה ליכולת של תוכנה משוכללת-מספיק להפתיע גם את מי שכתב אותה (ולכן הטענה המקובלת "מחשב לא יכול לעשות שום דבר שלא לימדו אותו" אינה מדוייקת). הסיפור השני הוא על הרצאה של סטיבן הוקינג שהגיע פעם לדבר באוני' העברית. כידוע, הוא נואם בעזרת סינתסייזר-קול, וההרצאה עצמה מוכנה מראש והוא רק שולט בקצב ע"י שהוא מקליק בשביל להתחיל את המשפט הבא. עוזר שלו עמד ליד הלוח ודאג לרישומים. בכל אופן, בסוף הגיע גם זמן לשאלות. מישהו שאל שאלה, ואז השתררה דממה ארוכה בעוד הוקינג משתמש בממשק המצומצם-מאוד שלו כדי לבנות את התשובה. כעבור כמה דקות כבר החלו רחשושים בקהל, ופתאום רעם הקול המתכתי: "Yes". כולם נשתתקו - מה, על זה הוא עבד כל-כך הרבה זמן? - ואז התשובה נמשכה; ה-Yes רק נועד לדאוג לכך שראשית המענה לא יאבד ברחש. |
|
|
|
|
|
|
||
|
||||
|
מזכיר את מחשב העל של הפנטגון, אשר היה אמור לספק פתרונות אופטימליים למצבים איסטרטגיים. בטקס ההשקה של המחשב, הציגו לו סידרת ארועים, ובקשו הנחיה האם לפעול בדרך א' או בדרך ב'. המחשב עבד במשך מספר שניות, כאשר כל הקהל מצפה בדריכות למוצא פיו(?). לבסוף יצא הפלט: "כן". מבוכה קלה השתררה בקרב מפתחי המחשב, ואז החליטו להוסיף שאלת הבהרה. "כן מה?" נשאל המחשב. שוב התחיל המחשב לעבוד במרץ, נקפו מספר שניות, ואז פלט המחשב את התשובה המתוקנת: "כן, המפקד!" |
|
|
|
|
|
|
||
|
||||
|
המתכנת היה E. Gelernter, וההוכחה התגלתה במקור ע"י Pappus (בשנת 300 לספירה לערך). | |
|
|
|
|
|
||
|
||||
|
תודה רבה על החצי הראשון. החצי השני היה ירידה מעודנת...? אגב, איפה זה סופר, ב-GEB מיודענו? | |
|
|
|
|
|
||
|
||||
|
לא ירידה, חלילה: סתם משהו שאכזב המון אנשים, כי פירוש הדבר שהתוכנה לא מצאה הוכחה "מקורית" (מבחינה זו שאף אחד לא גילה אותה לפניה). ע' 606. |
|
|
|
|
|
|
||
|
||||
|
תודה תודה. בשנים שחלפו כבר נתגלו הוכחות מקוריות, ואפילו בעיות פתוחות נפתרו. הזכרתי את השערת Robbins, ועכשיו כדאי שגם אוסיף סייג: ההשערה הזו מתאימה במיוחד להוכחה ממוחשבת. (אגב, מי שסבור שגיאומטריה אוקלידית זה קל מוזמן להוכיח שמשולש שבו חוצי-הזווית שווים באורכם הוא שווה-שוקיים.) |
|
|
|
|
|
|
||
|
||||
|
אי אפשר לתת למחשב לבדוק את ההוכחה? תוכנת הבדיקה יכולה להיות אחרת לגמרי מהתוכנה המוכיחה, וגם הרבה יותר פשוטה, וקל יותר להשתכנע שהיא עובדת נכון (בודקים אותה עם הוכחות שאנו יודעים חיצונית שהן נכונות). מידת הבטחון שלנו בנכונות בדיקה כזו לא צריכה להיות קטנה ממידת הבטחון שלנו בנכונות בדיקה אנושית; ואפשר לכתוב עוד ועוד תוכניות בדיקה שונות, מאפס לצורך העניין, כדי להבטיח עוד יותר אמינות. (והשלב הבא: תוכנה שולחת הוכחה מעניינת לכתב עת; תוכנת השיפוט מזהה שהשולחת היא תוכנה ולא אדם, ובאקט של יד-רוחצת-יד מקבלת את ההוכחה לפרסום למרות שהיא לא באמת שווה.) |
|
|
|
|
|
|
||
|
||||
|
השלב הקודם: אח, על זה כבר סיפר לנו קישון. מכונה שחורשת את השדה, זורעת, קוצרת, אוספת, מובילה לטחנת קמח, לשה, אופה ובסוף אוכלת. | |
|
|
|
|
|
||
|
||||
|
ה"QED Manifesto" היא יוזמה שמטרתה לארגן את כלל הידע המתמטי במסגרת מערכת ממוחשבת פורמלית. אין כוונה כאן למערכת אוטומטית שמגלה או מוכיחה משפטים, אלא רק למערכת שתכיל את הידע הזה בצורה בת-וידוא: במקביל, היילס עצמו מנהל פרוייקט בשם Flyspeck שמטרתו לפרמל באופן כזה את ההוכחה שלו להשערת קפלר, והוא מזמין בעלי הבנה במתמטיקה ומחשבים לעזור: |
|
|
|
|
|
|
||
|
||||
|
הגליון הנוכחי (דצמבר 2008) של ה-Notices of the AMS מוקדש להוכחות פורמליות. המאמרים מאוד מעניינים בעיני, אז חשבתי שתתעניינו גם (all three of you). בין הכותבים תומס היילס בעצמו (ההוא מהכותרת של התגובה הזו). התחום נמצא הרחק מעבר למה שדמיינתי: יש כבר הוכחות פורמליות של משפטים כמו חוק ההדדיות הריבועית, משפט המספרים הראשוניים, משפט העקום של ג'ורדן, משפט גדל, הוכחות נאותות של המערכות עצמן, ובדיקת הוכחות של מערכת אחת בידי מערכת אחרת. תראו איזה יופי: All the basic theorems of mathematics up המערכת Mizar דנה בהוכחות שאפשר כמעט לכנותן קריאות בקלות ע"י בני-אנוש1. המערכת HOL Light אינה ממש כזו, אבל היא קטנה ואלגנטית להדהים2. המערכות כבר מנסחות השערות משלהן, אבל ברור לי שאין להן מושג כלשהו של "יופי". זה ייקח עוד זמן.through the Fundamental Theorem of Calculus are proved from scratch on the user’s laptop in about two minutes every time the system loads. 1 בני-אנוש עם נטיות מפוקפקות במקצת. ראו את ההוכחה של "משפט 11" במאמר של Wiedijk, עמ' 1413. 2 יש מי שיתפלאו לשמוע שהיא מסוגלת להוכיח את המשפטים הנ"ל, כולל המשפט מטופולוגיה, בלי להניח אפילו פעם אחת שהקו מורכב מנקודות. מצד שני, יש מי שלא יתפלאו. |
|
|
|
|
|
|
||
|
||||
|
"On average, a programmer introduces 1.5 bugs per line while typing" וואו. במערכת בת 100,000 שורות קוד שיוצאת לשוק יש לצפות לאלף באגים, ואנשים עוד מעיזים לקטר על MSwindows.
"About one bug per hundred lines of computer code ships to market without detection" |
|
|
|
|
|
|
||
|
||||
|
בהנחה שהיית רציני, רוב הקוד בווינדוס הוא הרבה הרבה אחרי שלב הship to market, ומושקעות בו הרבה יותר שעות מתכנת מאשר בקוד ממוצע. אז אפשר לצפות שהוא יהיה קצת יותר מדובג. | |
|
|
|
|
|
||
|
||||
|
זה יכול להיות מעניין למדי לבקש ממערכת למצוא הוכחה פורמלית למשפט טניאמה-שימורה-ויילס. מן הסתם המערכת לא מסוגלת למצוא לבדה הוכחה פורמלית, אבל היא יכולה להתחיל מההוכחה המלאה של ויילס, ומשם למצוא קשרים יותר עמוקים/ישירים ולקצר את ההוכחה. אם היא תצליח לקצר את ההוכחה, זה יביא לבניית מערכות אלגבריות חדשות. [*] דיסקליימר: אין לי מושג ירוק על עקומות אליפטיות והצגות מודולריות. יש לי מעט יותר מושג על הוכחות פורמליות. |
|
|
|
|
|
|
||
|
||||
|
עקומים אליפטיים ותבניות מודולריות (אני עדיין תחת טראומת ה''צורות מודולריות'' של תרגום הספר של סינג). | |
|
|
|
|
|
||
|
||||
|
זה בהחלט יכול להיות מעניין, אם כי גם קשה (כדי לפרמל את ההוכחה המלאה של ויילס יש קודם לכן לפרמל שלל משפטים והוכחות אחרות.) אני לא חושב שקיצור ההוכחה יביא בהכרח לבניית מערכות אלגבריות חדשות. אולי כן, אולי לא. ייתכן גם שהוכחה פורמלית מקוצרת תישאר סתומה למדי עבור מי שינסה להבין איך ולמה היא עובדת, אבל זה בלי ספק יהיה תרגיל מעניין. [*] מקובל בעברית "עקומים אליפטיים". |
|
|
|
|
|
|
||
|
||||
|
[**] כפי שאמרתי, אין לי מושג ירוק :-) | |
|
|
| חזרה לעמוד הראשי | המאמר המלא |
| מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
 RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |