בתשובה להאייל האלמוני, 22/10/07 22:14
 |
|
 |
||
|
||||
 |
זו לא שאלה טפשית, ואני חושב שבוודאי. למעשה, ברור שקיים אלגוריתם טיפש שיוכל לייצר הוכחה כזו, וכל הוכחה תקפה סופית, רק שייקח לו הרבה זמן. למעשה, ברור שקיים אלגוריתם עוד יותר טיפש שכל מה שהוא עושה זה לייצר מיידית את ההוכחה של ויילס. אבל אתה שואל בוודאי על אלגוריתם שיכול להפיק הוכחות בסגנון של מתמטיקאים, למשפטים שלא ידועים עדיין, ותוך המצאת טכניקות חדשות. אז זה לא מובן מאליו, אבל אני בכל זאת חושב שבוודאי. זה נראה לי קרוב יותר לשחמט מאשר לניהול שיחה על ענייני שירה ורגש. והייתי שמח לראות נימוק למה שיקולי ה"אסתטיקה" אינם ניתנים לייצוג אלגוריתמי. גם נכונות מתמטית וגם פשטות של הוכחה נראים לי כמעט טריוויאליים לייצוג אלגוריתמי - מה יש כאן יותר מזה? אם כבר, האתגר הגדול יותר לאלגוריתם הוא לשפוט איזו הוכחה *יפה* יותר מרעותה. |  |
 |
 |
