בכתבה הזו
המתמטיקאי תומאס הילס, המחבר הראשי של המאמר על ההוכחה הפורמלית של השערת קפלר, פרסם בבלוג של טרנס טאו (9 באוקטובר 2026) פוסט אורח על מידת האמינות של Lean, כלי ההוכחות הפופולרי ביותר בקרב מתמטיקאים. הפוסט מגיע אחרי "קיץ הבאגים", שבו נמצאו ב-Lean פגמים שאפשרו להוכיח טענות שקריות. לפי הילס, התקלות הללו דווקא מעידות על בריאות המערכת, אך שאלות יסוד על התאוריה שמאחוריה עדיין פתוחות.
מהי הוכחה פורמלית ומה השתנה ב-2026
הוכחה פורמלית היא הוכחה שנבדקה עד לרמת היסודות של המתמטיקה והלוגיקה, בדרך כלל באמצעות תוכנה ייעודית שנקראת "עוזר הוכחות". Lean, שפותח ב-2013 על ידי ליאו דה מורה במיקרוסופט, היא התוכנה הפופולרית ביותר בתחום. ספריית mathlib שלה כוללת כמעט 300,000 משפטים, 2.5 מיליון שורות קוד ויותר מ-700 תורמים.
בעבר, תרגום של הוכחה מנייר לצורה פורמלית נעשה ידנית. ההוכחה הפורמלית של השערת קפלר, למשל, דרשה כ-20 שנות עבודה אנושיות. לדברי הילס, ב-2026 הפכה "אוטופורמליזציה", כלומר תרגום אוטומטי של מאמרים להוכחות פורמליות בידי בינה מלאכותית, למציאות מעשית. הוא מונה כמה אבני דרך: Math Inc. הציגה ב-2025 תרגום חלקי של משפט המספרים הראשוניים, וב-2026 של בעיית אריזת הכדורים בממד 24 (כ-500 אלף שורות שקוצרו לכ-200 אלף). קבוצה ב-Meta תרגמה חלק גדול מ-26 ספרי לימוד. לפי הפוסט, Anthropic הודיעה ב-4 בספטמבר על תרגום המשפט האחרון של פרמה ב-13 מיליון שורות Lean תוך 11 ימים, ו-OpenAI הודיעה ב-8 בספטמבר על הוכחת התפוצצות במשוואות נבייה-סטוקס עם כוח חיצוני, בליווי תרגום ל-Lean. הנתונים האלה מבוססים על הפוסט של הילס ולא נבדקו כאן באופן עצמאי.
קיץ הבאגים
הבאג החמור ביותר במערכת כזו הוא פגם בליבת הבדיקה של המערכת (ה"קרנל") שמאפשר להוכיח "שקר", ומכאן כל טענה שהיא. זו התקלה החמורה ביותר שיכולה לקרות בעוזר הוכחות. לדברי הילס, באחד הבאגים הוכחה בטעות הפרכה של השערת קולאץ, ובאחר הוכחה קצרה ובלתי חוקית של השערת קפלר.
הפוסט של דה מורה, שנכתב באוגוסט, מפרט את ציד הבאגים. דניאל סלסם מ-OpenAI השתמש במודלים פנימיים של החברה, ובין 30 ביולי ל-20 באוגוסט איתר פגמים בקרנל ובסביבת הריצה של Lean. לפי דה מורה, אותו מודל פנימי מצא בסוף התהליך שני ניצולים בסביבת הריצה: דרך לגרום לגלישה של מונה ההפניות של אובייקט בזיכרון ולהוכיח "שקר", והעובדה שהגרסה של Lean ללינוקס נבנתה עם גרסה ישנה של ספריית החשבון GMP שכוללת באג ידוע. התיקונים שוחררו ב-21 באוגוסט בגרסה 4.33.1. הקבוצות שהשתמשו במודלים זמינים לציבור לא דיווחו על באגים.
הילס רואה בכך התפתחות חיובית: הבאגים נחשפו בידי חוקרי אבטחה שעבדו עם מודלים מתקדמים, ולא בידי תוקפים, וכולם תוקנו. mathlib נבדקה מחדש עם הקרנל המתוקן.
שלוש דרכים להפחית סיכון
הילס דן בשלוש גישות. הראשונה היא כתיבת קרנלים נוספים ובדיקה צולבת. כ-25 קרנלים ל-Lean כבר נכתבו, וההוכחה של נבייה-סטוקס אושרה על ידי יותר מתריסר בודקים. אבל בדיקה צולבת אינה מושלמת: באג הקולאץ לא נתפס על ידי קרנל Nanoda, שהיה מיושן וסבל מבאג משלו. הילס מציע קרנל שנכתב ב"חדר נקי", בלי להסתכל בקוד הקיים.
הגישה השנייה היא אימות פורמלי של הקרנל עצמו. משפט האי-שלמות השני של גדל מגביל את מה שאפשר להשיג: לכל היותר הוכחת עקביות יחסית. ב-10 בספטמבר פרסם יואכים ברייטנר קרנל מאומת בשם Con-Leche, שנכתב ב-Lean עם קוד והוכחות שיצר Claude. הילס מכנה זאת אחד מאבני הדרך החשובות בתולדות Lean, אך מציין שההוכחה מניחה הנחות לגבי המהדר, סביבת הריצה והחומרה.
הגישה השלישית היא העמקת ההבנה התאורטית של תורת הטיפוסים שמאחורי Lean.
שאלות שעדיין פתוחות
כאן הילס ביקורתי. המסמך המכונן של התאוריה, עבודת התזה של מריו קרנירו מ-2019, כולל שגיאה שנמצאה, ומתייחס לגרסה ישנה של Lean. תכונות בסיסיות, כמו טיפוס יחיד לכל ביטוי, עדיין לא הוכחו. ועל השאלה החשובה מכולן, עקביות של התאוריה ביחס לתורת הקבוצות, הילס כותב שהוא אינו מכיר הוכחה מלאה ופומבית נכון לאוקטובר 2026. Con-Leche מוכיח טענה קרובה, אך לא זהה.
הילס מסכם שהקהילה המתמטית לא נותנת מספיק תשומת לב לשאלות היסוד האלה, ושאם מתמטיקאים עוברים מתורת הקבוצות לתורת הטיפוסים, צריך לחזק את התשתית התאורטית.
ומה עם נאמנות ההצהרה
הילס מדגיש עוד נקודה: גם הוכחה שעברה את הקרנל צריכה ביקורת אנושית שתוודא שהמשפט שאומת הוא באמת המשפט המיועד, ושההגדרות ב-Lean תואמות את המשמעות הצפויה. לדבריו, משימה זו קלה בהרבה מבדיקת ההוכחה עצמה. כלי בשם comparator מסייע בכך. השאלה עד כמה אוטופורמליזציה מדויקת בהתאמת הניסוח הפורמלי למשפט המקורי נשארת פתוחה, והפוסט אינו מכריע בה.
יש לציין: הפוסט עצמו הומר מפורמט קובץ אחר באמצעות בינה מלאכותית, כפי שצוין בו.
תגובות