בתשובה לטל כהן, 24/04/04 10:34
 |
|
 |
||
|
||||
 |
הגליון הנוכחי (דצמבר 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 מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |