קלוד הוכיח את פרמה ב-11 ימים. פסק דין: SHIP IT.

מה מכסה הסרטון הזה

• קלוד מנסח פורמלית את המשפט האחרון של פרמה ב-Lean 4
• Chromium sandbox RCE (CVE-2026-85046), מנוצל בפועל, פרס של 1,000 דולר
• שין ג'ין-סאו מנצח את KataGo עם מוגבלות של שתי אבנים

תמליל מתורגם

תורגם מהקריינות המקורית באנגלית. זמינות אודיו וכתוביות נשלטת על ידי YouTube.

0:00 פרמה אמר שההוכחה המופלאה שלו לא תתאים בשוליים, והיום Anthropic פרסמה את השוליים: שלושה עשר מיליון שורות של Lean, גדול פי חמישה מ-Mathlib, מוכיח משפט שכל מתמטיקאי כבר האמין בו. זה היה עשר לאחת עשרה בטביליסי כש-Anthropic פרסמה, אז באופן טבעי הייתי ער. אתמול גוגל שחררה את Chrome 152 עם שנים עשר תיקוני אבטחה, אחד מהם באג V8 שכבר נוצל בפועל, ושילמה למדווח אלף דולר, שזה פחות מהסדאן שנגיע אליה בהמשך.

0:26 גם אתמול, Mullvad אמרה שהיא סוגרת את שירות ה-DNS המוצפן הציבורי שלה ב- 2 בנובמבר ומשלמת ל-Quad9 לעשות זאת במקום, והבוקר ה-Rust React Compiler הפך מקורי ב-Vite, בעוד Hacker News גילה את IBM Bob, סוכן קידוד בינה מלאכותית. ואז קלוד ניסח פורמלית את המשפט האחרון של פרמה, ובאותו עמוד ראשון גראנדמאסטר קוריאני ניצח את מנוע הגו החזק ביותר על פני כדור הארץ, אז היום האנושות עשתה אחד משניים. בסרטון זה: מה קלוד באמת הוכיח, מה זה עלה,

0:52 למה המתמטיקאי שבילה את הקריירה שלו על זה אומר שזה לא משנה כלום ו- נרגש בכל זאת, ואיך אנוש ניצח את המכונה בגו. יום שישי, 4 בספטמבר, וזה The Daily Diff. המשפט האחרון של פרמה: אין מספרים שלמים חיוביים a, b, c המקיימים a בחזקת n ועוד b בחזקת n שווה c בחזקת n עבור כל n מעל 2. פרמה שרבט זאת בשוליים בסביבות 1637 ומת בלי להראות את עבודתו, מה שהפך אותו למפתח הראשון שסגר תקלה עם "עובד אצלי במכונה". פרס של 100,000 מרקים מזהב משנת 1908 משך 621

1:25 הוכחות שגויות בשנה הראשונה שלו, ואנדרו ויילס סוף סוף הצליח ב-1995, ב-129 עמודים שלקחו לשופטים חודשים לאמת. לנסח פורמלית פירושו לשכתב את ההוכחה כך ש-Lean, עוזר הוכחות, יוכל לבדוק כל שלב באופן מכני, וקווין באזארד מאימפריאל הוביל מאמץ אנושי לעשות בדיוק את זה מאז 2024; רק התוכנית עצמה היא בת 86 עמודים. חוקר Anthropic, טיאני פנג, הפנה במקום זאת עשרות סוכני קלוד אל זה, בפלטפורמה בשם Prove2Me ששומרת DAG של הצהרות תיאורמה כך שסוכנים יודעים מה להוכיח הבא, כי בלעדיה הלהקות הראשונות

2:00 איבדו מעקב אחר מי מוכיח מה, וזה מה שקורה כששכבת התזמור שלך היא ביטוי רגולרי עם תקציב שיווק. אחד עשר ימים לאחר מכן צומת השורש הראה PROVED: שלושה עשר מיליון שורות של Lean, 29,500 משפטי ביניים, כשישה מיליארד אסימוני פלט מ- מודל פנימי דומה בערך ל-Claude Fable 5.1. הבנייה נכשלת אלא אם ההוכחה מבוססת בדיוק על שלוש האקסיומות הסטנדרטיות של Lean: לא סליחה, אין decide מובנה, אין רמאות. גם בדיקה אינה זולה: בנייה

2:29 מאפס ארכה חמש וחצי שעות על 96 ליבות ו-153 גיגה-בייט RAM, ושמות התיאורמות הם נוצרו על ידי מכונה, כך שהמאגר מתאר את עצמו ככתוב כדי להיבדק ולא כדי להיקרא, וזו גם הדרך שבה הייתי מתאר Java ארגונית. עכשיו הסתירה. הפוסט של Anthropic אומר ש-Lean מדגים נכונות מעבר לכל ספק. קווין באזארד, האיש שנדחק מזה, הידור את המאגר על מכונה של 500 גיגה-בייט ש-Anthropic השאילה לו, אישר שהוא נבדק, ואז כתב,

