תגית: Lean 4

מאמר בן 76 עמודים שפורסם ב־arXiv מתאר פריצת דרך תאורטית באלגוריתמים, ומייחס את גילוי הרעיון המרכזי למודל Claude של Anthropic. לפי המחברים, האלגוריתמים משפרים את החסמים המוכרים לשתי בעיות יסוד: 3SUM, שבודקת אם שלושה מספרים מסתכמים לאפס, ו־APSP, שמחשבת את המרחקים הקצרים ביותר בין כל זוג צמתים בגרף.

המאמר מציג זמן ריצה של O(n^1.9992) עבור 3SUM ושל O(n^2.9995) עבור APSP. השיפורים קטנים מבחינת המעריכים, אבל משמעותיים מבחינה תאורטית: הם מפריכים את השערות 3SUM ו־APSP, שלפיהן אין אלגוריתמים שמשיגים שיפור פולינומי מתחת לחסמים המקובלים. התוצאות תקפות לתנאי הקלט המפורטים במאמר — בין היתר, מספרים או משקלים שלמים בעלי גודל פולינומי.

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

מה תפקידו של Lean 4?

המחברים מדווחים כי Claude גם אימת את התוצאות המרכזיות בעזרת Lean 4 וספריית Mathlib — כלים לבניית בדיקות פורמליות של הוכחות מתמטיות. לפי המאמר, החוקרים עבדו לאחר מכן כדי להבין, לפשט, לחזק ולהרחיב את האלגוריתם. האימות הפורמלי הוא חלק מהדיווח של המחברים; הוא אינו מחליף קריאה ובחינה של הטענות המדעיות.

למאמר המלא ב־arXiv.