בתשובה לטל כהן, 24/04/04 10:34
היילס, תפוזים והוכחות ממוחשבות 214196
אי אפשר לתת למחשב לבדוק את ההוכחה? תוכנת הבדיקה יכולה להיות אחרת לגמרי מהתוכנה המוכיחה, וגם הרבה יותר פשוטה, וקל יותר להשתכנע שהיא עובדת נכון (בודקים אותה עם הוכחות שאנו יודעים חיצונית שהן נכונות). מידת הבטחון שלנו בנכונות בדיקה כזו לא צריכה להיות קטנה ממידת הבטחון שלנו בנכונות בדיקה אנושית; ואפשר לכתוב עוד ועוד תוכניות בדיקה שונות, מאפס לצורך העניין, כדי להבטיח עוד יותר אמינות.

(והשלב הבא: תוכנה שולחת הוכחה מעניינת לכתב עת; תוכנת השיפוט מזהה שהשולחת היא תוכנה ולא אדם, ובאקט של יד-רוחצת-יד מקבלת את ההוכחה לפרסום למרות שהיא לא באמת שווה.)
ארבינקא, תפוזים והוכחות ממוחשבות 214201
השלב הקודם: אח, על זה כבר סיפר לנו קישון. מכונה שחורשת את השדה, זורעת, קוצרת, אוספת, מובילה לטחנת קמח, לשה, אופה ובסוף אוכלת.

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

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