ב-11 ימים: קלוד יצר הוכחה לבעיה מתמטית בת 358 שנים

חברת אנת'רופיק טוענת שמודל ה-AI שלה, קלוד, יצר בתוך 11 ימים הוכחה פורמלית מלאה למשפט האחרון של פרמה - הוכחה שאפשר לבדוק במחשב שורה אחר שורה. לפי החברה, מדובר בהוכחה המתמטית הארוכה ביותר שנבנתה עד היום: 13 מיליון שורות קוד.

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

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

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

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

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

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

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

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

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

במקרה של קלוד, לפי הדיווח, ההוכחה המלאה בת 13 מיליון השורות כבר נמצאת ב-GitHub וזמינה לכל מתמטיקאי שירצה לבדוק אותה שורה אחר שורה.