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

ב-4 בספטמבר 2026 פרסמה Anthropic שקלוד (Claude) השלים את ההוכחה הראשונה של משפט פרמה האחרון שמחשב אימת מקצה לקצה. הריצה עצמה קדמה להודעה: לפי הדוח הטכני היא נפתחה ב-7 באוגוסט והסתיימה ב-17 בו — אחד-עשר יום.

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

רגע, קלוד הוכיח את משפט פרמה?

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

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

מה בדיוק קרה שם

• 13 מיליון שורות Lean, שהן לפי Anthropic יותר מפי חמישה מ-Mathlib, ספריית ההוכחות המרכזית של הקהילה
• 30,300 משפטים הוכחו, מהם 29,500 נכנסו להוכחה הסופית
• הסתמכות על שלוש האקסיומות הסטנדרטיות של Lean בלבד, בלי אף מציין מקום לא-מוכח מסוג sorry
• ההוכחה פורסמה במלואה, יחד עם הסבר כתוב, במאגר בגיטהאב

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

אז מה החזיק אותו אחד-עשר יום?

שני דברים, ושניהם תשתית — לא מודל.

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

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

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

המספרים שממתנים את ההתלהבות

בגלוי, כי בלי זה התמונה מעוותת:

• המודל אינו מודל שאפשר לקנות. הדוח מתאר “מודל מחקר פנימי כללי, בקירוב בסדר גודל של פייבל 5.1”. לא פייבל 5.1 עצמו
• כשש מיליארד טוקני פלט. Anthropic מגדירה את הריצה כעתירת טוקנים, וזה הניסוח שלה
• ההוכחה ארוכה מדי, לפי Anthropic עצמה: היא כותבת שהיא “כנראה ארוכה בהרבה ממה שהיא צריכה להיות”, בהשוואה ל-Mathlib שהוא תמציתי ועבר סקירה
• כ-7% מהשורות שאינן שבלוניות הגיעו מניסיונות שנכשלו — כלומר גם ריצה שהסתיימה בהצלחה גרפה איתה שאריות של דרכים שלא הובילו לשום מקום

והחלק שכן אפשר לגעת בו

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

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

מה זה אומר על העבודה שלכם

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

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

מה שכן עובר משם לכאן:

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

שורה תחתונה

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

מי שהתשובה שלו היא “כלום”, יודע עכשיו מה חוסם את הריצות הארוכות שלו. נקודת ההתחלה היא המדריך לאימות בקלוד קוד, ואחריו סוכני משנה.