הישגי AI במתמטיקה (AI in Mathematics)

יולי 2024: מדליית כסף ראשונה — AlphaProof ו-AlphaGeometry 2

ב-25 ביולי 2024 הודיעה Google DeepMind ששתי המערכות שפיתחה, AlphaProof ו-AlphaGeometry 2, פתרו ארבע מתוך שש הבעיות של האולימפיאדה הבינלאומית למתמטיקה (IMO) לשנת 2024. הן צברו 28 נקודות מתוך 42 האפשריות, ציון ברמת מדליית כסף, וקיבלו ציון מושלם בכל בעיה שפתרו. AlphaProof, מערכת למידת חיזוק, פתרה שתי בעיות אלגברה ובעיית תורת המספרים אחת, ובהן הבעיה הקשה ביותר בתחרות, שרק חמישה מתמודדים אנושיים פתרו אותה; AlphaGeometry 2 פתרה את בעיית הגיאומטריה. שתי בעיות הקומבינטוריקה נשארו בלתי פתורות. רף מדליית הזהב באותה שנה עמד על 29 נקודות, ו-58 מתוך 609 המתמודדים הרשמיים הגיעו אליו. חשוב להבחין: את הפתרונות ניקדו, לפי כללי ה-IMO, שני מתמטיקאים שגוגל פנתה אליהם, טימותי גאוורס וג'וזף מאיירס, ולא מתאמי התחרות הרשמיים. לפני שהמערכות עבדו על הבעיות, הן תורגמו ידנית לשפה פורמלית. בעיה אחת נפתרה בתוך דקות, אבל פתרון של אחרות ארך עד שלושה ימים, בעוד שמתמודדים אנושיים מקבלים שני מושבים של ארבע וחצי שעות.

יולי 2025: שתי תוצאות ברמת זהב — אחת מאושרת רשמית ואחת בפרסום עצמאי

שנה לאחר מכן הגיעו שתי חברות לרמת זהב, אבל בדרכים שונות מהותית. ב-19 ביולי 2025, יום שבת, פרסמה OpenAI שמודל ניסיוני שלה פתר חמש מתוך שש בעיות ה-IMO לאותה שנה וצבר 35 נקודות — רמת זהב — בלי שימוש בכלים, בגישה לאינטרנט או בשפת ההוכחה הפורמלית Lean. OpenAI העריכה את התוצאה בעצמה ופרסמה אותה לפני כל אימות רשמי. יומיים אחר כך, ב-21 ביולי 2025, הודיעה Google DeepMind שגרסה מתקדמת של Gemini Deep Think הגיעה לאותו ציון בדיוק — 35 נקודות, אותן חמש בעיות — אך הפעם במסגרת הרשמית: גוגל השתתפה בתחרות כחלק מקבוצת הבדיקה הרשמית הראשונה למערכות AI, ומתאמי ה-IMO ניקדו את התשובות לפי אותם קריטריונים שלפיהם נבדקים מתמודדים אנושיים. נשיא ה-IMO, גרגור דולינר, אישר בפומבי את התוצאה, ודמיס האסאביס, מנכ"ל DeepMind, כינה אותה "הדירוג הרשמי הראשון של ביצועים ברמת זהב למערכת AI". גוגל עצמה כתבה: "הקפיצה שלנו מכסף לזהב בתוך שנה אחת בלבד מראה קצב התקדמות יוצא דופן בבינה מלאכותית". נועם בראון מ-OpenAI כתב שחבר בדירקטוריון ה-IMO ביקש מהחברה לפרסם רק אחרי טקס הפרסים, ושאיש לא ביקש ממנה לחכות עם ההכרזה מעבר לכך. לפי Euronews, רק כעשירית מ-630 המתמודדים האנושיים זכו במדליית זהב באותה תחרות. סם אלטמן, מנכ"ל OpenAI, כתב שכשהחברה רק התחילה, הישג כזה היה "חלום, אבל לא כזה שנראה לנו ממש ריאלי", ושהחברה לא תשיק לציבור מודל ברמה כזו "עוד חודשים רבים".

התשתית: הוכחה פורמלית בשפת Lean, לעומת חיפוש מקורות בשפה טבעית

ההבדל בין AlphaProof לבין מודלי שפה כלליים אינו רק בציון, אלא בסוג האימות. AlphaProof מאמנת את עצמה, בלמידת חיזוק, להוכיח משפטים בשפה הפורמלית Lean — שפה שבה תוכנה יכולה לאמת אוטומטית שכל הוכחה נכונה מבחינה לוגית. AlphaGeometry, הגרסה הראשונה שפרסמה DeepMind בכתב העת Nature ב-17 בינואר 2024, שילבה מודל שפה עם מנוע כללים סימבולי, ופתרה 25 מתוך 30 בעיות גיאומטריה מתחרויות IMO קודמות בתוך זמן התחרות. לשם השוואה, השיטה הקלאסית הקרויה "שיטת וו" פתרה רק 10 מהן. הציון של AlphaGeometry תואר כקרוב לציון הממוצע של זוכה מדליית זהב אנושי. גרסה משודרגת, AlphaGeometry 2, שפורסמה ב-5 בפברואר 2025, הרחיבה את שפת הייצוג כך שתכסה גם תנועת גופים ומשוואות של זוויות, יחסים ומרחקים. היא מכסה 88% מכלל בעיות הגיאומטריה שהוצגו ב-IMO בין 2000 ל-2024, ומשתמשת בגרסה מכווננת של Gemini כדי להציע קווי עזר לחיפוש ההוכחה ולתרגם בעיות מאנגלית לשפת הייצוג הפורמלית.

