כך קלוד, לפי אנתרופיק, הפך את המשפט האחרון של פרמה להוכחת Lean בתוך 11 ימים

לא פתרון חדש של הבעיה — אלא הוכחה קיימת בשפה שמחשב יכול לבדוק

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

המשפט האחרון של פרמה קובע שלמשוואה (a^n+b^n=c^n), כאשר (n\geq3), אין פתרון לא־טריוויאלי במספרים טבעיים. הניסוח ב־Mathlib, ספריית המתמטיקה של Lean, אומר שכל פתרון כזה חייב לקיים (a=0), (b=0) או (c=0) — ניסוח השקול לאמירה המוכרת על היעדר פתרונות במספרים שלמים חיוביים. 31

המסלול המתמטי: גרסה מודרנית של אסטרטגיית ויילס

הפרויקט התבסס על ההצגה של Darmon–Diamond–Taylor לאסטרטגיית Wiles/Taylor–Wiles, ולא על המצאת דרך חדשה במתמטיקה. גם פרויקט הפורמליזציה של אימפריאל קולג' מתאר את מסלולו כגרסה מודרנית של הוכחת ויילס/טיילור–ויילס. 511

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

למה נדרשו 13 מיליון שורות קוד

אנתרופיק מדווחת על כ־30,300 משפטים שנבדקו ממוחשבת במהלך הפרויקט; כ־29,500 מהם מופיעים בשרשרת התלויות של ההוכחה הסופית. הפיתוח משתרע על אלגברה, גאומטריה, אנליזה הרמונית ותורת המספרים. 215

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

המפתח: תיאום חיצוני בין סוכנים רבים

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

הרעיון הארגוני המרכזי הוא גרף תלויות מכוון:

• כל צומת מייצג הגדרה, למת עזר או משפט שעדיין נדרשים.
• קשתות מראות אילו תוצאות נחוצות כדי להשלים תוצאות מאוחרות יותר.
• סוכנים יכולים לבחור משימות פתוחות ובעלות ערך, להוכיח אותן ב־Lean, ולהעמיד את התוצרים לשימוש סוכנים אחרים.
• כך אפשר להתקדם מרכיבי יסוד אל המשפט הסופי.

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

מה בדיוק אומר "נבדק במחשב"?

לפי אנתרופיק, בפרויקט הסופי אין מצייני מקום מסוג sorry — המנגנון של Lean שמאפשר להניח טענה בלי להוכיח אותה — והוא נשען רק על שלוש האקסיומות הסטנדרטיות של Lean. 5

זו טענה חזקה בהרבה מטקסט מתמטי משכנע לכאורה שמודל שפה ניסח. ליבת Lean בודקת שכל צעד מקודד נובע מכללי הלוגיקה של המערכת, מהאקסיומות ומהתלויות שיובאו. אנתרופיק מוסיפה שבדקה שהטענה הסופית תואמת לניסוח הקיים של FermatLastTheorem ב־Mathlib. 531

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

מדוע קווין באזארד הגדיר זאת הישג יוצא דופן

לפי דיווחה של אנתרופיק, המתמטיקאי קווין באזארד תיאר את התוצאה כ"הישג יוצא דופן של פורמליזציה אוטומטית". 21 המשמעות אינה רק היכולת לפתור תרגילי Lean בודדים, אלא הטענה שסוכנים הרכיבו פיתוח פורמלי עמוק, רב־שכבתי וניתן לשימוש חוזר — בהיקף שבעבר נראה ככזה שדורש שנים של עבודת צוות אנושית.

אם תהליך כזה יהפוך לשחזור וזול יותר, הוא עשוי לסייע למחקר המתמטי בכמה דרכים:

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

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

הפרשנות המדויקת להכרזה

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

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

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