OpenAI: המודל Astra פתר עשר בעיות פתוחות במתמטיקה, ולכל הוכחה יש אישור ב-Lean

גרסה פנימית של OpenAI Astra פתרה לטענת החברה עשר בעיות פתוחות במתמטיקה ובמדעי המחשב התיאורטיים. OpenAI Astra עדיין לא זמין לציבור, אבל לכל הוכחה יש אישור שמחשב יכול לבדוק. OpenAI פרסמה את התוצאות ב-1 באוגוסט 2026.

Astra היא משפחת המודלים הבאה של OpenAI. את הפרטים מביא דוח של OpenAI בשם Ten Advances in Mathematics and Theoretical Computer Science. הגרסה העדכנית שלו נושאת תאריך 6 באוגוסט, ויש בה קישור לגרסה המקורית. אישורי ההוכחה עצמם פתוחים לכולם ב-GitHub.

עשר תוצאות: מה פתר OpenAI Astra

התוצאה המרכזית היא בנייה של קבוצה שאינה sofic. מתמטיקאים שואלים אם קבוצות כאלה קיימות מאז 1999, אחרי ש-Mikhail Gromov הציג את המושג. לפי TNW, איש לא הכריע בשאלה במשך 27 השנים שחלפו.

הרשימה כוללת גם הפרכה של השערת הקשיחות של Connes. בנוסף יש הוכחה של השערת הנפח של Ehrhart. יש גם פתרון של שלוש בעיות מהרשימה של Erdős, שמספרן 146, 180 ו-183.

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

איך OpenAI Astra הגיע לתוצאות ומי בדק אותן

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

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

בנוסף, OpenAI מדווחת שהטוקנים של כל עשר ההוכחות היו עולים כ-2,000 דולר לפי תעריפי ה-API של Sol. המספר מתאר רק את הטוקנים של הפתרונות.

המאגר openai/ten-proofs ב-GitHub משתמש ב-Lean 4.32.0. יש בו הוראות בנייה והוראות לבדיקה עצמאית בכלי Comparator. מי שמתקין Lean יכול להריץ את הבדיקה בעצמו.

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

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

מה ידוע על Astra עצמו

Astra הוא מודל פנימי, ו-OpenAI לא נתנה תאריך השקה. לפי The Information, כפי ש-The Decoder סיכם, Astra יהיה מחלקה חדשה של מודלים. הוא יעמוד לצד Sol, Terra ו-Luna. OpenAI עדיין לא החליטה אם ישווק בשם GPT-6 או כגרסה בסדרת GPT-5.

לפי אותו דיווח, Sam Altman הציג את Astra לפוליטיקאים ולרגולטורים בוושינגטון. Astra אמור להיות הראשון שיעבור במסגרת הבדיקה הפדרלית שממשל Trump מתכנן. המסגרת תחייב להגיש מודלים לממשלה לפני השחרור.

Thomas Bloom מאוניברסיטת מנצ'סטר מנהל את אתר erdosproblems.com. הוא כתב ב-X שהתוצאות הן ״חדשות גדולות״. Noam Brown מ-OpenAI כתב שהצוות ניסה גם בעיות גדולות אחרות ולא הצליח. לדבריו, אין עדיין פתרון לאף אחת מבעיות פרס המילניום.

עוד ב-GEEKLIK: דיווח: מאות קבלנים של OpenAI קוראים שיחות אמיתיות ב-ChatGPT כדי לדרג תשובות