# أثبت كلود مبرهنة فيرما في 11 يومًا. الحكم: SHIP IT.

Published: 2026-09-07

أمضى كلود 11 يومًا وحوالي 6 مليارات رمز في كتابة برهان Lean لمبرهنة فيرما الأخيرة المكون من 13 مليون سطر - وهو أول برهان يتم التحقق منه بواسطة الكمبيوتر بالكامل - بينما يقول عالم الرياضيات الذي يقوم بصياغته منذ عام 2024 إنه "لا يخبرنا شيئًا جوهريًا" رياضيًا، وهو سعيد على أي حال. في نفس اليوم: يهزم شين جين سيو المصنف الأول عالميًا في لعبة غو، KataGo بنتيجة 2-1 مع إعاقة بحجرين. الحكم: SHIP IT.

Canonical: https://thedailydiff.dev/ar/video/2026-09-04-fermat-lean/

## ما يغطيه هذا الفيديو

- كلود يصيغ مبرهنة فيرما الأخيرة في Lean 4
- Chromium sandbox RCE (CVE-2026-85046)، تم استغلاله في الواقع، مكافأة 1000 دولار
- شين جين سيو يهزم KataGo بإعاقة بحجرين

## النص المترجم

مترجم من السرد الإنجليزي الأصلي. يتم التحكم في الصوت والتعليقات التوضيحية المتاحة بواسطة YouTube.

0:00 قال فيرما إن إثباته الرائع لن يتناسب مع الهامش، واليوم نشرت Anthropic الهامش: ثلاثة عشر مليون سطر من Lean، خمسة أضعاف حجم Mathlib، تثبت مبرهنة كان كل عالم رياضيات يعتقدها بالفعل. كانت الساعة العاشرة إلى الحادية عشرة في تبليسي عندما نشرت Anthropic، لذلك بطبيعة الحال كنت مستيقظًا. أمس، أطلقت جوجل Chrome 152 مع اثني عشر إصلاحًا أمنيًا، أحدها خطأ في V8 تم استغلاله بالفعل في الواقع، ودفعت للمبلغ ألف دولار، وهو أقل من السيارة السيدان التي سنتطرق إليها لاحقًا.

0:26 أيضًا أمس، قالت Mullvad إنها ستغلق نظام DNS المشفر العام الخاص بها في الثاني من نوفمبر وستدفع لـ Quad9 للقيام بذلك بدلاً من ذلك، وهذا الصباح، انتقل مترجم Rust React إلى العمل الأصلي في Vite، بينما اكتشف Hacker News IBM Bob، وكيل ترميز بالذكاء الاصطناعي. ثم قام كلود بصياغة مبرهنة فيرما الأخيرة، وفي نفس الصفحة الأولى، هزم أستاذ كوري كبير أقوى محرك Go على وجه الأرض، لذا اليوم حققت الإنسانية واحدًا من اثنين. في هذا الفيديو: ما أثبته كلود بالفعل، وما كلفه ذلك،

0:52 لماذا يقول عالم الرياضيات الذي أمضى حياته المهنية في هذا إن ذلك لا يغير شيئًا و هو سعيد على أي حال، وكيف هزم إنسان الآلة في Go. إنه الجمعة، 4 سبتمبر، وهذا هو The Daily Diff. مبرهنة فيرما الأخيرة: لا توجد أعداد صحيحة موجبة a، b، c تحقق a أس n زائد b أس n يساوي c أس n لأي n أكبر من 2. كتبها فيرما على هامش ورقة حوالي عام 1637 وتوفي دون إظهار عمله، مما يجعله أول مطور يغلق تذكرة بعبارة "يعمل على جهازي". جائزة عام 1908 بقيمة 100,000 مارك ذهبي جذبت 621 إثباتًا خاطئًا

1:25 في عامها الأول، وحصل عليها أندرو ويلز أخيرًا في عام 1995، في 129 صفحة استغرقت المحكمين شهورًا للتحقق منها. التحويل إلى صيغة رسمية يعني إعادة كتابة هذا الإثبات بحيث يمكن لـ Lean، وهو مساعد إثبات، التحقق من كل خطوة ميكانيكيًا، وقد قاد كيفن بوزارد في إمبريال جهدًا بشريًا للقيام بذلك بالضبط منذ عام 2024؛ المخطط وحده يبلغ 86 صفحة. بدلاً من ذلك، وجه الباحث في Anthropic تياني بنغ العشرات من وكلاء كلود إليها على منصة تسمى Prove2Me تحتفظ بـ DAG من عبارات المبرهنات لكي يعرف الوكلاء ما يجب إثباته بعد ذلك، لأنه بدونها، فقدت الأسراب الأولى

