Claude כותב ב־Lean הוכחה מאומתת למשפט פרמה
Anthropic דיווחה ב־4 בספטמבר 2026 ש־Claude הפיק את ההוכחה הראשונה המלאה שנבדקה במחשב למשפט האחרון של פרמה: כ־13 מיליון שורות Lean וכ־29,500 משפטי־ביניים במשך כ־11 ימים של עבודה סוכנית בעיקר אוטונומית על פלטפורמת Prove2Me, עם שלושת אקסיומות Lean הסטנדרטיות וניסוח שאומת מול FLT ב־Mathlib. החוקר Tianyi Peng מ־Anthropic כיוון עדיפויות ברמה גבוהה; קווין באזרד (Kevin Buzzard) סקר את התוצאה וכינה את האוטו־פורמליזציה יוצאת דופן, ואמר שטכניקות כאלה יכולות לעזור לבדוק מתמטיקה שנוצרה ב־AI ולהקל על שיפוט מאמרים. Anthropic ממסגרת זאת כאימות של נתיב וויילס (דרך Darmon–Diamond–Taylor), לא מתמטיקה חדשה כמו תוצאת רימן חדשה, ולא השקת מוצר Claude לצרכן.
This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics.