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

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

מהו המשפט האחרון של פרמה - ומדוע הוא התנגד להוכחה במשך 350 שנה

המשפט האחרון של פרמה קובע ששום מספרים שלמים חיוביים a, b ו-c אינם יכולים לספק את המשוואה aⁿ + bⁿ = cⁿ עבור כל ערך של n גדול מ-2. פייר דה פרמה רשם את הטענה בסביבות 1637 בשולי העותק שלו של אריתמטיקה של דיופנטוס, והוסיף חומר שאין לו הוכחה אמיתית שגילה עכשיו- השוליים היו צרים מכדי להכיל.

במשך יותר משלוש מאות שנים השערה עמדה על כל ניסיון להוכיח אותה. לפי החשבון של אנתרופיק, פרס של 100,000 מארקי זהב גרמניים שהוכרזו ב-1908 גרר 621 ניסיונות שגויים בשנה הראשונה בלבד. סר אנדרו ויילס הציג סוף סוף הוכחה נכונה ב-1993 - רק עבור סוקרים לחשוף פער קריטי חודשיים לאימות. ויילס בילה שנה בתיקון ההוכחה עם תלמידו לשעבר ריצ'רד טיילור לפני שפרסם את הגרסה הסופית בת 129 עמודים במאי 1995, שנדרש חודשים של עבודה מאומצת לאימות.

איך קלוד בנה הוכחה של 13 מיליון קווים

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

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

פועל על רתמה מרובת סוכנים מבוססת קלוד קוד, צוות הסוכנים צרך בערך שישה מיליארד אסימוני פלט ממודל מחקר פנימי שאנתרופיק מתאר כדומה לקלוד פייבל 5.1. קלט אנושי הוגבל להוראות מזדמנות ברמה גבוהה - אנתרופיק מצטט הודעות כמו "יעקוביאן כתכנית נשמעת בעדיפות גבוהה" ובקשה לדחוף את משפט מזור לביצוע בקרוב. ההוכחה הושלמה בשעה 02:00 UTC ב-18 באוגוסט, כאשר משפט השורש של הפלטפורמה התהפך ל-Proed.

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

מדוע הוכחה רזה פותרת את השאלה

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

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

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

המשמעות של מחקר מתמטיקה ו-AI

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

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

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

---

הישאר לפני AI

קבל את החדשות, הניתוחים ופריצות הדרך האחרונות של AI - הכל במקום אחד.

קרא עוד חדשות AI →