אוקטובר 2025: טענה שהופרכה על עשר בעיות ארדש פתוחות

ב-12 באוקטובר 2025 כתב סבסטיאן בובק, איש צוות טכני ב-OpenAI, ש-GPT-5-pro הוא "על-אנושי בחיפוש ספרות מחקרית". בעקבות זאת כתב המתמטיקאי מארק סלקה שהמודל זיהה עשר בעיות ארדש המסומנות כפתוחות במסד הנתונים erdosproblems.com, והתקדם חלקית בעוד 11 בעיות. קווין וייל, סמנכ"ל המדע של OpenAI, פרסם — ואז מחק — טענה שהמודל "מצא פתרונות" לעשר בעיות שהיו עד אז בלתי פתורות. תומס בלום, שמנהל את erdosproblems.com, קרא לטענה "ייצוג מוטעה דרמטי": "GPT-5 מצא מקורות שפתרו את הבעיות האלה, מקורות שאני באופן אישי לא הייתי מודע להם." לדבריו, סימון בעיה כ"פתוחה" באתר שלו מציין רק שהוא לא נתקל במאמר שפתר אותה — לא שהיא באמת בלתי פתורה. בפועל GPT-5 לא יצר הוכחות חדשות, אלא אִתר מאמרים קיימים שכללו כבר את הפתרון. במסד הנתונים עצמו רשומים גם מקרים שבהם כלי AI כן הוביל לתוצאה חדשה. למשל, בעיה מספר 397 מסומנת כבעיה שנפתרה בשלילה, ולפי רישום האתר, נל סומני סיפק בעזרת ChatGPT את התשובה השוללת: משפחת פתרונות שמראה שיש אינסוף פתרונות, ולא מספר סופי כפי שהיה משוער.

ינואר 2026: בעיות ארדש ראשונות שנפתרו כמעט באופן אוטונומי

בתחילת ינואר 2026 כתב GPT-5.2 Pro הוכחה לבעיית ארדש מספר 728, ומערכת בשם Aristotle תרגמה אותה לשפה הפורמלית Lean, שבה תוכנה יכולה לאמת שההוכחה נכונה, ובדרך תיקנה אוטומטית כמה שגיאות קטנות. המתמטיקאי טרנס טאו כתב שהבעיה נפתרה "פחות או יותר באופן אוטונומי" בידי ChatGPT, אחרי משוב ראשוני, אך הוסיף הסתייגויות: רמת הקושי של בעיות ארדש משתנה בכמה סדרי גודל, ובעיה שנשארה פתוחה 50 שנה לא בהכרח עמדה בפני מאמצים אנושיים רבים; ייתכן שפשוט איש לא ניסה לפתור אותה ברצינות. לפי הערכתו, רק כאחד עד שניים אחוזים מבעיות ארדש הפתוחות פשוטים מספיק כדי שכלי ה-AI של היום יפתרו אותם בעזרה אנושית מינימלית.

יולי 2026: דיווחים על ציון מלא ב-IMO

ב-IMO 2026 בשנגחאי השתתפו 666 מתמודדים אנושיים, ורק שבעה מהם השיגו ציון מלא. שתי חברות סיניות, Huawei ו-Xiaohongshu, דיווחו שהמודלים שלהן, Celia ו-dots-note-3.0, צברו 42 נקודות מתוך 42. Xiaohongshu מסרה שהפתרונות הוגשו למארגני התחרות לבדיקה, וטענה שעד אז שום מודל שפה לא השיג ציון מלא במסגרת השיפוט הרשמי. במקביל פרסם המשקיע דידי דאס ניסוי פרטי שבו ארבעה מודלים, בהם מודלים של OpenAI ושל Anthropic, קיבלו כולם 42 — תוצאה שלא עברה אימות רשמי.

FrontierMath: אמת המידה שבאמצעותה הוצג o3, בלי לחשוף מי מימן אותה

FrontierMath הוא אוסף של שאלות מתמטיקה ברמת מומחים, שנועד למדוד עד כמה מודלי AI מתקדמים במתמטיקה של חזית המחקר. את האוסף בנתה Epoch AI, עמותת מחקר שממומנת בעיקר על ידי Open Philanthropy. ב-20 בדצמבר 2024, באותו יום שבו הציגה OpenAI את המודל o3 והדגימה את יכולותיו באמצעות FrontierMath, חשפה Epoch AI ש-OpenAI מימנה את יצירת אמת המידה. חלק מהמתמטיקאים שכתבו את השאלות אמרו שלא ידעו על כך לפני הפרסום. ל-OpenAI יש גישה לרוב השאלות והפתרונות של FrontierMath, חוץ מקבוצת שאלות נפרדת שנשמרת חסויה. תמאי בסירוגלו, סגן מנהל Epoch, אמר שקיים הסכם בעל פה שלפיו החברה לא תאמן מודלים על השאלות שנחשפו לה. אליוט גלייזר, המתמטיקאי הראשי של Epoch, אמר אז שהארגון לא יכול לערוב לתוצאות עד שתושלם הבדיקה העצמאית שלו. כשהבדיקה פורסמה, ב-18 באפריל 2025, התברר ש-o3 השיג בה כ-10% בלבד, הרבה פחות מהציון של יותר מ-25% שהציגה OpenAI בדצמבר. לפי Epoch, ייתכן שהפער נובע מכך ש-OpenAI הריצה את המודל במעטפת פנימית חזקה יותר ועל קבוצת שאלות אחרת.