22 ضرباں، اک وی گھٹ نئیں

مفاداں دا ٹکراؤ۔ لکھاری دسدے نیں کہ AI ایجنٹاں — Anthropic دے Claude — نے اوہناں دی ہدایت ہیٹھ کھوج والا کوڈ تے اوہ Lean ثبوت لکھے جنہاں نوں کسے انسانی جانچ کار دی لوڑ نئیں، جدکہ اوہ حصہ جیہنوں انسان نے جانچنا اے، لکھاریاں نے آپ گھڑیا۔ ایہ لیکھ وی Claude نے لکھیا اے۔

نمبراں دے دو مربع جالاں — میٹرکس — نوں سکول والے طریقے نال ضرب دین وچ n قطاراں تے n کالماں والے جالاں لئی n³ ضرباں لگدیاں نیں۔ سٹراسن نے وکھایا کہ دو 2 × 2 میٹرکس 8 دی تھاں 7 ضرباں نال ضرب دتے جا سکدے نیں۔ ایہ چال بار بار (recursively) ورتی جا سکدی اے: اک وڈے میٹرکس نوں چار بلاکاں وچ کٹو، ہر بلاک نوں اک نمبر وانگ سمجھو، تے دہراؤ۔ فیر خرچہ n³ دی تھاں n^2.807 وانگ ودھدا اے۔ مقالے مطابق، 1971 وچ ثابت ہو گیا سی کہ ایہ 2 × 2 ترکیب سب توں چنگی اے۔

ایہو خیال ہر پکے سائز لئی کم کردا اے۔ اک ترکیب جیہڑی دو 3 × 3 میٹرکس نوں r ضرباں نال ضرب دیندی اے، تے جدوں اندراجات بلاک ہون تاں وی کم کردی اے، اوہ اجیہا خرچہ دیندی اے جیہڑا n دی طاقت log₃ r وانگ ودھدا اے۔ سادہ حساب داؤ تے لگی گل دسدا اے: اجیہی ترکیب سٹراسن نوں ٹھیک اوس ویلے ہراندی اے جدوں r 21 یا گھٹ ہووے، تے 22 یا ودھ تے ہار جاندی اے۔ سب توں چنگی جانی پچھانی 3 × 3 ترکیب، لیڈرمین دی، 23 ضرباں ورتدی اے تے 1976 توں ایہدے وچ بہتری نئیں ہوئی۔

اک بوہا جیہڑا ادھ کھلا رہیا

کسے مسئلے لئی سب توں چنگے ممکن نمبر نوں اوہدا رینک (rank) آکھدے نیں۔ 3 × 3 ضرب دے رینک دیاں تھلویاں حداں ہولی ہولی ودھیاں: 2003 وچ 19، فیر مارچ 2026 وچ 20، جیہڑا وانگ نے اک ننھے جیہے نمبر نظام تے کڈھیا جیہدے وچ صرف 0 تے 1 نیں تے جتھے 1 + 1 = 0۔ ستمبر 2026 وچ، وانگ تے یانگ دی اگوائی والی اک ٹیم وکھو وکھ، اک دوجے توں دس دناں دے اندر، 21 تک اپڑے۔ پر 21 نے وی سٹراسن نالوں تیز 3 × 3 ترکیب لئی گنجائش چھڈی ہوئی سی۔

پولی ٹیکنیک مانٹریال تے کارنیگی میلن یونیورسٹی دے آئزک روڈچ، تے پولی ٹیکنیک مانٹریال دے لوئی-مارٹن روسو نے ہن ایہ حد 22 تک دھک دتی اے۔

مسئلہ 1۔ ہر الگورتھم جیہڑا دو 3 × 3 میٹرکس نوں پورے نمبراں والے مستقلاں نال ضرب دیندا اے، تے ہر سائز دے بلاکاں تے بار بار ورتیا جا سکدا اے، گھٹو گھٹ 22 ضرباں ورتدا اے۔

ایس لئی کوئی اجیہا الگورتھم تقریباً n^2.814 توں چنگا نئیں کر سکدا — تے کوئی وی سٹراسن دے 2 × 2 طریقے نوں نئیں ہرا سکدا۔

496 نکیاں بجھارتاں

