המודלים הפנימיים של OpenAI ושל אנתרופית כמעט בו-זמנית הפריכו את השערת הזמן האקספוננציאלי (ETH). מאז סוף שנות ה-90, סברו כי בדיקת האם נוסחה לוגית עם n משתנים יכולה להיות נכונה במקרה הגרוע ביותר לא יכולה להתבצע מהר יותר מזמן אקספוננציאלי ל-n. OpenAI פרסמה פרינט מוקדם עם אלגוריתם מהיר יותר שהמודל שלה מצא. יום לאחר מכן, אנתרופית פרסמה תוצאה דומה של מודל קלוד, וההוכחה הפורמלית ב-Lean 4 נכתבה גם היא על ידי המודל, והתוכנית בודקת אותה. מתברר שהמודלים כבר מוצאים אלגוריתמים חדשים שבהם ההשערה מוחזקת כבר יותר מ-25 שנה, ומביאים את ההוכחה לאימות מכונה, כך שאין צורך להאמין למילה שלהם. כפי ש-אנתרופית כותב, התוצאה לא אומרת דבר על פתרון נוסחאות בפועל. OpenAI כתבה בתחילת אוקטובר שהיא מתכוננת לשחרר את המודל שמאחורי המאגר הזה, ולכן אני מצפה לתכונות כאלה גם ב-API הציבורי.