OpenAI טוענת לפתרון שאלות ענק במדע אבל המודל נשאר בפנים
החברה פרסמה פלטי גלם של הוכחות במתמטיקה, מדעי המחשב ופיזיקה קוונטית, אך במקום כלי עבודה לחוקרים היא מחלקת סמכויות לוועדות אקדמיות סגורות.
- הורידו את קובצי ה־Lean מ־GitHub כדי לבחון את ההוכחות בעצמכם, אך אל תבנו על שילוב מודל ההיסק המחקרי של OpenAI בעבודתכם.
השבוע שוב נפתרו כל בעיות היקום, לפחות לפי מחלקת יחסי הציבור של סן פרנסיסקו. אתמול, 26 באוקטובר 2026, הכריזה OpenAI על שורת הישגים מחקריים חריגים במאמר שכותרתו Working with academic communities to build scientific understanding. הבולטים שבהם הם פתרון השערת קאקייה במתמטיקה והפרכת השערת הזמן האקספוננציאלי במדעי המחשב. הודעה כזו לא רואים כל יום.
אם אתם חוקרים אלגוריתמים או בונים מערכות נתונים, הנטייה הראשונה היא לחפש איזה מודל בדיוק הפיק את ההוכחות הללו ובאילו תנאים. תחסכו לעצמכם את החיפוש בהודעה: לא פורסם באיזה מודל פנימי ספציפי השתמשו, לא צוין כמה כוח חישוב נדרש כדי להגיע לפלטים הללו, ולא נמסר כמה ניסיונות כושלים נוצרו בדרך. לא הייתי ממהר להסיק שמדובר ביכולת זמינה למחקר השוטף שלכם.
גלם בגיטהאב, לא מוצר
מה ששוחרר בפועל מוגדר על ידי OpenAI כנתוני מחקר גולמיים. במקום לשחרר כלי עבודה שיאפשר לקהילה המדעית להריץ היסקים דומים, החברה פרסמה טקסטים גולמיים בשפה טבעית לצד קובצי אימות בשפת Lean, תוכנה המאמתת עקביות של טענות לוגיות. את הפיענוח, הניתוח וההבנה של מה שהמכונה פלטה, היא מגלגלת הלאה. לפי הודעת החברה, התוצרים מוגדרים כנתוני מחקר גולמיים בלבד, והאקדמיה מוזמנת להתנדב כדי לפענח מה המודלים הפנימיים הפיקו בפועל.
זה לא מוצר, וזה שווה בעיקר למי שרוצה לעשות עבודה שחורה בחינם.
במתמטיקה, המערכת ייצרה ב־18 באוקטובר 2026 הוכחה להשערת ההחלקה המקומית שהציע סוגה ב־1991, תוך שימוש במשוואה דיפרנציאלית חלקית חדשה. יום למחרת, לפי החברה, ההוכחה כבר עברה פורמליזציה מלאה בקוד. במדעי המחשב, המודל ייצר ב־16 באוקטובר 2026 שלילה להשערת ETH, שנשענת על שאלת הסיבוכיות של בעיית SAT ומקושרת ישירות לשאלת P מול NP. שני הפלטים הללו, לצד קוד ה־Lean התואם, הועלו למאגר פתוח ב־GitHub.
לפי תפיסתנו, כתבי יד אלה מובנים בצורה הטובה ביותר כסוג של נתוני מחקר גולמיים. כדי להמיר את נתוני המחקר הגולמיים הללו להבנה מדעית, אנו מתנסים בגישה חדשה.הודעת OpenAI הרשמית
שלושה תחומים, שלושה מודלים
כדי להתמודד עם ניתוח הפלטים, OpenAI המציאה תפקיד חדש: רועים אקדמיים (shepherds). מדובר בחוקרים בכירים שנבחרו על ידי החברה כדי להוביל קבוצות עבודה חיצוניות שיבחנו את הטקסטים. אלא שבמקום מדיניות אחידה, החברה יצרה שלושה מסלולי שחרור שונים לחלוטין, שמעוררים תהיות לגבי מידת השקיפות האמיתית של הניסוי.
במתמטיקה, הגישה הייתה שחרור מיידי לרשת, ללא קבוצה ייעודית, בדומה למתווה שפורסם תחת שיתוף התקדמות ה־AI במתמטיקה. במדעי המחשב, התוצאה פורסמה לציבור במקביל להקמת צוות בהובלת ראסל אימפליאצו, רממוהן פטורי וראיין וויליאמס. השניים הראשונים הם מנסחי השערת ETH המקורית, ווויליאמס מגיע מ־MIT. כאן OpenAI גם התחייבה לממן כנס מדעי בנושא.
בפיזיקה תיאורטית, המצב שונה בתכלית. המודל ייצר בספטמבר 2026 הוכחה לקיום תורת יאנג-מילס הטהורה, שהיא אחת מבעיות המילניום של מכון קליי, ולאחר מכן הוכחה לקיום QCD והרחבה של המודל הסטנדרטי. הפורמליזציה ב־Lean הסתיימה ב־16 באוקטובר 2026. אלא שכאן החומרים ננעלו לחלוטין. קבוצה חיצונית בראשות חתן פרס נובל דייוויד גרוס, יחד עם חוקרים כמו ארתור יפה ומייקל דאגלס, החליטה שלא לשחרר את תוצרי ה־AI או את קובצי ה־Lean לציבור, אלא לשבת עליהם בדלתיים סגורות עד לכתיבת מאמר עצמאי.
| תחום מדעי | הבעיה שנפתרה | רמת שקיפות הפלט | מעורבות אקדמית חיצונית | זמינות קובץ Lean |
|---|---|---|---|---|
| מתמטיקה | השערת ההחלקה המקומית וקאקייה | פתוח לחלוטין ב־GitHub | ללא קבוצה ייעודית | זמין להורדה |
| מדעי המחשב | שלילת השערת הזמן האקספוננציאלי (ETH) | פתוח לקהילה במקביל לעבודה | צוות ייעודי בראשות אימפליאצו, פטורי וויליאמס | זמין להורדה |
| פיזיקה תיאורטית | קיום QCD ותורת יאנג-מילס | סגור לחלוטין לציבור | ועדה סגורה בראשות דייוויד גרוס | לא פורסם |
ההוכחה של Lean לא מספיקה
קל להסתנוור מהמילה הוכחה כשמוצמד אליה אימות מחשב. Lean אכן בודקת שכל צעד גוזר את הצעד הבא לפי כללי התחשיב הפורמלי, אך היא אינה בודקת האם ההגדרות עצמן תואמות את הבעיה המקורית שנשאלה בעולם האמיתי. פער קל בניסוח האקסיומות עלול לייצר הוכחה תקפה מתמטית למשפט שאף אחד לא התכוון להוכיח.
הפרכת השערת ETH היא דוגמה טובה לרגישות הזו. מאות מאמרים במדעי המחשב הניחו שהשערה זו נכונה כדי לבסס חסמים תחתונים על סיבוכיות של אלגוריתמים בגרפים וביולוגיה חישובית. אם השלילה תתברר כנכונה, שאלות רבות על זמני ריצה ייפתחו מחדש. מצד שני, אם יתגלה פגם בהבנת התנאים שפורמלו בקוד, הממצא כולו יקרוס. זה קרה בעבר בהוכחות אנושיות מורכבות, ואין שום סיבה להניח שמודל שפה חסין מטעויות כאלה.
הזמנה לבדוק, בלי כפתור הפעלה
לפי החברה, שיתופי הפעולה נשענים על ארבעה עקרונות: שקיפות ללא הסכמי סודיות, ויתור של OpenAI על קרדיט אקדמי, מתן קרדיט מלא למפרשים החיצוניים, ועצמאות אקדמית ללא שכר. בנוסף, החברה העבירה תרומה של 5 מיליון דולר לקרן סיימונס למימון סדנאות ומחקר. כל אלה צעדים יפים, אך הם לא משנים את העובדה המרכזית: הניסוי אינו ניתן לשחזור עצמאי על ידי גורם מחוץ לחברה.
הצעד המעשי היחיד שעומד כעת בפני מדעני נתונים וחוקרים באקדמיה הוא להוריד את קובצי ה־PDF וה־Lean ממאגר ה־GitHub הציבורי של החברה, או לנסות לשלוח דוא"ל לוועדת הפיזיקה הסגורה בכתובת YANGMILLS4D@gmail.com. להריץ מודל שיפתור לכם את הבעיה הפתוחה הבאה באלגוריתמים? זה לא יקרה בזמן הקרוב.
בינתיים, OpenAI השאירה לעצמה את המפתח למנוע, ונתנה לחוקרים לנקות את האגזוז.
מה שואלים על זה
- Working with academic communities to build scientific understandingopenai.com · המקור
- releaseopenai.com · מקושר מההודעה
- Lean proof (opens in a new window)github.com · מקושר מההודעה
30 עובדות בכתבה נבדקו אחת־אחת מול המקורות המקושרים ב־27 באוקטובר 2026. מה שלא אומת הוסר או מסומן כטענה של החברה. הכתיבה נעשתה בעזרת AI מהמקורות האלה בלבד, בעריכה ובאחריות של סלבה מלנדוביץ׳. טעות? כתבו לנו.