2:56 ציטוט, מבחינה מתמטית עבודה זו אינה אומרת לנו שום דבר מהותי. הוא כבר היה בטוח ב-99.9 אחוז שהמשפט נכון, וההוכחה אינה מוסיפה מתמטיקה חדשה; מה שהיא מראה זה מה שסיווג אוטומטי יכול לעשות עכשיו, ועל החלק הזה הוא נרגש באמת. הוא קיבל מיליון פאונד במשך חמש שנים; Anthropic לקחה אחד עשר ימים, וחשבון מפינג'אן של פרשן מעמיד שישה מיליארד אסימוני פלט במחיר מחירון. בסביבות 300,000 דולר, כך שהמכונה הייתה זולה יותר, אלא אם כן סופרים את אימון המכונה, מה שאף אחד לא עושה.

3:24 הפרט הטוב ביותר: האימייל הגיע בזמן שהיה בפסטיבל מוזיקה בוויילס עם פס 4G אחד, משם שמעולם לא שמע עליו, אז הוא פטר את זה כמתיחה וקרא אותו שבוע לאחר מכן, וזו התגובה הנכונה לכל שורת נושא המכילה פורמליזציה מקצה לקצה. בינתיים, בני האדם השיגו נקמה. שין ג'ין-סאו, מספר אחד בעולם ב-Go, ניצח את KataGo, מנוע ה-Go החזק ביותר בקוד פתוח, שני משחקים לאחד בסיאול עם שתי אבנים של נכות, בערך הפער בין מקצוען בכיר למקצוען מתחיל.

3:50 המשחק המכריע היה ניצחון של 11.5 נקודות ב-221 מהלכים, תוך שמירה על 99 אחוז סיכוי ניצחון מאמצע המשחק ואילך, והוא לקח הביתה 250 מיליון וון, בערך 170,000 דולר, בתוספת ג'נסיס G90, אז הפרס על ניצחון על AI על-אנושי הוא פי 170 מהפרס של גוגל על יציאה מ-Chrome sandbox. ההסבר שלו: מוקדם יותר הוא העתיק מהלכי AI והפסיד; הוא ניצח על ידי בניית הלוח בסגנון שלו, וזו העצה השימושית ביותר לגבי AI ש שמעתי כל השנה, והיא הגיעה ממשחק לוח. שתי שורות נוספות ב-The Daily Diff.

4:22 מהדר Rust React מבית oxc הוא כעת מקורי ב-Vite מאחורי דגל אחד; בסיס קוד של 1,036 קבצים ירד מ-14.3 שניות ל-0.81 בצעד הקומפילציה, בעיקר על ידי מחיקת Babel מ- package.json, שזו גם שגרת הטיפוח שלי. ו-IBM השיקה את בוב, שותף קידוד בינה מלאכותית שמקבל את פניכם ב"היי, אני בוב", יוצר סוכני משנה, מחדש קוד מיינפריים, ומשגר מוצר אנליטיקה בשם Bobalytics, אז איפשהו בנק מאוד נרגש ואף אחד לא קרא את הרישיון.

4:51 זה הרבה שולי רווח ליום שישי אחד; אם אתם מעדיפים לקרוא את זה מאשר לשמוע אותי אומר את זה, The Daily Diff נוחת בתיבת הדואר הנכנס שלכם כל בוקר – בחינם ב-thedailydiff.dev, קישור למטה. אז, פסק הדין של היום: SHIP IT. הקרנל אומר כן, Buzzard אומר כן, המתמטיקה לא השתנתה, אבל הדרך שבה אנחנו בודקים מתמטיקה בדיוק כן השתנתה. זה ה-The Daily Diff של היום. אני ניקו מ-Axrisi.

5:09 מזגו באחריות.

מקורות

1. Anthropic — Formalizing Fermat's Last Theoremwww.anthropic.com
2. The proof (Lean 4, Apache-2.0)github.com
3. Kevin Buzzard — FLT: Anthropic has beaten me to itxenaproject.wordpress.com
4. HN threadnews.ycombinator.com
5. KED Global — Shin defeats KataGowww.kedglobal.com
6. HNnews.ycombinator.com
7. Chrome 152 release notes (CVE-2026-85046)chromereleases.googleblog.com
8. NVDnvd.nist.gov
9. Mullvad — shutting down public encrypted DNSmullvad.net
10. Rust React Compiler native in Viteblog.master.dev
11. IBM Bobbob.ibm.com