AI ומתמטיקה פורמלית: גבול חדש שעומד ליפול

מחבר: התלתל (@taltimes2)
תאריך פרסום: 11 בדצמבר 2025
קישור למקור: שרשור מקורי

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

זה שרשור קצר על מתמטיקה פורמלית. ואולי זה גבול חדש שעומד ליפול לבינה המלאכותית.

אולי ראיתם את הכותרות: מערכות בינה מלאכותית של אופןאייעיי ושל גוגל הגיעו לרמת מדליית זהב באולימפיאדה הבינלאומית במתמטיקה 2025 (IMO), עם פתרון של 5 מתוך 6 בעיות, כמו המתחרים האנושיים המובילים.

צצו עכשיו סטארטאפים חדשים שמנסים להפוך את זה לקטגוריה חדשה: “מתמטיקאי מבוסס AI”...

כמה שמות שכדאי להכיר:

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

Harmonic:
סטארטאפ שהוקם על ידי המנכ"ל של רובינהוד ולד טנב, ומתמקד ב“תבונת על מתמטית”...

Epoch
גוף מחקר עצמאי שבודק עד כמה המערכות האלה באמת חזקות בבעיות מתמטיות קשות.

אז מה בעצם השתנה לאחרונה?

המערכת של Harmonic, שנקראת Aristotle, פתרה באופן אוטונומי גרסה מפושטת של בעיה בת 30 שנה מרשימת הבעיות המפורסמת של ארדש...

היא חיפשה רעיונות להוכחה במשך כ־6 שעות, כתבה הוכחה מלאה ב־Lean, והמחשב בדק אותה בפחות מדקה.

בלי התערבות בן אדם. זה די חדש.

(המון הסתייגויות, כמו למשל העובדה שאולי אף בנאדם לא ניסה לפתור את הבעיה הספציפית הזאת אף פעם)...

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

וללמים כליים של מאופןאייעיי ומגוגל כבר הגיעו לציונים ברמת מדליית זהב ב־IMO 2025...

כל זה נשען על רעיון אחד קריטי:

לא רק להאמין לתשובה של הבינה המלאכותית -
לחייב אותו להוכיח את התשובה בשפה פורמלית, כך שמחשב יוכל לאמת כל צעד.
זה הלב של מתמטיקה פורמלית...

אז מה זה “מתמטיקה פורמלית”? זה לא החשבון שלמדנו בביתספר.

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

השפה המפורסמת ביותר בתחום הזה כיום היא Lean.

לין היא:

• שפת תכנות קטנה, וגם
• “עוזר הוכחות” שיכול לבדוק אם הוכחה תקפה במאה אחוז.

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

הנה טעימה קטנה מלין:

ההגדרה של מספר זוגי:

def Even (n : Nat) : Prop :=
  ∃ k : Nat, n = 2 * k

שזה בעברית:

n הוא זוגי אם קיים מספר טבעי k כך ש n=2*k

...

עכשיו ננסה להוכיח משפט מתוחכם: הסכום של שני מספרים זוגיים הוא מספר זוגי.

בלין זה יראה ככה:

theorem even_add
    (a b : Nat)
    (ha : Even a) (hb : Even b) :
    Even (a + b) := by

נתתי למשפט שלנו שם, כתבתי את הנחות היסוד - a, b הם מספרים טבעיים.

אני נותן גם להנחות שלנו שמות, ha, hb זאת אומרת שאני מניח ש a זוגי וגם ש b זוגי

וכותב במפורש את מה שצריך להוכיח: Even (a + b) כלומר שסכום שני מספרים זוגיים הוא זוגי...

ואז ההוכחה נראת כך:

rcases ha with ⟨k, hk⟩

בגלל ש a זוגי יש מספר k שהוא החצי השלם שלו ומעיד עליו

rcases hb with ⟨l, hl⟩

ואותו הדבר יש מספר שלם l שמעיד על זוגיותו של המספר b

refine ⟨k + l, ?_⟩

