בתשובה להאייל האלמוני, 22/10/07 22:14
לרבע את הלולאה. 460791
זו לא שאלה טפשית, ואני חושב שבוודאי. למעשה, ברור שקיים אלגוריתם טיפש שיוכל לייצר הוכחה כזו, וכל הוכחה תקפה סופית, רק שייקח לו הרבה זמן. למעשה, ברור שקיים אלגוריתם עוד יותר טיפש שכל מה שהוא עושה זה לייצר מיידית את ההוכחה של ויילס. אבל אתה שואל בוודאי על אלגוריתם שיכול להפיק הוכחות בסגנון של מתמטיקאים, למשפטים שלא ידועים עדיין, ותוך המצאת טכניקות חדשות. אז זה לא מובן מאליו, אבל אני בכל זאת חושב שבוודאי. זה נראה לי קרוב יותר לשחמט מאשר לניהול שיחה על ענייני שירה ורגש. והייתי שמח לראות נימוק למה שיקולי ה"אסתטיקה" אינם ניתנים לייצוג אלגוריתמי. גם נכונות מתמטית וגם פשטות של הוכחה נראים לי כמעט טריוויאליים לייצוג אלגוריתמי - מה יש כאן יותר מזה? אם כבר, האתגר הגדול יותר לאלגוריתם הוא לשפוט איזו הוכחה *יפה* יותר מרעותה.
לרבע את הלולאה. 460799
האין גא"ב מזכיר תוכנה להוכחת משפטים בגאומטריה, אשר הצליחה לגלות [*] הוכחה שלא הייתה ידועה למחבריה?

[*] אך במחקר לאחר מעשה, הסתבר שההוכחה הנ"ל התגלתה כבר בסין או משהו כזה.
לרבע את הלולאה. 460813
הכוונה כנראה להוכחה אלגנטית‏1 למשפט שזויות הבסיס במשולש שוה שוקיים שוות. אני לא יודע לגבי סין, אבל היא באמת היתה מוכרת למתמטיקאים אבל לא לכותבי התוכנה.
____________
1- בלי בניית עזר.
לרבע את הלולאה. 460805
העניין הוא שאי אפשר להגדיר בדיוק את השיקולים האסתטיים הללו. מה הופך את משפט פרמה למעניין, בניגוד לאינסוף משפטים (כביכול פשוטים) נכונים אחרים? מה הופך אותו לחשוב? כלומר, אולי השאלה שלי היתה צריכה להיות האם אלגוריתם כלשהו היה בכלל "מגלה" אותו כייחודי מלכתחילה?
התשובות לשאלות אלו, לפחות כך נראה לי, יהיו חייבות להיות מנוסחות במושגים של הבנה ומשמעות.
לרבע את הלולאה. 460811
אם נצליח להגדיר אלגוריתם שמזהה "הוכחה אסתטית" לעומת "הוכחה מכוערת שרק מחשב יכול היה לחשוב עליה" (כשאני אומר מזהה, אני מתכוון ל"מסכים עם מתמטיקאים אנושיים"), בעינך האלגוריתם "מבין" מתמטיקה?
לרבע את הלולאה. 460902
לי נראה שמה שהפך את משפט פרמה (וגם בעת היותו השערה) למעניין דווקא די ברור:
1. זו טענה שניתנת לניסוח קצר,
2. היא תקפה לכל המספרים עד הרבה,
3. לא ידועה הוכחה קצרה.

אני חושב שכל מה שמקיים את שלושת התנאים האלה ייחשב למעניין כמו משפט פרמה (וכידוע, יש לפחות עוד אחד). ושלושתם כמעט טריוויאליים למחשב בעל יכולת טכנית לבניית הוכחות מתמטיות.
לרבע את הלולאה. 460931
3. עד לפני שנים לא רבות לא הייתה ידועה *שום* הוכחה, קצרה או ארוכה. לעומת זאת, היה ידוע שפרמה, לפחות, חשב שהוא הוכיח את המשפט, כך שבאיזה אופן, הייתה הרגשה שיש כאן הוכחה במעמד של "סוד". ובאיזה אופן, לא אתפלא אם גם היום עוד יהיו פה ושם מתמטיקאים שינסו למצוא הוכחות אחרות, לגלות את אותו סוד - שהרי ברור שאם פרמה אכן הוכיח את משפטו, ההוכחה שלו הייתה אחרת לגמרי.
לרבע את הלולאה. 460991
האם את אותה אלמונית שניהלה איתי את הפתיל עד כה? חשבתי שהתכוונת שמשפט פרמה מעניין מבחינה מתמטית - עכשיו את אומרת שהוא מעניין בגלל האנקדוטה ההיסטורית. האמנם, או שאני מבין לא נכון?
לרבע את הלולאה. 461010
לא, פשוט אינני אותה אלמונית. :)
לרבע את הלולאה. 461114
הנקודה שלי היתה שיש אינסוף משוואות המקיימות את שלושת התנאים שלך. אז למה דווקא פרמה? או גולדבך? או כל משוואה מתמטית אחרת?
מה מייחד אותן? אני טוען שהבסיס הוא המשמעות, הפירושים ה"לא מתמטיים", של משוואות אלו. הבעיה היא שאין לי (ברגע זה, ואולי לעולם לא) הגדרות טובות למושגים אלו.
לרבע את הלולאה. 461130
אינסוף טענות‏1? מה פתאום. יש מספר סופי מאוד, ובכלל לא כל כך גדול, של טענות שאפשר לכתוב אותן בכל כך מעט סימנים בשפה טבעית טיפוסית לאריתמטיקה, ו(בהתאם לכך) בשפה פורמלית טיפוסית לאריתמטיקה - וזה התנאי הראשון. כמה מתוכן מקיימות את שני התנאים האחרים? אין לי אפילו אינטואיציה. המתמטיקאים כאן מוזמנים לשפר. למעשה, זה נראה לי נושא נחמד למחקר מתמטי - ואולי, יום אחד, למחקר ממוחשב! (כיום אני מנחש שהתוכנות להוכחות אריתמטיות עדיין חלשות מדי, וגם הוכחות קצרות למדי בשפה טיפוסית למתמטיקאי תידרושנה יותר מדי זמן לתוכנות למוצאן - אבל אני מקווה שנסכים שיכולת כזו היא בגדר יכולתם העקרונית של מחשבים כפי שאנו מכירים אותם כיום). אני עדיין חושב שאם יש עוד טענות כאלה, אז במבט מתמטיקאי טהור (אנושי, אבל מנוטרל משיקולי היסטוריה) הן תהיינה מעניינות לא פחות מפרמה וגולדבאך. אם מחקר שיטתי ימצא אלפי טענות כאלה, אז הן כנראה תפסקנה להיות מעניינות כשלעצמן - אבל אז גם פרמה וגולדבאך עלולות להפסיק להיחשב מעניינות.

