 |
"איזה אלגוריתם" - ברוב המקרים, אין אלגוריתם *פרקטי* לאימות/הפרכה, אם כי בתורות פשוטות מאוד אין קושי למצוא כזה. נדמה לי שבגיאומטריה של המישור זה אכן נעשה:
(נסה להתעלם מההומור הגיקי לגבי ספר מהעתיד; שים לב לסעיף Theorems שבו יש הוכחות ממוחשבות למשפטים ידועים בגיאומטריה).
"במידה והיה אלגוריתם לבדיקה האם הדבר לא היה טכני ומידי" - כן, *אם* היה כזה, ו*אם* הוא היא רץ בזמן סביר, ו*אם* אנדרו ויילס היה מתאמץ לכתוב את ההוכחה שלו בשפה פורמלית. מתמטיקאים כמעט אף-פעם לא עושים זאת; המטרה שלהם היא לשכנע את עמיתיהם שההוכחה תקפה.
עם זאת, התחום של הוכחות ממוחשבות (ובדיקה ממוחשבת של הוכחות) הולך ומתפתח. למשל:
ועוד. אם זה מעניין אותך, חפש proof checking בגוגל. יהיה מעניין לראות אם בעוד 50 שנה יתחולל איזה שינוי מהותי בדרך בה מתמטיקאים מוודאים את התגליות שלהם, ומשוחחים עליהן (אני לא בטוח שזה יקרה כל כך מהר, ולא בטוח שזה צריך לקרות).
"או שבתאוריות לא שלמות אי אפשר לאמת את המשפטים ע"י אלגוריתם" - בתאוריות לא שלמות אי-אפשר *להוכיח* את *כל* המשפטים ע"י אלגוריתם, אבל ודאי שאפשר *לאמת* הוכחה מוצעת.
|
 |
RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש