Axiom Math — חברת AI שמתרגמת מתמטיקה לקוד שהמחשב בודק

מה הודיעה Axiom Math בנובמבר 2026

ב-4 בנובמבר 2026 פרסמה Axiom Math, חברת הזנק שנוסדה ב-2025 ומפתחת בינה מלאכותית למתמטיקה, שהשלימה פירמול של ה-Stacks Project בשפה Lean. פירמול פירושו תרגום של מתמטיקה כתובה, במילים ובנוסחאות, לקוד שמחשב יכול לבדוק צעד אחר צעד. לפי החברה, הטקסט המקורי משתרע על כ-7,500 עמודים, והתרגום שלו הניב כ-16 מיליון שורות קוד. TechCrunch, שסיקר את ההודעה ב-5 בנובמבר, כתב על כ-7,654 עמודים. Axiom מתארת את התוצר כ"the largest integrated, reusable library of formalized mathematics ever built" (הספרייה הגדולה ביותר שנבנתה אי פעם של מתמטיקה מפורמלת, משולבת וניתנת לשימוש חוזר). זו טענה של החברה עצמה, וכך גם המספרים. את העבודה עשו, לפי Axiom, נחילים של סוכני AI, תוכנות שמקבלות משימה ומבצעות אותה בכמה צעדים בעצמן. הספרייה פתוחה לציבור באתר נפרד של החברה, שמציג את הטקסט המקורי לצד קוד ה-Lean ואת מפת התלות בין המשפטים, והקוד עצמו מפורסם ב-GitHub ברישיון קוד פתוח Apache 2.0. ב-27 באוקטובר 2026 פרסמה החברה גם פירמול ב-Lean של משפט המיון של החבורות הפשוטות הסופיות.

מה זה ה-Stacks Project

ה-Stacks Project הוא ספר לימוד ועיון פתוח בגיאומטריה אלגברית, ענף מתמטי שחוקר צורות שמוגדרות בעזרת משוואות. את המיזם יזם ב-2005 המתמטיקאי ההולנדי יוהאן דה יונג (Johan de Jong), פרופסור באוניברסיטת קולומביה, והוא גם מתחזק אותו: בודק את השינויים המוצעים ומאשר אותם. לפי Axiom, מאות מתמטיקאים תרמו לו הוכחות, דוגמאות ותיקונים לאורך שני עשורים. לפי ויקיפדיה, באוקטובר 2024 הוא כלל כ-7,500 עמודים ב-116 פרקים. לטענות בו יש תגיות קבועות בנות ארבעה תווים, שבעזרתן אפשר להפנות לכל אחת מהן. ההודעה של Axiom מסבירה למה החומר הזה חשוב: הוא מניח את היסודות של הגיאומטריה האלגברית המודרנית, שבבסיסה תורת הסכמות של אלכסנדר גרותנדיק ושותפיו, והיסודות האלה סיפקו את הכלים להישגים כמו הוכחת השערות וייל בידי פייר דלין והוכחת המשפט האחרון של פרמה בידי אנדרו ויילס. TechCrunch הזכיר שפיטר ווייט (Peter Woit), מתמטיקאי מקולומביה, אמר על ה-Stacks Project שאין לו מקבילה: "nothing else really comparable" (שום דבר אחר שבאמת דומה לו). ווייט השווה אותו ל-"the famous Bourbaki books", סדרת הספרים של בורבקי, שבנתה מחדש את המתמטיקה מיסודותיה במאה ה-20. הדברים נאמרו על המיזם המקורי, לא על העבודה של Axiom.

מה זה אומר שמחשב בודק הוכחה

הוכחה מתמטית רגילה כתובה בשפה טבעית, ומתמטיקאים בודקים אותה בקריאה. בהוכחה ארוכה מאוד, קורא יכול להחמיץ הנחה חסרה או צעד שגוי. Lean היא, בלשון האתר הרשמי שלה, "an open-source programming language and proof assistant" (שפת תכנות בקוד פתוח ועוזר הוכחות). בשפה הזו כותבים את ההגדרות, הטענות וההוכחות כקוד, ורכיב קטן בשם ליבה (kernel) בודק שכל צעד נובע מהקודמים לפי כללי הלוגיקה. אם צעד אחד לא מסתדר, הקוד לא עובר. את Lean מפתח ארגון מחקר ייעודי בשם Lean FRO. סביבו קמה ספרייה קהילתית בשם Mathlib, שלפי אתר Lean כוללת יותר ממיליון שורות של מתמטיקה מפורמלת. הפירמול של Axiom בנוי מעליה. לפי מסמך ההסבר של המאגר ב-GitHub, אין בקוד אף שימוש בפקודה sorry, שמאפשרת לדלג על הוכחה ולהשאיר בה חור. חשוב להבין מה הבדיקה הזו אינה מבטיחה: המחשב מאשר שההוכחה בקוד נכונה, אבל לא שהטענה בקוד אומרת בדיוק את מה שכתוב בספר. לכן Axiom מציינת שהיא בודקת את נאמנות הניסוח לטקסט המקורי בביקורת של כמה סוכנים, בהשוואות לטקסט המקורי ובבדיקות ממוקדות של הגדרות יסוד ומשפטים מרכזיים. גם זה תיאור של החברה, ולא בדיקה חיצונית.

איך זה נעשה: סוכנים שעובדים במקביל

לפי Axiom, החברה בנתה מערכת היררכית של סוכני AI, שבה לכל סוכן תפקיד מוגדר וכללי תיאום נוקשים, אם כי לדברי החברה לא הייתה זו היררכיה מלאה: הסוכנים קיבלו מבנה כללי ופעלו במקביל. הסוכנים מתרגמים טענות, מחפשים ב-Mathlib הגדרות שכבר קיימות, בונים הוכחות ומשלימים טענות עזר שחסרות בדרך. אשווין סוואמינתן, חבר בצוות הטכני של החברה, תיאר ב-TechCrunch את אופן העבודה: "The agents were finding tasks for themselves and identified things that they could work on in parallel" (הסוכנים מצאו לעצמם משימות וזיהו דברים שאפשר לעבוד עליהם במקביל). לפי TechCrunch, החברה אימנה גם מודלים משלה למתמטיקה, ובשלב מוקדם מומחה Lean מצוות החברה לימד את הסוכנים מעין "טעם" מתמטי, כלומר תחושה של איך נראה פירמול טוב. כל טענה בקוד מסומנת בתגית שלה ב-Stacks Project, כך שקורא יכול לעבור מהטקסט לקוד ובחזרה. תגית אחת בספר הופכת לעיתים לכמה הגדרות וטענות בקוד, וחלקן מקושרות ישירות להגדרות שכבר היו ב-Mathlib. החברה לא פרסמה כמה זמן נמשכה העבודה, כמה סוכנים השתתפו בה או כמה כוח מחשוב היא דרשה.

מה נמצא בדרך: טעויות בטקסט המקורי

פירמול אינו רק העתקה. כשטענה בספר לא מצליחה לעבור בדיקה במחשב, זה יכול להיות סימן לבעיה בטענה עצמה. לפי Axiom, המערכת שלה מצאה עשרות טענות ב-Stacks Project שדרשו תיקון מקומי: הנחות שחסרו בניסוח, מקרי קצה שבהם הטענה נכשלת, וטענות שאינן נכונות בכלליות שבה נוסחו. במקרים כאלה הסוכנים בנו דוגמאות נגדיות, כלומר מקרים מפורשים שמראים איפה הטענה המקורית נשברת. כשטענת עזר שגויה הותירה חור בהוכחה של תוצאה מרכזית, הסוכנים חיפשו בספרות המתמטית דרך אחרת להגיע לאותה תוצאה תחת אותן הנחות. לפי Axiom, בהודעה מ-21 באוקטובר 2026 ביקש דה יונג שבינתיים לא יוגשו ישירות למאגר של ה-Stacks Project הערות ובקשות שינוי שנוצרו בידי AI. לכן החברה שומרת את הפירמול, את הדוגמאות הנגדיות ואת התיקונים במאגר משלה, שאינו חלק מהמיזם המקורי, ושם מתמטיקאים יכולים לעיין בהם. ה-Stacks Project נשאר טקסט חי בניהולו של דה יונג וקהילת התורמים.

