קלוד השלים פורמליזציה ממוחשבת למשפט האחרון של פרמה

Anthropic פרסמה בסוף השבוע פורמליזציה מלאה של המשפט האחרון של פרמה בשפת Lean. לפי החברה, עשרות סוכני קלוד עבדו במשך 11 ימים, כתבו כ-13 מיליון שורות קוד והשלימו עשרות אלפי משפטי ביניים. התוצאה אינה הוכחה מתמטית חדשה: היא ממירה מסלול מוכר מהספרות של ויילס וטיילור-ויילס למבנה לוגי שמחשב יכול לבדוק צעד אחר צעד.

מה בדיוק נבדק

במאגר הקוד הפומבי מופיעה הטענה המלאה עבור מספרים טבעיים וחזקות גדולות משתיים. יעד הבנייה הראשי בודק שהמסקנה נשענת על שלוש האקסיומות הסטנדרטיות של Lean, בלי הנחות עזר לא מוכחות. Anthropic הריצה גם כלי השוואה שמוודא כי ניסוח המשפט זהה לניסוח המקובל ב-Mathlib, ספריית המתמטיקה המרכזית של Lean. המאגר עבר בנוסף בדיקה באמצעות ליבה עצמאית שנכתבה ב-Rust.

קווין באזארד מאימפריאל קולג', שמוביל פרויקט אנושי רב-שנתי לפורמליזציה של אותו משפט, הוריד את הקוד, קימפל אותו והריץ את כלי ההשוואה. לדבריו, הבדיקה הושלמה בהצלחה. הוא גם מדגיש את הגבול: הקוד אינו מוסיף כמעט ידע מתמטי חדש, והוא ארוך בהרבה מהצגה שנועדה לקורא אנושי.

איך העבודה חולקה

המערכת השתמשה ב-Prove2Me, פלטפורמה שמנהלת גרף תלות בין משפטים. כל צומת מייצג טענה שצריך להוכיח, והקשרים קובעים אילו משימות מוכנות לעבודה. כך סוכנים שונים יכלו לטפל באלגברה, אנליזה, גאומטריה ותורת המספרים במקביל, בלי להסתמך על זיכרון שיחה ארוך. Anthropic דיווחה על כשישה מיליארד טוקני פלט, ולכן זהו ניסוי עתיר מחשוב, גם אם לוח הזמנים קצר.

המסלול הפורמלי נשען על Mathlib ועל עבודה קודמת של פרויקט FLT באימפריאל ושל flt-regular. הוא מטפל בחזקות הגדולות או שוות ל-17 באמצעות המסלול של דרמון, דיימונד וטיילור, ומשלים את המקרים הקטנים בעזרת תוצאות שכבר עברו פורמליזציה. ייחוס החלקים האלה מתועד במאגר.

למה זה חשוב

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

המאגר כולל נתיב הוכחה, קבצי מקור ואתר מקומי לעיון באלפי המשפטים. העובדה שאפשר להריץ את הבדיקה מחדש חשובה כאן יותר מהכרזה יחידה של מעבדת AI: היא נותנת למתמטיקאים חומר שאפשר לבחון, לבקר ולשפר. צוות חיצוני יכול גם לשחזר את הבנייה, לבדוק את גרסאות הכלים ולזהות במדויק איזו הנחה מזינה כל מסקנה.