בבלוג של טרנס טאו: תומס היילס מסביר למתמטיקאים מה צריך לדעת על Lean בעידן ה-AI

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

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

מהי הוכחה פורמלית

לפי ההגדרה בפוסט, הוכחה פורמלית היא הוכחה שנבדקה עד הסוף, עד רמת היסודות של המתמטיקה וחוקי הלוגיקה הבסיסיים. בגלל מספר הצעדים העצום הבדיקה נעשית במחשב, בתוכנות שנקראות proof assistants, כלומר עוזרי הוכחה. היילס מונה כמה מהן: HOL Light,‏ Isabelle,‏ Coq (ששמה שונה בשנה שעברה ל-Rocq),‏ Mizar ו-Lean. בקרב מתמטיקאים Lean היא הפופולרית ביותר.

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

Lean ו-mathlib

את Lean פיתח ליאו דה מורה ב-2013, כשעבד במיקרוסופט, והוא שכנע את החברה לשחרר אותה כ-open source (קוד פתוח). ב-2017 הקימו מריו קרניירו ויוהנס הלצל את mathlib, ספרייה של מתמטיקה שעברה פורמליזציה. היום יש בה כמעט 300 אלף משפטים, יותר מ-100 אלף הגדרות ו-2.5 מיליון שורות קוד, שכתבו יותר מ-700 תורמים. כל משפט בספרייה זמין להוכחות חדשות, כך שאין צורך להוכיח אותו שוב.

ההקשר האישי חשוב כאן. היילס ידוע בעיקר כמי שהוכיח את השערת קפלר, ולפי הפוסט ההוכחה הפורמלית שלה דרשה כ-20 שנות עבודה של בני אדם, וכ-500 אלף שורות של proof scripts, כלומר סקריפטים של הוכחה.

autoformalization: החלום הישן מתממש

autoformalization הוא תהליך שבו AI קורא מאמר מתמטי ומפיק ממנו בעצמו הוכחה פורמלית ב-Lean או בכלי דומה. לפי היילס, ב-2026 זה כבר "מציאות מעשית". הוא מונה כמה אבני דרך:

• ספטמבר 2025: חברת Math Inc. ביצעה "כמעט-autoformalization" של משפט המספרים הראשוניים. הוא נקרא "כמעט" כי בני אדם התערבו בכל פעם שה-AI נתקע.
• ינואר 2026: ג'וזף אורבן פרסם preprint (טיוטת מאמר לפני שיפוט) שבו ביצע פורמליזציה אוטומטית של חלקים גדולים מספר הלימוד של מאנקרס בטופולוגיה.
• מרץ 2026: Math Inc. הכריזה על autoformalization של בעיית אריזת הכדורים ב-24 ממדים. התוצאה הייתה כ-500 אלף שורות קוד, שאחר כך קוצצו לכ-200 אלף.
• מאי 2026: קבוצה במטא ביצעה פורמליזציה אוטומטית של חלק גדול מ-26 ספרי לימוד, בפרויקט שנקרא ATLAS.

לפי היילס, הבולט מכולם הוא ה-autoformalization של המשפט האחרון של פרמה, שהכריזה עליו אנתרופיק.

למה זה חשוב

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

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