חוקר נעזר ב-AI כדי להרחיב מחקר של OpenAI והוכיח: ממד 13 הוא האופטימלי במשפחת צורות מסוימת
דניאיל קיסלב פרסם הוכחה ממוחשבת, שנכתבה בסיוע משמעותי של AI, שלפיה סימפלקסים בממד 13 נותנים את קצב הגידול הטוב ביותר במשפחת צורות שנחקרה במאמר של OpenAI מספטמבר. ההוכחה נבדקה במערכת Lean, ובמקביל דווח ברשת על שימוש ב-AI גם בבעיה של ארדש.
חוקר בשם דניאיל קיסלב (Daniil Kiselev) פרסם פרויקט קוד פתוח ב-GitHub שמרחיב מחקר מתמטי שפרסמה OpenAI לפני שבועיים. לפי הפרויקט, סימפלקסים בממד 13, ורק הם, נותנים את קצב הגידול המעריכי הגבוה ביותר בתוך משפחה מסוימת של צורות גאומטריות. הקצב הזה עומד על כ-2.8099647. קיסלב מציין במפורש שנעזר ב-AI באופן משמעותי, ומפרט את השימוש בקובץ ייעודי במאגר.
מה בדיוק הוכח
סימפלקס הוא הכללה של משולש ושל טטרהדרון לממדים גבוהים יותר. ב-24 בספטמבר 2026 פרסמה OpenAI מאמר בשם "A product counterexample to the simplex maximum for projection-body volume". המאמר עוסק בגוף ההיטלים (projection body), אובייקט מתחום הגאומטריה הקמורה, ומראה דוגמה נגדית שנבנית ממכפלות של סימפלקסים בממד 10. הבנייה הזו מניבה קצב גידול מעריכי.
קיסלב שאל שאלה המשך: אם בונים מכפלות כאלה, איזה ממד של "אבן בניין" נותן את הקצב הטוב ביותר? התשובה שהוכיחה העבודה היא 13. על פי הפרויקט, הקבוע שמתקבל מסימפלקס בממד 13 הוא החסם ההדוק לכל ממד חיובי, והשוויון מתקבל רק כשכל הגורמים במכפלה הם בממד 13.
בפרויקט מקפידים לסמן את גבולות הטענה. העבודה לא קובעת מהי המכפלה הטובה ביותר בכל ממד כולל נתון, ולא מהי הצורה האופטימלית מבין כל הגופים הקמורים. היא מוגדרת "תוספת" אלמנטרית למאמר המקורי. הנוסחה הבסיסית, הגאומטריה של המכפלות והבנייה בממד 10 מיוחסות כולן ל-OpenAI. קיסלב גם כותב שלא מצא את האופטימיזציה הזו במקורות שבדק, אבל אינו טוען שבדק את כל הספרות הקודמת. עוד נכתב שלא הוצג שום יישום מעשי ישיר לתוצאה.
הוכחה שהמחשב בודק
ההוכחות נכתבו ב-Lean, שפה ומערכת לאימות פורמלי של הוכחות מתמטיות, יחד עם ספריית mathlib. לפי המאגר נבדקו 44 מודולים, ומתוכם 35 מודולים של OpenAI שהועתקו בלי שינוי. דוחות האקסיומות כוללים רק את שלוש האקסיומות הסטנדרטיות של המערכת, ואין בהם "חורים" כמו sorryAx. גם כאן מסייג המחבר: אימות פורמלי מוכיח שהטענה נכונה, אבל לא שהיא חדשה.
לא מקרה בודד
במקביל הופיע ברדיט דיווח נוסף, שלא אומת באופן עצמאי, על שימוש ב-AI במחקר מתמטי. לפי הפוסט, מחבר אנונימי השיג קבוע מדויק בבעיה מספר 1034 מתוך בעיות ארדש, ובכך שיפר תוצאה של קוואניו טאנג (Quanyu Tang) וג'יה מא (Jie Ma). לדבריו, עיקר העבודה נעשה בשיטת flag algebra בעזרת הכלי FlagAlgebraToolbox, ו-Codex שימש בעיקר לייעול החיפוש החישובי ולהצעת רעיונות. בשלב זה לא ניתן היה לבדוק את הטענה מול מקור עצמאי.
למה זה חשוב
שני המקרים מראים, ככל הנראה, דפוס עבודה שמתחיל להתגבש. ה-AI לא "פותר מתמטיקה" לבד. הוא משמש עוזר שמאפשר לחוקר יחיד להמשיך תוצאה קיימת, לחדד אותה ולגבות אותה בהוכחה ממוחשבת. מה שבולט בפרויקט של קיסלב הוא בעיקר השקיפות: גילוי מלא של השימוש ב-AI, ייחוס מפורט של כל רכיב שאינו מקורי, והפרדה ברורה בין מה שהוכח לבין מה שלא. בתקופה שבה טענות על "פריצות דרך" של AI במתמטיקה מתרבות, ייתכן שהסטנדרט הזה יתברר כחשוב לא פחות מהתוצאה עצמה.