ثبوت وانگ دے بنائے اک جدول تے کھڑا اے، جیہڑا اوکھے مسئلے نوں 496 سوکھیاں وچ ونڈدا اے۔ ہر اک پہلے میٹرکس تے “شرطاں” جوڑدا اے — مثال دے طور تے، کہ اوہدے کجھ اندراجات جوڑ کے صفر بن جان۔ جنیاں ودھ شرطاں، مسئلہ اونا سوکھا، ایتھوں تک کہ اوہ معمولی حالت آ جاندی اے جتھے میٹرکس سارا صفر ہوندا اے۔

لکھاریاں نے پہلاں اک پکا کھوج والا پروگرام بنایا جیہنے اوہناں نوں ہر بجھارت دا اصلی جواب، اوہنوں ثابت کرن دی کوشش توں پہلاں دس دتا۔ ایہ جواب اک نقشے دا کم کردے رہے: ایہناں نے دسیا کہ کیہڑیاں تھلویاں حداں پچھا کرن دے قابل نیں۔ آخر وچ، اوہناں دا ثبوت ساریاں 496 بجھارتاں دی حد بنھدا اے، ایہناں وچوں 359 نوں پکے طور تے حل کردا اے — وانگ دے تازہ نتیجیاں وچ 195 دے مقابلے — تے 252 لئی تھلویں حد اچی کردا اے۔ اوہناں دا اپنا اک “جوڑن” (gluing) والا مسئلہ دو سوکھیاں بجھارتاں دیاں ترکیباں نوں رلا کے تیجی لئی ترکیب بناندا اے، تے ایہنے 145 اتلیاں حداں دتیاں۔

آخری بیان وچ دو شرطاں اہم نیں۔ پورے نمبراں والے مستقل: پورے نمبراں والے مستقلاں دی ترکیب، 0 تے 1 والے نمبر نظام وچ پڑھی جاوے تاں وی، ودھ ضرباں توں بغیر اک درست ترکیب رہندی اے، ایس لئی حد اوتھے وی لاگو ہو جاندی اے۔ بلاک: ایس شرط توں بغیر سوکھے راہ موجود نیں۔ مقالے وچ حوالہ دتا گیا روزوسکی دا 3 × 3 الگورتھم صرف 21 ضرباں منگدا اے، پر ایہ نمبراں دے ادل بدل (commuting) تے ٹکیا اے تے بار بار نئیں ورتیا جا سکدا۔

مشین دا پرکھیا ثبوت

ثبوت Lean وچ لکھیا گیا اے، اک پروگرامنگ زبان جیہدے وچ کوئی مسئلہ صرف اوس ویلے کمپائل ہوندا اے جدوں ہر قدم دی تصدیق ہو جاوے۔ پورا ثبوت 3,521 ماڈیولاں وچ ونڈیاں تقریباً دس لکھ سطراں دا اے، تے اک پروسیسر کور تے ایہنوں پرکھن وچ 11.1 گھنٹے لگدے نیں۔ کسے نوں سارا پڑھن دی لوڑ نئیں۔ اک جانچ کار تقریباً 1,000 سطراں دی اک لائبریری پڑھدا اے، جیہڑی لکھاریاں نے کسے وی ثبوت دے ہون توں پہلاں لکھی سی، جیہڑی دسدی اے کہ ضرب دی ترکیب کیہ ہوندی اے تے مسئلہ بیان کردی اے؛ باقی Lean دا کرنل پرکھدا اے، تے اک آزاد جانچ کار نتیجے نوں مڑ چلا سکدا اے۔

لکھاری ایہ وی دسدے نیں کہ AI ایجنٹاں نے لکھتاں دی کھوج کیتی: اوہناں نے پرکھیا کہ ہر حوالہ موجود اے، “پر ایہ نئیں کہ ہر اک وچ ٹھیک اوہی خیال اے جیہدا سہرا اسیں اوہنوں دیندے آں۔”

آخری خلا

اک سوال باقی اے: کیہ 22 ضرباں والی کوئی 3 × 3 ترکیب موجود اے، یا لیڈرمین دیاں 23 ای اصلی گھٹ توں گھٹ نیں؟ لکھاریاں نوں امید اے کہ ایہ خلا “چھیتی ای بند ہو جاوے گا”، تے اوہ اپنا کھوج والا کوڈ اوس ویلے جاری کرن گے جدوں ایہ بند ہو جاوے، یا جدوں مقالہ چھپن لئی منظور ہو جاوے۔ ایہ حد غیر پورے نمبراں والے مستقلاں والیاں ترکیباں نوں وی پاسے چھڈدی اے۔