אחד האתגרים המפרכים ביותר בהיסטוריה של המתמטיקה מצא את פתרונו במקום הבלתי צפוי ביותר. חברת אנתרופיק, היצרנית של מודל הבינה המלאכותית קלוד, חשפה השבוע כי הצ'אטבוט הפופלרי שלה הצליח להשלים בתוך 11 ימים בלבד את ההוכחה הממוחשבת המלאה הראשונה למשפט האחרון של פרמה - חידה מתמטית שהטריפה את מוחותיהם של החוקרים במשך 358 שנים.
בניגוד להוכחות אנושיות, הדורשות שנים של ביקורת עמיתים מפרכת, קלוד ייצר 13 מיליון שורות קוד שניתן לאמת באופן אוטומטי ובאופן מוחלט, ללא צורך באמון בבני אדם.
שבירת מוסכמות: מרוץ שהוכרע מראש
הרגע ההיסטורי הזה מכה גלים בקהילה האקדמית מכיוון שהוא מאפיל על מאמצים אנושיים קיימים. צוות חוקרים בראשות המתמטיקאי הידוע קווין באזארד, מאימפריאל קולג' לונדון, מנהל מאז 2024 פרויקט ייעודי שמטרתו לתרגם את ההוכחה המקורית של אנדרו ווילס משנת 1995 לשפת תכנות מתמטית. פרויקט זה, הנתמך בתקציבים ובצבא מתנדבים, תוכנן להימשך לפחות עד 2029 - אך הסוכנים האוטונומיים של קלוד גמאו את הדרך אל קו הסיום תוך שבועיים בלבד.
קלוד הוכיח את המשפט ללא שום הנחות מלבד, והציג קבצים שזכו לאישורו המלא של באזארד. (אגב, באזארד, המוביל את פרויקט תרגום ההוכחה, בדק את הקבצים של קלוד שפורסמו ב-GitHub ואישר שהם אכן תקפים ומסתמכים אך ורק על האקסיומות הבסיסיות ביותר של המתמטיקה).
מאחורי הקלעים: כך קלוד עשה היסטוריה
ההישג לא הגיע בקלות. ההצלחה של קלוד התאפשרה בזכות פריסת עשרות סוכני בינה מלאכותית שעבדו במקביל על הוכחת אלפי משפטי עזר קטנים וחיבורם לתמונה גדולה. בשלבים הראשונים, עשרות סוכני בינה מלאכותית שעבדו במקביל איבדו את הצפון, הפסיקו לשתף פעולה ויצרו כפילויות שעדיין מהוות כ-7% משורות הקוד הגולמיות. הפתרון הגיע בדמות כלי עזר ייעודי בשם Prove2Me, שפיתח טייאני פנג מאוניברסיטת קולומביה יחד עם צוותו.
Prove2Me פעל כלוח משימות דינמי ומרכזי. הכלי ניהל רשימת מטלות חיה, מנע חפיפה במידע, וסיכם בקצרה בשפה טבעית את ההישגים של כל סוכן. בזכות מנגנון זה, המודלים הצליחו לייצר רצף לוגי המורכב מ-13 מיליון שורות קוד בשפת Lean, תוך צריכת מיליארדי טוקנים ופתרון כשלים בזמן אמת. בסיום התהליך, קלוד הוכיח יותר מ-30 אלף משפטי עזר וצרך מיליארדי טוקנים.
(ראוי לציין כי 13 מיליון שורות הקוד שנכתבו שוות ערך ל-160 רומנים שלמים של טיעון לוגי צרוף - פי חמישה מנפחה של ספריית Mathlib השיתופית שבה משתמשים מתמטיקאים כיום).
כניסתם של כלי AI המסוגלים לייצר הוכחות פורמליות מלאות בשפת Lean מטלטלת את יסודות המחקר האקדמי. כאמור, עד כה, מתמטיקאים הסתמכו על ביקורת עמיתים ידנית ואיטית, תהליך מפרך שלעיתים לקח שנים ולעולם לא חף משגיאות נסתרות או פערים לוגיים. ההישג של קלוד מוכיח כי מעתה ניתן ליצור "קבלות ממוחשבות" דטרמיניסטיות המאמתות כל צעד מתוך אקסיומות בסיסיות ללא תלות באמון אנושי. עבור הקהילה המדעית, מדובר בהצלה מהירה מעומס עצום של מחקרים והוכחות חדשות שהחוקרים כבר מתקשים לבדוק לבד, מה שסולל עידן שבו המכונה הופכת לשותפה אקטיבית וקריטית בפיתוח המדע.
למה ההישג הזה משנה את כללי המשחק?
חשוב להבהיר: קלוד לא גילה מתמטיקה חדשה יש מאין, שכן אנדרו ווילס כבר פתר את המשפט המפורסם בשנת 1995. החידוש הגדול טמון ביכולת לייצר "קבלה ממוחשבת" המאמתת את כל השלבים באופן דטרמיניסטי לחלוטין. בעוד שמתמטיקאים טובעים כיום בכמות עצומה של הוכחות לא מאומתות - כולל כאלה שנכתבות על ידי מודלי AI שונים - פתרונות מסוג זה פותרים את משבר האמון ומבטלים את השגיאות האנושיות המאפיינות בדיקות ידניות מורכבות.
פתרון המשפט האחרון של פרמה על ידי ווילס ב-1995 נחשב לאחד השיאים המפוארים של המתימטיקה המודרנית, אך הוא דרש שבע שנים של עבודה סודית, מסע מפרך של 129 עמודים, ותיקון דרמטי של חור לוגי שהתגלה רק בדיעבד. ההוכחה של ווילס הסתמכה על ענפים במתמטיקה שלא היו קיימים בימיו של פייר דה פרמה, ודרשה אינטואיציה אנושית יוצאת דופן. לעומת זאת, הפרויקט של קלוד לא המציא מתמטיקה חדשה יש מאין, אלא תרגם את המבנה הקיים לשפה ממוחשבת קפדנית.
בעוד שווילס סיפק את הפריצה הרעיונית, קלוד סיפק את האימות המוחלט - חיבור מושלם בין גאוניות אנושית לדיוק מכני חסר פשרות.
ההוכחה המלאה כבר זמינה ב-GitHub לכל מי שמעוניין לרדת לעומקה, שורה אחר שורה.
טעינו? נתקן! אם מצאתם טעות בכתבה, נשמח שתשתפו אותנו