ב-4 בספטמבר פרסמה אנתרופיק את מה שהיא מתארת כהוכחה הממוחשבת המלאה הראשונה של המשפט האחרון של פרמה (frama). סוכנים של קלוד כתבו אותה בשפת Lean במשך 11 יום, רוב הזמן בלי התערבות אנושית: 13 מיליון שורות קוד ו-29,500 משפטי ביניים. אבל את הפרט הכי שימושי בהודעה קל לפספס. הניסיונות הראשונים נכשלו, והסיבה לא הייתה חוסר ביכולת מתמטית. הסוכנים איבדו את הצפון.
הם פשוט הפסיקו לדעת מה כבר נעשה.
מה הוכח, ומה לא
המשפט עצמו כבר הוכח. פייר דה פרמה רשם אותו בשוליים של ספר בסביבות 1637: אין שלושה מספרים שלמים חיוביים a, b ו-c שמקיימים aⁿ + bⁿ = cⁿ כש-n גדול מ-2. ההוכחה הראשונה שהחזיקה מעמד, של אנדרו וויילס, התפרסמה ב-1995, השתרעה על 129 עמודים, ובדיקה שלה דרשה חודשים של עבודה.
אנתרופיק לא טוענת שקלוד גילה מתמטיקה חדשה. בהודעה היא כותבת במפורש שהחידוש כאן הוא האימות, בדיקה של הוכחה כמו שבודקים חישוב במחשבון. Lean היא שפה שבה מחשב בודק כל צעד לוגי, כולל הצעדים שמתמטיקאי מדלג עליהם כי הם "ברורים". הוכחה שעוברת את הבדיקה הזאת לא תלויה בכך שמישהו קרא אותה בעיון.
מאז 2024 מוביל קווין באזארד מאימפריאל קולג' בלונדון מאמץ קהילתי לעשות בדיוק את זה, והוא תוכנן לשנים. רק תוכנית העבודה של שלב הפתיחה בפרויקט הזה מגיעה ל-86 עמודים. באזארד קיבל את ההוכחה של קלוד לבדיקה, וכינה אותה הישג יוצא דופן שמוכיח את המשפט בלי שום הנחה מלבד האקסיומות של המתמטיקה.
לפי אנתרופיק, ההוכחה משתמשת רק בשלוש האקסיומות הסטנדרטיות של Lean, וכלי השוואה אישר שהניסוח של המשפט בסוף זהה לניסוח שמופיע ב-Mathlib, הספרייה הקהילתית שעליה כל העבודה נשענת. יש לבדיקה הזאת סיבה טובה: הוכחה מושלמת למשפט שנוסח קצת אחרת היא דרך מוכרת לרמות את עצמך.
הניסיון שנכשל
ההודעה של אנתרופיק מקדישה לזה שלוש שורות, והן השורות המעניינות ביותר בה. עשרות סוכנים של קלוד עבדו במקביל: הגדירו מושגים, הוכיחו משפטי עזר, והשתמשו בהם כדי להוכיח טענות קשות יותר. בהתחלה זה עבד. אחר כך, בלשון החברה, הסוכנים איבדו מהר את המעקב אחרי מצב הפרויקט והפסיקו לשתף פעולה ביעילות.
מהעבודה של הניסיונות האלה לא נשאר הרבה. לפי אנתרופיק, הם תרמו כ-7 אחוזים מהשורות המהותיות בהוכחה הסופית.
כל מי שהפעיל יותר מסוכן אחד על משימה ארוכה מכיר את התסמינים. סוכן אחד מוכיח משהו שסוכן אחר כבר הוכיח. סוכן שלישי מחכה לתוצאה שאף אחד לא עובד עליה. ההקשר של כל אחד מהם מתמלא, והזיכרון של מה שסוכם לפני שלושה ימים נשחק. כשמדובר בעשרות סוכנים, סביר להניח שזה יקרה.
מה שהציל את הפרויקט: גרף משימות
ההצלחה הגיעה אחרי מעבר ל-Prove2Me, פלטפורמה פתוחה לפורמליזציה שיתופית שפיתחו טיאני פנג, חוקר באנתרופיק שהקבוצה שלו יושבת באוניברסיטת קולומביה, ושותפיו. לפי אנתרופיק, הכלי עשה שלושה דברים:
- ניהל גרף של כל המשפטים והתלויות ביניהם. הסוכנים בחרו לפיו מה להוכיח עכשיו, וזה, כותבת החברה, עזר במיוחד מול שחיקת הזיכרון ואיפשר לכמה סוכנים לעבוד במקביל.
- הפריד בין ניסוח משפט להוכחה שלו, בקבצים נפרדים, כך שהקומפילציה של Lean נעשתה מהירה וזולה יותר.
- החזיק תיאור בשפה טבעית לכל משפט, כדי שסוכן יוכל למצוא משפט קיים ולהשתמש בו במקום להוכיח אותו מחדש.
אף אחד מהשלושה אינו יכולת של המודל. אלה החלטות של ניהול פרויקט: רשימת משימות משותפת עם תלויות, חלוקה לקבצים, ומפתח שאפשר לחפש בו.
המודל, לפי ההודעה, היה מודל מחקר פנימי כללי שדומה ביכולותיו ל-Claude Fable 5.1. הרתמה הייתה מערכת סוכנים שבנויה על קלוד קוד. ההוכחה המלאה פתוחה בגיטהאב, יחד עם הסבר כתוב, והמאמר על Prove2Me פורסם ב-arXiv.
כמה בן אדם היה בלולאה
לפי אנתרופיק, התרומה המתמטית של בני אדם הסתכמה בהוראות כלליות מדי פעם של פנג. שתיים מהן מצוטטות בהודעה, ושתיהן נשמעות כמו מנהל פרויקט ולא כמו מתמטיקאי: שהיעקוביאן כסכֶמה נשמע בעדיפות גבוהה, ושצריך לדחוף את משפט מזור להסתיים בקרוב.
זה מתאים לתמונה. אדם החליט על סדר העדיפויות, וגרף המשימות דאג שהסוכנים יעבדו לפיו.
החברה פרסמה גם קטעים מהחשיבה של קלוד ברגע הסיום. באחד מהם הסוכן מדווח שהשורש של הגרף, המשפט עצמו, מסומן כמוכח, ב-18 באוגוסט בשעה 02:00 לפי שעון גריניץ'. ובאחר הוא מכנה את זה רגע היסטורי, ומוסיף הסתייגות בסוגריים: בכפוף לבדיקה חוזרת.
גם הסוכן, מסתבר, לא סומך על עצמו עד שהבודק אומר את דברו. זו בדיוק ההתנהגות שרוצים.
שישה מיליארד טוקנים, או שלושה מנויים
החשבון לא זול. לפי אנתרופיק, הפרויקט צרך כשישה מיליארד טוקנים של פלט. הוכחה של 13 מיליון שורות גדולה פי חמישה ויותר מכל Mathlib, והחברה מודה בהערת שוליים שחלק מהפער נובע מכך שההוכחה שלה כנראה ארוכה בהרבה ממה שהיא צריכה להיות.
אבל באותה הודעה יש ניסוי קטן שמספר סיפור אחר. חוקרים באנתרופיק הפעילו סוכנים על שלושה מנויי Claude Max אישיים, כולם עובדים דרך Prove2Me, והשלימו פורמליזציה של משפט שלושת הראשוניים של וינוגרדוב בשלושה ימים. המסקנה שהחברה עצמה מנסחת: עם הפיגום הנכון, פורמליזציה שיתופית של תוצאות גדולות אפשרית גם במנויים לצרכנים.
ההשוואה לא מושלמת, כי הפורמליזציה של וינוגרדוב כנראה קטנה בהרבה. ובכל זאת, בשני המקרים החברה מייחסת את ההצלחה לפיגום, ולא לגודל של המודל.
למה זה מגיע דווקא עכשיו
ארבעה ימים אחרי ההודעה הזאת פרסמה OpenAI הוכחה לבעיית נאוויה-סטוקס, שנוצרה בנחיל של אלפי סוכנים ולוותה גם היא באימות ב-Lean. מתמטיקאים מתחילים לקבל יותר הוכחות מכונה ממה שהם מסוגלים לקרוא.
ההיסטוריה של המשפט של פרמה מראה כמה זה יקר גם בלי מכונות. ב-1908 הוכרז פרס של 100 אלף מארק זהב למי שיוכיח אותו, ובשנה הראשונה לבדה הוגשו 621 הוכחות שגויות. ההוכחה שוויילס הציג ב-1993 הכילה פער שהתגלה רק אחרי חודשיים של בדיקה, והוא עבד שנה כדי לתקן אותו.
באזארד אמר לאנתרופיק שאם פורמליזציה אוטומטית של פרמה אפשרית היום, זה צעד גדול לקראת פורמליזציה אוטומטית של הספרות המתמטית המודרנית, ושהטכניקות האלה יאפשרו לבדוק מתמטיקה שנוצרה במודלי שפה, תהליך שכיום הוא יקר מאוד ונעשה בידי בני אדם. אנתרופיק עצמה כותבת שהוכחה פורמלית לא אמורה להחליף הסבר שבני אדם יכולים לקרוא, אבל שהיא אולי הדרך המעשית היחידה לעמוד בקצב של מה שמודלים מייצרים.
כלומר, הפתרון לעודף הוכחות של מכונות הוא מכונה שבודקת אותן. זה נשמע מעגלי, וזה לא. Lean לא סומך על אף אחד, ובזה כל הערך שלו.
הלקח נמצא מחוץ למתמטיקה
רוב האנשים שמפעילים סוכנים לא כותבים הוכחות. הם מריצים סוכני קוד, תהליכי מחקר, או שרשרת של סוכנים שמעבירים עבודה אחד לשני. הכשל שאנתרופיק תיארה, סוכנים שמאבדים את מצב הפרויקט, לא שייך לפרמה. הוא שייך לכל משימה שארוכה מחלון ההקשר של סוכן אחד.
והפתרון שעבד שם היה צנוע: מקום אחד, מחוץ לראש של הסוכנים, שבו כתוב מה הוכח, מה תלוי במה, ומה הצעד הבא. בפרויקט של אנתרופיק זה היה גרף. בפרויקט קטן יותר זה יכול להיות קובץ משימות משותף, ובלבד שהסוכנים באמת קוראים ממנו וכותבים אליו.
המבחנים שבודקים מודלים מודדים בדרך כלל כמה סוכן אחד חכם. בפרויקט הזה, לפי התיאור של אנתרופיק, העשרות נכשלו ואחר כך הצליחו, והשינוי שהיא מדגישה בין שני השלבים הוא רשימת המשימות.
מבוסס על ידיעה שפורסמה באתר של אנתרופיק, 4 בספטמבר 2026. הליד הגיע מכתבה של Mehmet Özel ב-Data Science Collective.