הסייג: מה בדק אדם ומה רק המחשב

הספרייה של Axiom מחולקת לשני חלקים, לפי אתר הפרויקט ומסמך ההסבר במאגר. StacksCore מכיל פירמולים שאדם בדק מול הטקסט המקורי, והותאמו לסטנדרט של Mathlib בשמות, בכלליות ובסגנון. StacksFrontier מכיל קוד שכתבו סוכני AI ועדיין לא עבר את הבדיקה הזו. בלשון החברה זה החלק שבו הכיסוי גדל הכי מהר, "and where review is most needed" (ושבו הכי נדרשת ביקורת), לפני שהקוד יעבור ל-StacksCore. Lean בודק את ההוכחות בשני החלקים, אבל רק בראשון עבר גם אדם על הניסוח. המשמעות לקורא: "16 מיליון שורות שנבדקו במחשב" פירושו שכל ההוכחות תקינות מבחינה לוגית, ולא שמתמטיקאים אישרו שכל טענה בקוד תואמת את הספר. החברה לא פרסמה איזה חלק מהקוד כבר נמצא ב-StacksCore. עוד סייג: לפי מסמך ההסבר, פורמלו כל התגיות שיש בהן תוכן שאפשר לפרמל, אבל דוגמאות, תרגילים והערות שעדיין לא פורמלו נשארו משימות לתורמים. גם התואר "הספרייה הגדולה ביותר" הוא תיאור של החברה עצמה.

למה זה חשוב: אימות מול שטף של טענות

TechCrunch הציג את המהלך על רקע מה שמכונה AI slop, שטף של תוכן שנוצר בבינה מלאכותית בלי בדיקה. הכתבה פותחת בכך ש-OpenAI פרסמה אוסף של 719 כתבי יד שטוענים לפתרון של כמה מהבעיות הקשות בתחום. האוסף פורסם ב-6 באוקטובר 2026, ומספר כתבי היד בו השתנה בימים שאחרי הפרסום. אלה טענות, ולא תוצאות שנבדקו. Axiom כותבת שכאשר מערכות AI מייצרות טיעונים מתמטיים מהר מכפי שבני אדם יכולים לבדוק, אימות במחשב נעשה הכרחי, ושהליבה של Lean מבטיחה שכל תוצאה מצוטטת משמשת רק כשההנחות שלה מתקיימות במדויק. ספרייה מפורמלת גדולה היא גם תשתית: חוקרים וסוכני AI יכולים לייבא ממנה הגדרות ומשפטים ישר להוכחות חדשות. TechCrunch הביא גם משפט כללי של טרנס טאו, מתמטיקאי מ-UCLA וזוכה מדליית פילדס, על הוכחות מפורמלות באופן כללי, ולא על העבודה הזו: "The more formalized proofs you have, the more formalized proofs you can make" (ככל שיש לך יותר הוכחות מפורמלות, כך אתה יכול לייצר יותר הוכחות מפורמלות). לפי TechCrunch, Axiom מהמרת שגם התוכנה של העתיד תצטרך לעמוד על יסודות מאומתים, כמו ה-Stacks Project עכשיו, ורוצה לבנות בסיס שסוכני AI יוכלו לסמוך עליו כשהם כותבים תוכנה. ב-12 במרץ 2026 הודיעה קרן Menlo Ventures שהובילה סבב גיוס A של 200 מיליון דולר ב-Axiom Math, לפי שווי של 1.6 מיליארד דולר אחרי הגיוס. בסוף הכתבה ב-TechCrunch הציבה מייסדת החברה ומנכ"ליתה, קרינה הונג (Carina Hong), אתגר לחברות אחרות: "I openly challenge all the coding companies to work on formalization at this scale" (אני מאתגרת בגלוי את כל חברות התכנות לעבוד על פירמול בהיקף כזה).