Lean, מוכיח המשפטים, מתמודד עם שאלות אמינות כשהאוטופורמליזציה של AI מתפתחת

פורמליזציה ואוטופורמליזציה

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

אוטופורמליזציה, שבה AI קורא מאמר ומפיק הוכחה פורמלית, הפכה למציאות מעשית ב-2026. אבני דרך בולטות כוללות: קוואזי-אוטופורמליזציה של משפט המספרים הראשוניים בידי Math Inc. בספטמבר 2025, פורמליזציה של חלק גדול מספר הלימוד של Munkres לטופולוגיה, בעיית אריזת הספירות ב-24 ממדים, אוטופורמליזציה של המשפט האחרון של פרמה בידי Anthropic ב-4 בספטמבר, שהפיקה 13 מיליון שורות Lean ב-11 ימים, ופורמליזציה של התפוצצות Navier-Stokes בידי OpenAI, שהוכרזה ב-8 בספטמבר.

עיצוב ומודל אמינות

Lean משלב שפת תכנות לשימוש כללי עם שפה מתמטית להגדרות, לניסוח משפטים ולסקריפטים של הוכחות. את סקריפטי ההוכחות מנתח, מריץ ובודק הליבה של Lean, כמה אלפי שורות קוד C++. בפוסט מודגש שאין להאמין להוכחות Lean לפני שהליבה בדקה אותן, ונדרש ביקורת אנושית נפרדת כדי לאשר את נאמנות הניסוח, שהמשפט המאומת הוא אכן המשפט שהתמטיקאים התכוונו אליו.

קיץ תקלות האמינות

תקלת אמינות היא תקלה בליבה שמאפשרת הוכחה של „False“, ולכן של כל טענה. כמה תקלות כאלה ב-Lean התגלו ביולי ובאוגוסט 2026, ולכך קוראים כיום קיץ תקלות האמינות. תקלה אחת גרמה לשלילה בלתי חוקית של השערת קולץ, והשנייה להוכחה קצרה ובלתי חוקית של השערת קפלר. כולן תוקנו במהירות, ו-mathlib נבדק עם הליבה המתוקנת.

הצעות ובעיות פתוחות

נבחנות שלוש תגובות. ראשית, כתבו ליבות Lean נוספות ובדקו הוכחות לרוחב; קיימות כ-25 ליבות, והפורמליזציה של Navier-Stokes אומתה בידי יותר מעשרה בודקי הוכחות. שנית, אמתו את הליבה באופן פורמלי, כפי שעשה יואכים ברייטבר עם Con-Leche, ליבת Lean מאומתת שהוכחת העקביות שלה נוצרה עם Claude ושהיא בדקה את mathlib. שלישית, העמיקו את ההבנה התאורטית של תורת הטיפוסים של Lean, שבה טיפוסיות ייחודית, Pi-אינג'קטיביות, תכונת Church-Rosser שהשתנתה והוכחת עקביות יחסית ציבורית מלאה עדיין פתוחות. הפוסט מסתיים בציטוט מתוך „Reflections on Trusting Trust“ מאת קן תומפסון ומזהיר שאמון עיוור במערכות כמו Lean אינו אפשרי עוד.

מקורות: terrytao.wordpress.com