נגדיר מספר שהוא הסכום של k,l שיהיה עד שלנו להמשך...

ועכשיו צריך לעשות אלגברה:

calc
    a + b = 2 * k + 2 * l := by
      simp [hk, hl]
    _ = 2 * (k + l) := by
      simpa using (Nat.mul_add 2 k l).symm

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

אם הבינה מנסה לנפנף ידיים או לדלג על שלב בהוכחה, לין תדחה את זה.

זה ההבדל הגדול מול צ'טבוטים רגילים: צ'אט - הנה התשובה שלך, סמוך עלי לין - הנה הוכחה שהיא ב 100% נכונה. בדוק...

זה עובד לא רק למתמטיקה - יש ענף שלם של תוכנה ששווה לנו להשקיע כדי לוודא שאין באגים: חוזים חכמים של מטבעות וירטואליים תוכנת בקרה של פצצה גרעינית תוכנת בקרה של גבשושית (זאת המילה?) ששולחים למאדים קריפטוגרפיה

זאת ממש לא שפה כיפית אבל לפעמים המחיר שווה את המאמץ...

וזו בדיוק הסיבה שסטארטאפים כמו Harmonic ו־Axiom קיימים.

המטרה שלהם היא להפוך “הסקה פורמלית” לפרימיטיב חישובי חדש:

• שואלים שאלה בשפה טבעית
• ה AI מחפש רעיונות
• אחר כך הוא כותב הוכחה פורמלית ב- לין
• בודק הוכחות ממוחשב מאשר (או דוחה) את זה

הצנרת הזאת היא המוצר...

מילה על ולד טנב, המנכ"ל של רובינהוד: אז הוא גם בעל תואר במתמטיקה מסטנפורד והוא גם היזם של הרמוניק והוא גם מליארדר בן 38...

Epoch
לא בונים מוצר שאפשר לקנות. הם מתפקדים יותר כמו שופט:

הם מתחזקים את FrontierMath, אוסף בעיות מתמטיות קשות ובלתי מפורסמות ובוחנים מודלים חדשים כדי לבדוק אם הם באמת עושים מתמטיקה חדשה, או רק משווים לתבניות שראו בעבר

הם בונים את “האולימפיאדה של מתמטיקת AI”...

אבל יש כאן ניואנס חשוב שהמתמטיקאי טֶרֶנס טאו מדגיש:

כרגע הבינה מצטיינת בקטיף של פירות "נמוכים” – בעיות שהן טכנית קשות אבל שפשוט לא קיבלו מספיק תשומת לב אנושית.

הבעיות העמוקות והמרכזיות ביותר של המתמטיקה עדיין רחוקות מפתרון...

במילים אחרות, אנחנו כנראה נכנסים למצב של סימביוזה:

הבינה מטפלת באלפי בעיות ברמת קושי בינונית, בודקת הוכחות, וחוקרת מרחבי חיפוש עצומים.
מתמטיקאים אנושיים מתמקדים ברעיונות חדשים, תוכניות מחקר גדולות, והבעיות הקשות ביותר, עם ה־AI כשותף...

לאן אנחנו הולכים?
השלב הבא הוא אימון עצמי (self-play) של מתמטיקה: כמו ש־AlphaGo שיחקה מול עצמה מיליוני משחקים כדי לגלות אסטרטגיות חדשות, כך מערכות מתמטיות יוכלו “לשחק” מול עצמן: להמציא השערות, לנסות להוכיח או להפריך אותן, לשכלל רעיונות, עם הוכחות פורמליות שהמחשב בודק בקפדנות...

וכשמחברים יחד הבנה שפתית חזקה, יכולת להוכיח בלין, בדיקה אוטומטית של הוכחות, ו self-play שמחפש השערות חדשות: מקבלים אבטיפוס של מדען מתמטי אוטונומי. מערכת שלא רק פותרת את מה שנותנים לה, אלא גם מחפשת בעצמה מתמטיקה חדשה. השאלה הגדולה כבר לא אם זה אפשרי, אלא כמה מהר זה יקרה. סוף.