2:00 تتبع من كان يثبت ماذا، وهذا ما يحدث عندما تكون طبقة التنسيق الخاصة بك عبارة عن تعبيرات منتظمة بميزانية تسويقية. بعد أحد عشر يومًا، قرأت العقدة الجذرية PROVED: ثلاثة عشر مليون سطر من Lean، 29,500 مبرهنة وسيطة، حوالي ستة مليارات رمز إخراج من نموذج داخلي قابل للمقارنة تقريبًا مع Claude Fable 5.1. يفشل البناء ما لم يعتمد الإثبات على بديهيات Lean الثلاث القياسية بالضبط: لا آسف، لا يوجد قرار أصلي، لا غش. التحقق من ذلك ليس رخيصًا أيضًا: استغرق البناء

2:29 من الصفر خمس ساعات ونصف على 96 نواة و 153 جيجابايت من ذاكرة الوصول العشوائي، وأسماء المبرهنات هي مولدة آليًا، لذا يصف المستودع نفسه بأنه مكتوب ليتم التحقق منه بدلاً من قراءته، وهذا أيضًا كيف أصف 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 دولار، بالإضافة إلى Genesis G90، لذا فإن المكافأة مقابل هزيمة ذكاء اصطناعي فائق هي 170 ضعف مكافأة جوجل لهروب Chrome sandbox. تفسيره: في البداية قلد حركات الذكاء الاصطناعي وخسر؛ فاز عن طريق بناء اللوحة بأسلوبه الخاص، وهي النصيحة الأكثر فائدة حول الذكاء الاصطناعي التي سمعتها هذا العام، وجاءت من لعبة لوحية. سطران آخران في The Daily Diff.

4:22 مترجم Rust React من oxc أصبح الآن أصليًا في Vite خلف علامة واحدة؛ قاعدة بيانات بـ 1,036 ملفًا انتقلت من 14.3 ثانية إلى 0.81 في خطوة الترجمة، وذلك أساسًا بحذف Babel من package.json، وهو أيضًا روتيني للعناية بالبشرة. وأطلقت IBM Bob، شريك برمجة الذكاء الاصطناعي الذي يرحب بك بـ مرحبًا، أنا Bob، ينشئ وكلاء فرعيين، يحدّث رمز المين فريم، ويشحن منتج تحليلات يسمى Bobalytics، لذا ففي مكان ما يوجد بنك متحمس جدًا ولم يقرأ أحد الترخيص.

4:51 هذا هامش كبير ليوم جمعة واحد؛ إذا كنت تفضل قراءة هذا بدلاً من سماعي أقوله، فإن The Daily Diff يصل إلى صندوق بريدك كل صباح — مجانًا على daily diff dot dev، الرابط أدناه. إذًا، حكم اليوم: SHIP IT. النواة تقول نعم، Buzzard يقول نعم، الرياضيات لم تتغير، لكن الطريقة التي نتحقق بها من الرياضيات تغيرت للتو. هذا هو The Daily Diff اليوم. أنا نيكو من Axrisi.

5:09 ادمج بمسؤولية.

## المصادر

- [Anthropic — Formalizing Fermat's Last Theorem](https://www.anthropic.com/research/formalizing-fermats-last-theorem) — www.anthropic.com
- [The proof (Lean 4, Apache-2.0)](https://github.com/anthropics/fermats-last-theorem) — github.com
- [Kevin Buzzard — FLT: Anthropic has beaten me to it](https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/) — xenaproject.wordpress.com
- [HN thread](https://news.ycombinator.com/item?id=49568506) — news.ycombinator.com
- [KED Global — Shin defeats KataGo](https://www.kedglobal.com/artificial-intelligence/newsView/ked202607210007) — www.kedglobal.com
- [HN](https://news.ycombinator.com/item?id=49544762) — news.ycombinator.com
- [Chrome 152 release notes (CVE-2026-85046)](https://chromereleases.googleblog.com/2026/09/stable-channel-update-for-desktop_01882797386.html) — chromereleases.googleblog.com
- [NVD](https://nvd.nist.gov/vuln/detail/cve-2026-85046) — nvd.nist.gov
- [Mullvad — shutting down public encrypted DNS](https://mullvad.net/en/blog/shutting-down-our-public-encrypted-dns-servers-and-sponsoring-quad9-instead) — mullvad.net
- [Rust React Compiler native in Vite](https://blog.master.dev/react-now-rusted-all-the-way-out/) — blog.master.dev
- [IBM Bob](https://bob.ibm.com/) — bob.ibm.com