בתוך 11 ימים: קלוד יצר פורמליזציה מלאה של ההוכחה למשפט האחרון של פרמה
מודל הבינה המלאכותית קלוד יצר לראשונה הוכחה פורמלית מלאה למשפט האחרון של פרמה, שניתן לאמת אותה במלואה באמצעות מחשב - כך הודיעה חברת אנת'רופיק. המערכת כתבה כ-13 מיליון שורות קוד בשפת Lean והוכיחה עשרות אלפי טענות ביניים
חברת אנת'רופיק הודיעה כי מודל הבינה המלאכותית שלה, קלוד, יצר לראשונה הוכחה פורמלית מלאה למשפט האחרון של פרמה, שניתן לאמת אותה במלואה באמצעות מחשב. העבודה נמשכה 11 ימים: המערכת כתבה כ-13 מיליון שורות קוד בשפת Lean והוכיחה עשרות אלפי טענות ביניים.
אין מדובר בהוכחה חדשה למשפט עצמו. את המשפט ניסח פייר פרמה במאה ה-17, וההוכחה הסופית של אנדרו ויילס פורסמה ב-1995. הישגו של קלוד הוא בכך שהוכחה מתמטית ידועה הומרה לרצף מפורמל בקפידה של צעדים לוגיים, הניתן לבדיקה ממוחשבת.
את הפרויקט הוביל החוקר מאנת'רופיק טיאני פנג. לצורך העבודה נעשה שימוש בעשרות סוכני קלוד, שחילקו ביניהם חלקים נפרדים של המשימה ואיחדו את התוצאות. לפי נתוני החברה, המערכת ייצרה כשישה מיליארד טוקני פלט.
את ההוכחה שהתקבלה בדק המתמטיקאי קווין באזארד מאימפריאל קולג' לונדון (Imperial College London), העוסק בעצמו בפורמליזציה של המשפט האחרון של פרמה. להערכתו, התוצאה אכן מוכיחה את המשפט במסגרת האקסיומות המתמטיות הסטנדרטיות.
באנת'רופיק רואים בניסוי זה עדות לכך שהבינה המלאכותית כבר מסוגלת לבצע פרויקטים רחבי היקף של פורמליזציה למתמטיקה הקיימת.