OpenAI חשפה שגרסה פנימית של Astra, הדגם הבא שלה שטרם שוחרר, פתרה עשר בעיות פתוחות במתמטיקה ובמדעי המחשב התיאורטיים — חלקן ללא פתרון כבר יותר מעשור. החברה פרסמה מסמך בן 249 עמודים ב-GitHub, ולכל הוכחה צורף אימות פורמלי במערכת Lean 4 שבודק כל שלב באופן ממוחשב וחד-משמעי.
ההישג הבולט מביניהם הוא הבנייה המפורשת הראשונה של "חבורה לא-סופית" (non-sofic group) — שאלה מרכזית בתורת החבורות שנותרה פתוחה מאז 1999. בנוסף, הדגם הפריך את השערת הנוקשות של קון (Connes) באלגברות פון-נוימן, הוכיח את השערת הנפח של אֶרהארט, ופתר שלוש בעיות של פול ארדש, כולל שיפור ראשון מאז 1978 בחסמים על צפיפות אריזת כדורים.
לפי OpenAI, כל התהליך החישובי שהוביל לפתרונות עלה כ-2,000 דולר בלבד לפי תעריפי ה-API שלה. סבסטיאן ביבק, ראש מחקר המתמטיקה בחברה, תיאר את ההוכחות כ"יפות", וציין שלכל אחת מהן מצורף אישור Lean והסברים. הפרסום מגיע על רקע "הצהרת ליידן" מיוני 2026, שבה מתמטיקאים הביעו חשש מכך שחברות AI משתמשות במחקר קיים ומדלגות על בדיקת עמיתים.
מקורות: OpenAI The Next Web
