کلاڈ نے 11 دنوں میں فرما کا نظریہ ثابت کر دیا۔ فیصلہ: SHIP IT۔

اس ویڈیو میں کیا شامل ہے

• کلاڈ نے فرما کے آخری نظریہ کو لین 4 میں رسمی شکل دی۔
• کرومیم سینڈ باکس آر سی ای (CVE-2026-85046)، میدان میں استعمال کیا گیا، $1,000 کا انعام
• شن جن-سیو نے کاتاگو کو دو پتھروں کی ہینڈی کیپ کے ساتھ ہرا دیا۔

ترجمہ شدہ ٹرانسکرپٹ

اصل انگریزی بیان سے ترجمہ کیا گیا۔ دستیاب آڈیو اور کیپشنز یوٹیوب کے زیر انتظام ہیں۔

0:00 فرما نے کہا تھا کہ اس کا حیرت انگیز ثبوت حاشیے میں نہیں سمائے گا، اور آج Anthropic نے وہ حاشیہ شائع کر دیا: لین کی تیرہ ملین لائنیں، میتھلب کے حجم سے پانچ گنا زیادہ، ایک ایسا نظریہ ثابت کرتے ہوئے جس پر ہر ریاضی دان پہلے ہی یقین رکھتا تھا۔ جب Anthropic نے پوسٹ کیا تو تبلیسی میں دس سے گیارہ بجے کا وقت تھا، تو قدرتی طور پر میں جاگ رہا تھا۔ کل گوگل نے بارہ سیکیورٹی فکسز کے ساتھ کروم 152 جاری کیا، ان میں سے ایک V8 بگ تھا جو پہلے ہی میدان میں استعمال ہو چکا تھا، اور رپورٹر کو ایک ہزار ڈالر ادا کیے، جو اس سیڈان سے کم ہے جس کا ذکر ہم بعد میں کریں گے۔

0:26 کل ہی، Mullvad نے کہا کہ وہ 2 نومبر کو اپنی عوامی انکرپٹڈ DNS بند کر رہا ہے اور اس کے بجائے Quad9 کو یہ کام کرنے کے لیے ادا کر رہا ہے، اور آج صبح Rust React کمپائلر Vite میں مقامی ہو گیا، جبکہ ہیکر نیوز نے IBM Bob کو دریافت کیا، ایک AI کوڈنگ ایجنٹ۔ پھر کلاڈ نے فرما کے آخری نظریہ کو رسمی شکل دی، اور اسی پہلے صفحے پر ایک کورین گرینڈ ماسٹر نے زمین کے سب سے طاقتور گو انجن کو ہرا دیا، تو آج انسانیت ایک کے مقابلے میں دو پر رہی۔ اس ویڈیو میں: کلاڈ نے دراصل کیا ثابت کیا، اس کی کیا لاگت آئی،

0:52 کیوں اس ریاضی دان نے جس نے اپنی پوری زندگی اس پر صرف کی، کہا کہ اس سے کچھ نہیں بدلا اور پھر بھی وہ بہت خوش ہے، اور کیسے ایک انسان نے گو میں مشین کو ہرا دیا۔ یہ جمعہ، 4 ستمبر ہے، اور یہ The Daily Diff ہے۔ فرما کا آخری نظریہ: کوئی مثبت صحیح اعداد a, b, c a کی n طاقت جمع b کی n طاقت برابر c کی n طاقت کو کسی بھی n کے لیے 2 سے زیادہ پر پورا نہیں کرتے۔ فرما نے اسے تقریباً 1637 میں ایک حاشیے میں لکھ دیا اور اپنا کام دکھائے بغیر وفات پا گئے، جس سے وہ پہلے ڈویلپر بن گئے جنہوں نے 'works on my machine' کے ساتھ ایک ٹکٹ بند کیا۔ 1908 کا 100,000 سونے کے مارکس کا انعام پہلے سال میں 621 غلط

1:25 ثبوتوں کو اپنی طرف متوجہ کیا، اور اینڈریو وائلز نے بالآخر 1995 میں اسے حاصل کیا، 129 صفحات میں جسے ریفریوں کو تصدیق کرنے میں مہینوں لگے۔ رسمی شکل دینے کا مطلب ہے اس ثبوت کو دوبارہ لکھنا تاکہ Lean، ایک پروف اسسٹنٹ، ہر قدم کو میکانیکی طور پر چیک کر سکے، اور امپیریل میں کیون بزارڈ نے 2024 سے اس کام کو کرنے کے لیے انسانی کوشش کی قیادت کی ہے؛ صرف بلیو پرنٹ 86 صفحات پر مشتمل ہے۔ Anthropic کے محقق تیانئی پینگ نے اس کے بجائے درجنوں کلاڈ ایجنٹوں کو اس پر لگایا، ایک پلیٹ فارم پر جسے Prove2Me کہتے ہیں جو تھیوریم کے DAG کو بیانات رکھتا ہے تاکہ ایجنٹس کو پتہ چلے کہ اگلا کیا ثابت کرنا ہے، کیونکہ اس کے بغیر پہلی

2:00 ٹولیاں یہ بھول گئیں کہ کون کیا ثابت کر رہا تھا، جو تب ہوتا ہے جب آپ کی آرکیسٹریشن لیئر مارکیٹنگ بجٹ کے ساتھ ریگیکس ہو۔ گیارہ دن بعد روٹ نوڈ نے PROVED پڑھا: لین کی تیرہ ملین لائنیں، 29,500 درمیانی تھیوریم، ایک داخلی ماڈل سے تقریباً چھ بلین آؤٹ پٹ ٹوکن جو تقریباً Claude Fable 5.1 کے برابر ہے۔ تعمیر ناکام ہو جاتی ہے جب تک کہ ثبوت صرف لین کے تین معیاری axioms پر مبنی نہ ہو: نہیں معاف کیجیے، کوئی نیٹو فیصلہ نہیں، کوئی دھوکہ دہی نہیں۔ اسے چیک کرنا بھی سستا نہیں: ایک

2:29 ابتداء سے تعمیر میں ساڑھے پانچ گھنٹے لگے 96 کور اور 153 گیگا بائٹس ریم پر، اور تھیوریم کے نام مشین سے تیار کیے گئے ہیں، لہذا ریپو خود کو پڑھنے کے بجائے چیک کرنے کے لیے لکھا گیا بیان کرتی ہے، جو میں انٹرپرائز جاوا کے بارے میں بھی کہوں گا۔ اب تضاد۔ Anthropic کی پوسٹ کہتی ہے کہ لین بے شک درستگی کو ظاہر کرتا ہے۔ کیون بزارڈ، وہ شخص جسے اس میں مات دی گئی، اس نے ریپو کو ایک 500 گیگا بائٹ مشین پر کمپائل کیا جو Anthropic نے اسے دی تھی، تصدیق کی کہ یہ چیک ہوتا ہے، اور پھر لکھا،

2:56 اقتباس، ریاضیاتی طور پر یہ کام ہمیں عملی طور پر کچھ نہیں بتاتا۔ وہ پہلے ہی 99.9 فیصد یقین کر چکا تھا کہ تھیوریم صحیح تھا، اور ثبوت کوئی نئی ریاضی شامل نہیں کرتا؛ یہ جو دکھاتا ہے وہ یہ ہے کہ آٹو فارملائزیشن اب کیا کر سکتی ہے، اور اس حصے کے بارے میں وہ واقعی پرجوش ہے۔ اسے پانچ سالوں میں دس لاکھ پاؤنڈ دیے گئے؛ Anthropic کو گیارہ دن لگے، اور ایک تبصرہ نگار کے ابتدائی اندازے کے مطابق چھ بلین آؤٹ پٹ ٹوکن کی فہرست قیمت بنتی ہے۔ تقریباً 300,000 ڈالرز، تو مشین سستی تھی، جب تک آپ مشین کی تربیت کو شمار نہ کریں، جو کوئی نہیں کرتا۔

3:24 بہترین تفصیل: ای میل اس وقت پہنچی جب وہ ویلز میں ایک میوزک فیسٹیول میں تھا جس میں 4G کا ایک بار تھا، ایک ایسے نام سے جسے اس نے کبھی نہیں سنا تھا، اس لیے اس نے اسے ایک کرینک سمجھ کر رد کر دیا اور اسے ایک ہفتے بعد پڑھا، جو کہ کسی بھی سبجیکٹ لائن کے لیے درست ردعمل ہے جس میں 'end-to-end formalization' شامل ہو۔ اس دوران، انسانوں نے ایک جیت حاصل کی۔ شن جن-سیو، گو میں دنیا کا نمبر ایک، نے KataGo کو شکست دی، سب سے مضبوط اوپن سورس گو انجن، سیول میں دو کھیلوں میں ایک کے مقابلے میں دو پتھر کے ہینڈی کیپ کے ساتھ، تقریباً ایک ٹاپ پروفیشنل اور ایک روکی پروفیشنل کے درمیان کا فرق۔

3:50 فیصلہ کن میچ 221 چالوں میں 11.5 پوائنٹس کی جیت تھی، جس میں درمیانی کھیل سے 99 فیصد جیتنے کا امکان تھا، اور اس نے 250 ملین وون، تقریباً 170,000 ڈالرز، اور ایک Genesis G90 جیتا، تو ایک سپر ہیومن AI کو شکست دینے کا انعام گوگل کے کروم سینڈ باکس اسکیپ کے انعام کا 170 گنا ہے۔ اس کی وضاحت: شروع میں اس نے AI کی چالوں کو نقل کیا اور ہار گیا؛ اس نے اپنی ہی طرز میں بورڈ بنا کر جیتا، جو کہ AI کے بارے میں سب سے مفید مشورہ ہے جو میں نے پورے سال سنا ہے، اور یہ ایک بورڈ گیم سے آیا ہے۔ diff میں مزید دو لائنیں۔

4:22 oxc سے Rust React Compiler اب Vite میں ایک فلیگ کے پیچھے مقامی ہے؛ ایک 1,036 فائلوں کا کوڈ بیس کمپائل مرحلے میں 14.3 سیکنڈ سے 0.81 سیکنڈ تک ہو گیا، زیادہ تر Babel کو package.json سے حذف کر کے، جو کہ میری سکن کیئر روٹین بھی ہے۔ پیکیج.json سے، جو میری سکن کیئر روٹین بھی ہے۔ اور IBM نے باب، ایک AI کوڈنگ پارٹنر لانچ کیا جو آپ کو 'Hi,' 'I'm Bob' سے خوش آمدید کہتا ہے، ذیلی ایجنٹ بناتا ہے، مین فریم کوڈ کو جدید بناتا ہے، اور 'Bobalytics' نامی ایک تجزیاتی پروڈکٹ بھیجتا ہے، تو کہیں ایک بینک بہت پرجوش ہے اور کسی نے لائسنس نہیں پڑھا۔

4:51 یہ ایک جمعہ کے لیے بہت زیادہ مارجن ہے؛ اگر آپ اسے مجھ سے سننے کے بجائے پڑھنا چاہتے ہیں، تو The Daily Diff ہر صبح آپ کے ان باکس میں آتا ہے — روزانہ کی ڈف ڈاٹ ڈیو پر مفت، لنک نیچے ہے۔ ڈیو، لنک نیچے ہے۔ تو، آج کا فیصلہ: 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