אנתרופיק העלתה הוכחה מלאה של המשפט האחרון של פרמה ב-Lean 4

ההוכחה והכלים שמאחוריה

אנתרופיק פרסמה מאגר המכיל הוכחה מלאה של המשפט האחרון של פרמה, שנבדקה במכונה (machine-checked) ב-Lean 4. ההוכחה נשענת על Mathlib בגרסה 4.33.0, עם Lean 4.33.1 שכולל תיקוני יציבות גרעין (kernel soundness fixes) מ-2026. המבנה עוקב אחר השרשרת הקלאסית של פריי, סר, ריבה, ויילס וטיילור-ויילס, וקובץ PROOF-PATH.md ממפה כל שלב למשפט ה-Lean המתאים לו.

המספרים מאחורי הבנייה

הבנייה מהמקור (from-scratch lake build) כללה 60,475 מודולים, וכל הצהרה נבדקה על ידי הגרעין של Lean. התלות האקסיומטית מצטמצמת לשלוש האקסיומות הסטנדרטיות של Lean, propext, Classical.choice ו-Quot.sound, בלי sorry, בלי אקסיומות נוספות ובלי native_decide. הקובץ FinalCheck.lean מאכף את המגבלה הזו באמצעות #guard_msgs ו-#print axioms, והבנייה נכשלת אם מופיעה תלות נוספת.

אימות כפול בגרעינים נפרדים

שני כלים בלתי תלויים אישרו את התקינות. leanprover/comparator בגרסה 4.33.0 השווה את הסביבה הבנויה מול קובץ אתגר (Challenge.lean) שמנסח את המשפט רק בעזרת Mathlib, ואישר שההצהרה המוכחת וכל הקבועים שהיא מזכירה זהים לאתגר, שאין אקסיומות נוספות, ושכל ההוכחה, כולל Mathlib, עוברת מחדש בגרעין. גרעין עצמאי שני, nanoda 0.4.13 הכתוב ברוסט, קיבל ייצוא של אותה סביבה (דרך lean4export) ובדק 1,052,234 הצהרות בלי שגיאות. ארבעה תיקונים קטנים הוחלו על nanoda, אחד לפלט התקדמות ושלושה להאצת חיפוש שוויון הגדרתי, ואף אחד מהם לא משנה כלל טיפוס (typing rule).

מה מכיל הייצוא הגלוי

תיקיית html, בנפח כ-390 מגהבייט, מציגה את כל המאגר כדפי רשת סטטיים: עמוד לכל אחד מ-29,511 המשפטים עם ההצהרה המדויקת, הציטוטים והתלויות, גרף תלות נפתח, עמוד לכל אחד מ-1,450 מודולי הגדרות, תיבת חיפוש על שמות משפטים והגדרות, גרף משפטי ציון דרך, וגרסאות מרונדרות של README.md, PROOF-PATH.md ו-ATTRIBUTION.md עם קישורים צולבים. התיקייה כלולה במאגר עצמו, כך ששכפול (clone) או הורדת ZIP כבר מכילים אותה.

מעמד הפרויקט ומגבלותיו

המפרסמים מגדירים את הפרויקט כפריט מחקר (research artifact) שאינו מתוחזק ואינו מקבל תרומות. אף מודול אינו מכיל axiom, sorry, native_decide, unsafe, extern, implemented_by, הגדרה חלקית (partial def) או #eval, פרט לקובץ האתגר שמשתמש ב-sorry בכוונה ואינו חלק מהחבילה הנבדקת. הכלים מאמתים שהמשפט נובע משלוש האקסיומות הסטנדרטיות בהינתן אמון בגרעין ובכלי הבדיקה; מה ששום כלי אינו יכול לאמת הוא שכל משפט ביניים אכן מתכוון למה ששמו מרמז, את זה הקורא צריך לשפוט בעצמו, ו-PROOF-PATH.md מציין בדיוק באיזו עוצמה מוכח כל תוצאה קלאסית בשם.