1זה מה שהתכוונת, לא "משוואות". משפט פרמה הוא טיפה יותר מהמשוואה המפורסמת שבמרכזו - הוא כולל את העטיפה "לא קיימים מספרים A, B,C כך ש...", ואת השערת גולדבך לרוב מציגים בלי שום משוואה.
לרבע את הלולאה. 461170
אתה באמת חושב שעניין הקיצור חשוב כל כך? נראה לי שזה דורש הסבר.
לרבע את הלולאה. 461206
זה אותו עיקרון מעין-אסתטי שעומד בבסיס התער של אוקהם. אני לא יכול להצדיק אותו על-סמך משהו בסיסי יותר (אני יכול לומר ''פשטות'', אבל זה לא מסביר יותר מ''קיצור'', רק יותר מעורפל). אני מאמין בכל ליבי שטענה בעלת אותו מבנה לוגי של השערת פרמה או גולדבאך, אבל שהמשוואה שבליבה כוללת עשרה סימנים שונים (למעשה, עשרה גדלים שונים) לא היתה מעוררת את אותו עניין.
לרבע את הלולאה. 461269
לרבע את הלולאה. 460884
השאלות המעניינות אותי אינן האם אלגוריתם יכול לייצר הוכחה למשפט מתמטי ספציפי. ברור שהוא יכול, באופן טריוויאלי, כפי שכתבת בעצמך. מה שפחות מובן הוא:
1) האם קיים אלגוריתם שיכול לייצר את כ_ל ההוכחות שמתמטיקאים מסוגלים להפיק אי פעם (בהנתן זמן בלתי מוגבל)?
2) האם אלגוריתם המפיק הוכחה מתמטית מבין שהוא הפיק הוכחה מתמטית?

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

קשה לתת הגדרה ביהוויוריסטית להבנה, משום שהבנה איננה התנהגות, אם כי היא עשויה להתבטא גם באופן התנהגותי. יש מורים, למשל, שמפתחים מיומנות בכתיבת שאלות למבחן הבוחנות עד כמה התלמידים הבינו את החומר ולא סתם שיננו אותו. לדעתי תמיד ניתן למצוא מבחן כזה, אבל אני לא בטוח עד כמה זה פשוט למצוא אותו.
לרבע את הלולאה. 460943
האם לא נראה לך סביר שברגע שהוכחה קיימת, מכונה תוכל לבדוק את תקפותה? יש שיגידו שזאת *ההגדרה* של הוכחה. אם מכונה כזאת קיימת, כל מה שנותר לנו לעשות זה להזין אותה בגיבריש ולדלות מהגיבריש את ההוכחות התקפות.
לרבע את הלולאה. 460969
מכונה יכולה, תיאורטית, לבדוק תקפותן של הוכחות הכתובות בשפה פורמלית איתה היא יודעת לעבוד. אבל אין שום שפה פורמלית המאפשרת לקודד כל טיעון מתמטי אפשרי. הוכחות מתמטיות כתובות בעברית (או שפה טבעית אחרת), שהיא שפה יותר חזקה מכל שפה פורמלית אפשרית (למשל, היא מכילה את המטא-שפה של עצמה).
לרבע את הלולאה. 460971
אני חשבתי שעד שלא מעבירים הוכחה משפה טבעית לשפה פורמלית אי אפשר בעצם להוכיח כלום.
לרבע את הלולאה. 461069
למעשה יש מעט מאוד הוכחות מתמטיות שמנוסחות בשפה פורמלית. הסימנים המשונים של המתמטיקאים הם קצרנות, לא פורמליזציה. שפה פורמלית זה משהו מאוד ספציפי שמבוסס על הגדרת מחרוזות תווים מסויימות כאקסיומות ושורת פעולות מותרות עליהן ליצירת משפטים. הופשטטר תיאר את העניין מצויין בגא"ב.

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

חזרה לעמוד הראשי המאמר המלא

מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים