Anthropic: קלוד יצר הוכחה שלמה ומאומתת במחשב למשפט האחרון של פרמה בתוך 11 ימים
Anthropic פרסמה את ההוכחה השלמה הראשונה של המשפט האחרון של פרמה, מאומתת במחשב: קלוד כתב אותה בשפת Lean בעיקר באופן עצמאי בתוך 11 ימים, 13 מיליון שורות קוד.
מה קרה
Anthropic פרסמה את ההוכחה השלמה הראשונה, מאומתת במחשב, של המשפט האחרון של פרמה. לפי החברה, קלוד עבד בעיקר באופן עצמאי במשך 11 ימים כדי לכתוב את ההוכחה בשפת Lean, שפה המיועדת לאימות פורמלי, והפיק 13 מיליון שורות קוד ו-29,500 משפטי ביניים.
את העבודה הוביל חוקר Anthropic, טיאן פנג, שקבוצתו באוניברסיטת קולומביה בונה כלים לפורמליזציה בעזרת בינה מלאכותית. ההוכחה פורסמה בגלוי ב-GitHub.
למה זה חשוב
הטענה של פרמה — שאין מספרים שלמים חיוביים a, b ו-c המקיימים aⁿ + bⁿ = cⁿ עבור n > 2 — נרשמה בסביבות 1637, ואנדרו ויילס הוכיח אותה רק ב-1995, בהוכחה בת 129 עמודים שאימותה ארך חודשים. בניגוד לעבודה האחרונה של בינה מלאכותית על השערת רימן, שיצרה מתמטיקה חדשה, החידוש כאן הוא האימות: הוכחה פורמלית נבדקת על ידי מכונה.
מה אומרים המומחים
קווין באזארד מהמכללה האימפריאלית בלונדון, שמוביל מאמץ קהילתי רב-שנים לפורמליזציה של המשפט, כינה זאת "הישג אוטופורמליזציה יוצא דופן": המשפט מוכח בלי הנחות נוספות מלבד אקסיומות המתמטיקה. לדברי Anthropic, התוצאה מצביעה על עתיד שבו קל יותר לבדוק ידע מתמטי — וקל יותר לבטוח בו.