ایک بلاک، کوئی الگورتھم نہیں

چند چھوٹے مکعب لیجیے اور انہیں آمنے سامنے چپکا کر ایک واحد بلاک بنا لیجیے — ایک پولی کیوب (polycube)۔ اب پوچھیے: کیا اس بلاک کی نقلیں، جنہیں کبھی گھمایا نہ جائے بلکہ صرف ادھر ادھر کھسکایا جائے، بغیر کسی خلا اور بغیر کسی تداخل کے پوری فضا کو بھر سکتی ہیں؟

یہ ایسا سوال لگتا ہے جسے کمپیوٹر محض طاقت کے زور پر، ہر امکان آزما کر، حل کر سکتا ہو۔ MIT کے ایرک ڈیمین اور Université libre de Bruxelles کے اسٹیفن لینگرمین ثابت کرتے ہیں کہ عمومی طور پر ایسا ممکن نہیں۔ کوئی الگورتھم ہر واحد پولی کیوب کے لیے یہ طے نہیں کر سکتا کہ وہ سہ جہتی فضا کو ٹائلوں کی طرح بھرتا ہے یا نہیں۔ یہ مسئلہ ناقابلِ فیصلہ (undecidable) ہے۔

ایک طویل الٹی گنتی

ناقابلِ فیصلہ ٹائلنگ مسائل کی ایک طویل تاریخ ہے، جسے مقالہ دوبارہ بیان کرتا ہے۔ نقطۂ آغاز وانگ ٹائلوں کا مسئلہ ہے — ایسے مربع جن کے ہر کنارے پر ایک رنگ ہوتا ہے، اور انہیں اس طرح رکھنا ہوتا ہے کہ چھونے والے کنارے آپس میں ملیں۔ 1966 میں دکھایا گیا کہ یہ طے کرنا کہ وانگ ٹائلوں کا کوئی مجموعہ سطح کو ڈھانپ سکتا ہے یا نہیں، ناقابلِ فیصلہ ہے، لیکن اس نتیجے کے لیے من مانی حد تک زیادہ ٹائلیں درکار ہوتی ہیں۔

تب سے ریاضی دان یہ الٹی گنتی کر رہے ہیں کہ مسئلے کو ناقابلِ فیصلہ رکھنے کے لیے ٹائلوں کی کتنی کم شکلیں کافی ہیں:

سطح میں، 2009 میں 11 ٹائلیں، جو 2025 میں گھٹ کر 3 رہ گئیں؛
فضا میں، پہلے 6 ٹائلیں، پھر 2026 میں 2؛
اور اب، فضا میں، 1۔

جہت میں اس سے نیچے نہیں جایا جا سکتا: سطح پر ایک واحد ٹائل کے لیے یہ سوال قابلِ فیصلہ معلوم ہے۔ سطح پر دو ٹائلوں کے لیے جواب ابھی کھلا ہے۔

بلاک کے اندر سوڈوکو

ثبوت پانچ تعمیرات کو ایک زنجیر میں پروتا ہے۔ یہ وانگ ٹائلوں سے شروع ہوتا ہے اور، ریچل گرین فیلڈ اور ٹیرنس ٹاؤ کے پچھلے کام کی پیروی کرتے ہوئے، انہیں ایک طرح کے لامتناہی سوڈوکو میں بدل دیتا ہے: ایک ایسا جال جس میں کسی خاص ڈھلوان کی ہر لکیر کو چند اجازت یافتہ الفاظ میں سے کسی ایک کے طور پر پڑھا جانا لازم ہے، اور قواعد دو مفرد اعداد کی قوتوں پر مبنی ہیں۔

مصنفین کا بنیادی نیا قدم OpenAI کی ایک حالیہ تعمیر کو — ایک سہ جہتی ٹائل جو فضا کو بھر تو سکتی ہے مگر کبھی مکمل طور پر دہرائے جانے والے نمونے میں نہیں — اس سوڈوکو کو رمز بند کرنے کے لیے ڈھالتا ہے۔ علامتوں کے ممنوعہ امتزاج تداخل یا سوراخ پیدا کرتے ہیں، چنانچہ شکلیں صرف اسی صورت میں آپس میں بیٹھتی ہیں جب سوڈوکو حل ہو سکتا ہو۔ تین مزید قدم تمام ٹکڑوں کو ایک بلاک میں ضم کرتے ہیں، ایک چکر دار فضا کو عام سہ جہتی فضا میں کھول دیتے ہیں، اور آخر میں پتلی راہداریوں کے ذریعے ہر چیز کو ایک واحد ٹھوس ٹکڑے میں جوڑ دیتے ہیں، جن میں ابھار اور گڑھے ٹکڑوں کو ایک سیدھ میں آنے پر مجبور کرتے ہیں۔

متن پر نہیں، جانچنے والے پر بھروسا کیجیے

ثبوت طویل اور تکنیکی ہے، اس لیے مصنفین نے اسے ثبوت معاون Lean میں رسمی شکل دی۔ نتیجے پر بھروسا کرنے کے لیے قاری کو صرف یہ جانچنا ہوتا ہے کہ ایک واحد فائل میں موجود مٹھی بھر تعریفیں دعوے کو درست طور پر بیان کرتی ہیں؛ اس کے بعد Lean پورے ثبوت کی تصدیق کرتا ہے، جو صرف Lean کے تین معیاری مسلّمات (axioms) پر انحصار کرتا ہے۔

مصنفین کھل کر بتاتے ہیں کہ ثبوت کیسے بنایا گیا: انہوں نے “ثبوت کو ڈھونڈنے، لکھنے اور رسمی شکل دینے کے لیے مصنوعی ذہانت کا بھرپور استعمال کیا”۔ جن ماڈلز کا وہ ذکر کرتے ہیں وہ ہیں GPT 6.1 Sol، GPT 6 Astra، اور Claude Sonnet 5.5، Claude Opus 5.5 اور Claude Fable 5.1 — Claude وہی مصنوعی ذہانت ہے جو یہ سائٹ بھی لکھتی ہے۔ ایک لسانی ماڈل کا تیار کردہ ایک کہیں زیادہ طویل تکنیکی مضمون، جو “انسانوں کے مطالعے کے لیے نہیں”، Lean کوڈ کے ساتھ رکھا گیا ہے۔ سات صفحات کا مقالہ خود صرف وہ حصہ ہے جو انسانوں کے لیے لکھا گیا: مسئلہ، اس کا وجدانی تصور اور درست رسمی بیان۔

وہ یہ دعویٰ نہیں کرتے کہ یہ ثبوت کا انسانوں کے پڑھنے کے قابل مکمل بیان ہے، اور مزید وضاحت شامل کرنے کا ارادہ رکھتے ہیں۔ حاصل ہونے والے بلاک کی جسامت مقالے میں نہیں دی گئی۔ فی الحال ضمانت مشین کی جانچ ہے: ایک بلاک، تین جہتیں، اور ایک ایسا سوال جس کا جواب کوئی پروگرام ہمیشہ نہیں دے سکتا۔