|
|
|
||
|
||||
|
האין גא"ב מזכיר תוכנה להוכחת משפטים בגאומטריה, אשר הצליחה לגלות [*] הוכחה שלא הייתה ידועה למחבריה? [*] אך במחקר לאחר מעשה, הסתבר שההוכחה הנ"ל התגלתה כבר בסין או משהו כזה. |
|
|
|
|
|
|
||
|
||||
|
הכוונה כנראה להוכחה אלגנטית1 למשפט שזויות הבסיס במשולש שוה שוקיים שוות. אני לא יודע לגבי סין, אבל היא באמת היתה מוכרת למתמטיקאים אבל לא לכותבי התוכנה. ____________ 1- בלי בניית עזר. |
|
|
|
|
|
|
||
|
||||
|
העניין הוא שאי אפשר להגדיר בדיוק את השיקולים האסתטיים הללו. מה הופך את משפט פרמה למעניין, בניגוד לאינסוף משפטים (כביכול פשוטים) נכונים אחרים? מה הופך אותו לחשוב? כלומר, אולי השאלה שלי היתה צריכה להיות האם אלגוריתם כלשהו היה בכלל "מגלה" אותו כייחודי מלכתחילה? התשובות לשאלות אלו, לפחות כך נראה לי, יהיו חייבות להיות מנוסחות במושגים של הבנה ומשמעות. |
|
|
|
|
|
|
||
|
||||
|
אם נצליח להגדיר אלגוריתם שמזהה "הוכחה אסתטית" לעומת "הוכחה מכוערת שרק מחשב יכול היה לחשוב עליה" (כשאני אומר מזהה, אני מתכוון ל"מסכים עם מתמטיקאים אנושיים"), בעינך האלגוריתם "מבין" מתמטיקה? | |
|
|
|
|
|
||
|
||||
|
לי נראה שמה שהפך את משפט פרמה (וגם בעת היותו השערה) למעניין דווקא די ברור: 1. זו טענה שניתנת לניסוח קצר, 2. היא תקפה לכל המספרים עד הרבה, 3. לא ידועה הוכחה קצרה. אני חושב שכל מה שמקיים את שלושת התנאים האלה ייחשב למעניין כמו משפט פרמה (וכידוע, יש לפחות עוד אחד). ושלושתם כמעט טריוויאליים למחשב בעל יכולת טכנית לבניית הוכחות מתמטיות. |
|
|
|
|
|
|
||
|
||||
|
3. עד לפני שנים לא רבות לא הייתה ידועה *שום* הוכחה, קצרה או ארוכה. לעומת זאת, היה ידוע שפרמה, לפחות, חשב שהוא הוכיח את המשפט, כך שבאיזה אופן, הייתה הרגשה שיש כאן הוכחה במעמד של "סוד". ובאיזה אופן, לא אתפלא אם גם היום עוד יהיו פה ושם מתמטיקאים שינסו למצוא הוכחות אחרות, לגלות את אותו סוד - שהרי ברור שאם פרמה אכן הוכיח את משפטו, ההוכחה שלו הייתה אחרת לגמרי. | |
|
|
|
|
|
||
|
||||
|
האם את אותה אלמונית שניהלה איתי את הפתיל עד כה? חשבתי שהתכוונת שמשפט פרמה מעניין מבחינה מתמטית - עכשיו את אומרת שהוא מעניין בגלל האנקדוטה ההיסטורית. האמנם, או שאני מבין לא נכון? | |
|
|
|
|
|
||
|
||||
|
לא, פשוט אינני אותה אלמונית. :) | |
|
|
|
|
|
||
|
||||
|
הנקודה שלי היתה שיש אינסוף משוואות המקיימות את שלושת התנאים שלך. אז למה דווקא פרמה? או גולדבך? או כל משוואה מתמטית אחרת? מה מייחד אותן? אני טוען שהבסיס הוא המשמעות, הפירושים ה"לא מתמטיים", של משוואות אלו. הבעיה היא שאין לי (ברגע זה, ואולי לעולם לא) הגדרות טובות למושגים אלו. |
|
|
|
|
|
|
||
|
||||
|
אינסוף טענות1? מה פתאום. יש מספר סופי מאוד, ובכלל לא כל כך גדול, של טענות שאפשר לכתוב אותן בכל כך מעט סימנים בשפה טבעית טיפוסית לאריתמטיקה, ו(בהתאם לכך) בשפה פורמלית טיפוסית לאריתמטיקה - וזה התנאי הראשון. כמה מתוכן מקיימות את שני התנאים האחרים? אין לי אפילו אינטואיציה. המתמטיקאים כאן מוזמנים לשפר. למעשה, זה נראה לי נושא נחמד למחקר מתמטי - ואולי, יום אחד, למחקר ממוחשב! (כיום אני מנחש שהתוכנות להוכחות אריתמטיות עדיין חלשות מדי, וגם הוכחות קצרות למדי בשפה טיפוסית למתמטיקאי תידרושנה יותר מדי זמן לתוכנות למוצאן - אבל אני מקווה שנסכים שיכולת כזו היא בגדר יכולתם העקרונית של מחשבים כפי שאנו מכירים אותם כיום). אני עדיין חושב שאם יש עוד טענות כאלה, אז במבט מתמטיקאי טהור (אנושי, אבל מנוטרל משיקולי היסטוריה) הן תהיינה מעניינות לא פחות מפרמה וגולדבאך. אם מחקר שיטתי ימצא אלפי טענות כאלה, אז הן כנראה תפסקנה להיות מעניינות כשלעצמן - אבל אז גם פרמה וגולדבאך עלולות להפסיק להיחשב מעניינות. 1זה מה שהתכוונת, לא "משוואות". משפט פרמה הוא טיפה יותר מהמשוואה המפורסמת שבמרכזו - הוא כולל את העטיפה "לא קיימים מספרים A, B,C כך ש...", ואת השערת גולדבך לרוב מציגים בלי שום משוואה. |
|
|
|
|
|
|
||
|
||||
|
אתה באמת חושב שעניין הקיצור חשוב כל כך? נראה לי שזה דורש הסבר. | |
|
|
|
|
|
||
|
||||
|
זה אותו עיקרון מעין-אסתטי שעומד בבסיס התער של אוקהם. אני לא יכול להצדיק אותו על-סמך משהו בסיסי יותר (אני יכול לומר ''פשטות'', אבל זה לא מסביר יותר מ''קיצור'', רק יותר מעורפל). אני מאמין בכל ליבי שטענה בעלת אותו מבנה לוגי של השערת פרמה או גולדבאך, אבל שהמשוואה שבליבה כוללת עשרה סימנים שונים (למעשה, עשרה גדלים שונים) לא היתה מעוררת את אותו עניין. | |
|
|
|
|
|
||
|
||||
|
|
|
|
|
|
|
||
|
||||
|
השאלות המעניינות אותי אינן האם אלגוריתם יכול לייצר הוכחה למשפט מתמטי ספציפי. ברור שהוא יכול, באופן טריוויאלי, כפי שכתבת בעצמך. מה שפחות מובן הוא: 1) האם קיים אלגוריתם שיכול לייצר את כ_ל ההוכחות שמתמטיקאים מסוגלים להפיק אי פעם (בהנתן זמן בלתי מוגבל)? 2) האם אלגוריתם המפיק הוכחה מתמטית מבין שהוא הפיק הוכחה מתמטית? לדעתי התשובות לשתי השאלות האלו הן שליליות. אלגוריתם יכול אולי לשפוט נכונות של כל הוכחה מתמטית המיוצגת באמצעות שפה פורמלית מסויימת, אולם אין שום שפה פורמלית המייצגת את כל החשיבה המתמטית האפשרית. זה נובע, כך נדמה לי, ממשפט אי השלמות של גדל. בכלל, העובדה שלא ניתן לבצע פורמליזציה של השפה, אפילו לא של השפה המצומצמת המשמשת לחשיבה מתמטית, מוכיחה את הטיעון שלי. אלגוריתמים מוגבלים לשפות פורמליות בלבד. |
|
|
|
|
|
|
||
|
||||
|
לדעתי התשובה לשאלה הראשונה היא טריוואילת כן. שאלה מעט יותר מעניינת וקשה היא האם האלגוריתם ידע למיין את ההוכחות לנכונות ולא נכונות. התשובה לשאלה השנייה היא בעיתית כי לא נתת דרך עבור המתבונן לדעת מתי משהו אחר מבין. | |
|
|
|
|
|
||
|
||||
|
כמובן שהתכוונתי לאלגוריתם שיציג רק הוכחות נכונות. הוכחה שגויה כלל איננה הוכחה. האם קיים "מתמטיקאי אבסולוטי" אלגוריתמי, כזה שמסוגל לגלות את כל ההוכחות (התקפות!) שמתמטיקאים אנושיים עשויים לגלות, ולא להציג טיעונים שמכילים כשלים לוגיים או טעויות? קשה לתת הגדרה ביהוויוריסטית להבנה, משום שהבנה איננה התנהגות, אם כי היא עשויה להתבטא גם באופן התנהגותי. יש מורים, למשל, שמפתחים מיומנות בכתיבת שאלות למבחן הבוחנות עד כמה התלמידים הבינו את החומר ולא סתם שיננו אותו. לדעתי תמיד ניתן למצוא מבחן כזה, אבל אני לא בטוח עד כמה זה פשוט למצוא אותו. |
|
|
|
|
|
|
||
|
||||
|
האם לא נראה לך סביר שברגע שהוכחה קיימת, מכונה תוכל לבדוק את תקפותה? יש שיגידו שזאת *ההגדרה* של הוכחה. אם מכונה כזאת קיימת, כל מה שנותר לנו לעשות זה להזין אותה בגיבריש ולדלות מהגיבריש את ההוכחות התקפות. | |
|
|
|
|
|
||
|
||||
|
מכונה יכולה, תיאורטית, לבדוק תקפותן של הוכחות הכתובות בשפה פורמלית איתה היא יודעת לעבוד. אבל אין שום שפה פורמלית המאפשרת לקודד כל טיעון מתמטי אפשרי. הוכחות מתמטיות כתובות בעברית (או שפה טבעית אחרת), שהיא שפה יותר חזקה מכל שפה פורמלית אפשרית (למשל, היא מכילה את המטא-שפה של עצמה). | |
|
|
|
|
|
||
|
||||
|
אני חשבתי שעד שלא מעבירים הוכחה משפה טבעית לשפה פורמלית אי אפשר בעצם להוכיח כלום. | |
|
|
|
|
|
||
|
||||
|
למעשה יש מעט מאוד הוכחות מתמטיות שמנוסחות בשפה פורמלית. הסימנים המשונים של המתמטיקאים הם קצרנות, לא פורמליזציה. שפה פורמלית זה משהו מאוד ספציפי שמבוסס על הגדרת מחרוזות תווים מסויימות כאקסיומות ושורת פעולות מותרות עליהן ליצירת משפטים. הופשטטר תיאר את העניין מצויין בגא"ב. בכל אופן, גם אם צריך ואפשר להעביר כל הוכחה מתמטית תקפה לשפה פורמלית, מה שאי אפשר לעשות זה להעביר את כל ההוכחות האפשריות ל_א_ו_ת_ה שפה פורמלית. |
|
|
|
|
|
|
||
|
||||
|
אם אי אפשר, אז מחשב, שיכולת העיבוד המתמטית מוגדרת על ידי שפה פורמלית ספציפית (התלויה באלגוריתם שלו) לא יוכל להבין את ההוכחות המתמטיות שאינן ניתנות לקידוד באותה שפה. אבל לבני אדם אין מגבלה כזו. | |
|
|
|
|
|
||
|
||||
|
איך אנחנו יודעים אילו מגבלות יש לבני אדם? | |
|
|
| חזרה לעמוד הראשי | המאמר המלא |
| מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
 RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |