Axiom Math, חברה שבסיסה בסן פרנסיסקו הבונה מערכות בינה מלאכותית למתמטיקה, פרסמה את ההוכחה המלאה הראשונה שנבדקה במחשב של הסיווג של קבוצות סופיות ופשוטות (CFSG), שתוארה בהרחבה כהוכחה הארוכה ביותר בהיסטוריה של המתמטיקה. על פי הודעת החברה, מהנדסים ומתמטיקאים כיוונו נחילים של עשרות סוכני בינה מלאכותית במשך 24 ימים בלבד לייצר כ-43.1 מיליון שורות קוד ב-Lean proof assistant, מה שמאמת תוצאה שהשתרעה בעבר על כ-15,000 עמודים על פני יותר מ-500 מאמרים בכתבי עת 1 שנכתבו על ידי מספר עשורים של מתמטיים.
ההישג נוחת ברגע שבו מתמטיקה בעזרת מכונה מואצת במהירות, ושקעים העוקבים אחר חדשות מחקר AI צפו באימות הפורמלי עובר מפרקטיקה נישה ליכולת גבולית. מה שהופך את המהדורה הזו ליוצאת דופן היא קנה המידה: הפורמליזציה מכילה בערך 2.05 מיליון הצהרות מאורגנות ב-100 אבני דרך, כל אחת מהן נבדקת על ידי הליבה של Lean, הליבה הקטנה ומהימנה שמאמתת כל שלב לוגי.
מה שהסיווג אומר בפועל
קבוצות פשוטות סופיות הן אבני הבניין הבלתי ניתנות לחלוקה של סימטריה סופית, והסיווג - המכונה "המשפט העצום" - נותן רשימה מלאה שלהם. על פי התיעוד של הפרויקט, כל קבוצה פשוטה סופית היא אחת מארבעה סוגים: קבוצה מחזורית בסדר ראשוני, קבוצה מתחלפת על לפחות חמישה סמלים, אחת משש עשרה משפחות אינסופיות של קבוצות מסוג שקר הבנויות על פני שדות סופיים, או אחת מתוך 26 קבוצות ספורדיות בדיוק שאינן מתאימות לאף משפחה.
הוכחה שהרשימה הזאת ממצה כל אפשרות לקחה את החלק הטוב ביותר של מאה שנה של מאמץ קולקטיבי. ג'ון תומפסון, שעבודתו הייתה מרכזית בסיווג, קיבל את מדליית פילדס בשנת 1970 ואת פרס הבל בשנת 2008. ההוכחה הייתה כה ארוכה וכל כך הופצה על פני מאמרים ודורות של מתמטיקאים, שהספקות המתמשכים לגבי שלמותה נמשכו במשך עשרות שנים - ספקות שהפורמליזציה הזו מפיגה כעת רשמית.
נחילי סוכנים על פני 500 מקורות
ההוכחה המקורית מפוזרת על פני יותר מ-500 מאמרים וספרים, רבים שנכתבו לפני עשרות שנים בסימנים לא תואמים. מהנדס Axiom תיאר את השיטה בדיון ב-Hacker News על השחרור: נחיל סוכנים הוטל לעבור על כל המקורות הללו, כשהחלק הקשה הוא להרכיב הכל לכדי שלם קוהרנטי, מכיוון שניתן לנסח את אותו מושג בלתי פורמלי בדרכים מעט שונות אך לא תואמות מבחינה מתמטית.
בפוסט של החברה בבלוג נכתב כי המאמץ נמשך 24 ימים מתחילתו ועד לשחרורו, כאשר מהנדסי אנוש ומתמטיקאים מנווטים את נחילי הסוכנים במקום לעבוד שורה אחר שורה. התוצאה באה בעקבות אבני דרך קודמות של פורמליזציה אוטומטית בפרופיל גבוה בשנת 2026, כולל הוכחות Lean של משפטים קלאסיים מרכזיים שהופקו עם מודלים חזיתיים, אך בקנה מידה שאף פרויקט קודם לא ניגש.
34 סטיות מהרשומה שפורסמה
תרגום ההוכחה שפורסמה לצורה הניתנת לבדיקה במכונה חשף בעיות אמיתיות בספרות המתמטית. Axiom מדווחת שרוב הבעיות היו מינוריות - שגיאות דפוס, טעויות בטבלאות או השערות שנפלו. אבל היו 34 סטיות ראויות לציון מהתיעוד שפורסם שהיה צריך לפתור לפני שהפורמליזציה תעבור.
המהותי ביותר נגע למשפט הקבוצה הלא מאוזנת. תוך כדי פורמליזציה של מסלול דור ראשון לתוצאה, הצוות מצא דוגמאות נגד להצהרת סגירה המשמשת בטיעון שפורסם. בהתייעצות עם תיאורטיקנים של קבוצות מומחים, הם בנו מסלול חלופי שנבנה על טכניקות מבניות מתקופת דניאל גורנשטיין - ספציפית תיאוריה של 2 רכיבים מקסימליים משנות ה-70 - ופרסמו את התיקון כמאמר חדש של 35 עמודים לתיאוריה של קבוצות, שפורסם כדפוס 2610.00575. החברה טוענת כי תפרסם רשימה ארוכה של תקלות לרווחת הקהילה המתמטית, שנערכה בהתייעצות עם תיאורטיקני הקבוצות שעל עבודתם נשען הסיווג.
למה חשובה מתמטיקה שנבדקה במכונה
הערך של פורמליזציה הוא לא רק שמחשב אישר את ההוכחה. פורמליזציה של Lean מצמצמת את בסיס האמון לגרעין של עוזר ההוכחה - תוכנית קטנה ומבוקרת בכבדות - במקום הביטחון המצטבר של אלפי דפים הנקראים על ידי מומחים מפוזרים. מגיבים בשרשור האקר ניוז, שבו הסיפור גרר מאות הצבעות בעד, ציינו שידע אמפירי לגבי הסיבה שהסיווג מתקיים היה בסיכון ממש למות כשהדור המקורי של המתמטיקאים פרש, מכיוון שאף אדם אחד לא יכול להחזיק את כל הטיעון בראשו.
יש הדים מעשיים גם במקומות אחרים בפיזיקה. הגדולה מבין 26 הקבוצות הספורדיות, קבוצת המפלצת, מופיעה בתוכנית "מפלצתי ירח" המחברת סימטריה סופית לפונקציות מודולריות - עבודה שזיכתה את ריצ'רד בורצ'רדס במדליית פילדס ב-1998 - ובהצעה של אדוארד וויטן משנת 2007 הקושרת את הסימטריות של המפלצת לאנטרופיה תלת-ממדית של יקום שחור. סיווג מאומת מעמיד את המתמטיקה המבנית הבסיסית על קרקע יציבה יותר בדיוק עבור סוגים אלה של יישומים חוצי-תחומיים.
מה שיבוא אחר כך
אקסיום אומרת שעוד מסמכים שנגזרו מהפורמליזציה בדרך, לצד פרויקט ה-errata. עבור קהילת השיטות הפורמליות, המהדורה מציבה רף חדש למה שפרויקטי אימות מכווני סוכן יכולים לנסות; למתמטיקה, הוא ממיר הישג שיתופי רחב ידיים בן חצי מאה לחפץ אחד שכל מחשב יכול לבדוק. כבר לא מאמינים בסיווג בלבד. זה עכשיו, במובן המילולי ביותר, מוכח - וההוכחה זמינה לכל אחד להוריד ולאמת.
