ٹیکنالوجی میڈیا Gigazine نے گزشتہ روز (3 اگست) ایک بلاگ پوسٹ شائع کی، جس میں بتایا گیا کہ AI کی مدد سے تیار کیا گیا Lean کا ایک رسمی ثبوت، جس میں کولاتز قیاس کو غلط ثابت کرنے کا دعویٰ کیا گیا تھا، بے بنیاد ثابت ہوا۔
نوٹ: کولاتز قیاس (جسے طاق و جفت معمولی قیاس / 3n+1 قیاس بھی کہا جاتا ہے) جرمن ریاضی دان لوثار کولاتز (Lothar Collatz) نے 1937 میں پیش کیا تھا۔ یہ ایک ایسا ریاضیاتی مسئلہ ہے جس کا بیان انتہائی سادہ، مگر جو آج تک حل طلب ہے۔ اس کے مطابق ہر مثبت صحیح عدد پر مخصوص قواعد کو بار بار لاگو کرنے کے بعد نتیجہ بالآخر لازماً 1 تک پہنچتا ہے۔
اس کا حسابی قاعدہ کسی بھی مثبت صحیح عدد n کے لیے یہ ہے:
اگر n جفت ہو تو اسے 2 سے تقسیم کریں (n ÷ 2)۔
اگر n طاق ہو تو اسے 3 سے ضرب دے کر 1 جمع کریں (3n + 1)۔
نیا عدد حاصل ہونے کے بعد مذکورہ بالا مراحل کو اس وقت تک دہرائیں جب تک نتیجہ 1 نہ ہو جائے۔
مثال کے طور پر عدد 6 کو دیکھیں:
6 جفت ہے، اسے 2 سے تقسیم کرنے پر 3 حاصل ہوتا ہے
3 طاق ہے، اسے 3 سے ضرب دے کر 1 جمع کرنے پر 10 حاصل ہوتا ہے
10 جفت ہے، اسے 2 سے تقسیم کرنے پر 5 حاصل ہوتا ہے
5 طاق ہے، اسے 3 سے ضرب دے کر 1 جمع کرنے پر 16 حاصل ہوتا ہے
16 کو مسلسل 2 سے تقسیم کرنے پر 8، 4، 2، 1 حاصل ہوتے ہیں
حتمی سلسلہ یہ ہے: 6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1۔
رسمی تصدیق کے ماہر Ramana Kumar نے 25 جولائی کو GitHub پر ایک منصوبہ جاری کیا، جس میں ابتدا میں دعویٰ کیا گیا کہ AI کی مدد سے کولاتز قیاس کو غلط ثابت کر دیا گیا ہے۔ منصوبے میں کسی مخصوص ضد مثال کے صحیح عدد کی نشاندہی نہیں کی گئی، بلکہ صرف Lean (قضیہ ثابت کرنے کے معاون نظام) میں یہ ثابت کیا گیا کہ “ایسا عدد موجود ہے جو 1 تک نہیں پہنچ سکتا”۔
Lean ایک قضیہ ثابت کرنے والا معاون نظام ہے، جو صارفین کو ریاضیاتی فارمولوں اور منطق کو پروگرام کی شکل میں لکھنے اور کمپیوٹر کے ذریعے ثبوت کی درستگی کی تصدیق کرنے کی سہولت دیتا ہے۔ صارف کا لکھا ہوا Lean کوڈ ریاضیاتی قضیے اور ثبوت کو قابلِ جانچ پروگرام میں تبدیل کرتا ہے، جبکہ کرنل اقسام اور منطقی مطابقت کی تصدیق کرتا ہے۔
تاہم بعد میں تردیدی مواد کا جائزہ لیتے ہوئے انہوں نے دریافت کیا کہ متعلقہ طریقہ Lean کو “False” (غلط قضیے کی نمائندگی کرنے والی قدر) کو بھی غیر مشروط طور پر قبول کرنے پر مجبور کر سکتا ہے، اس لیے موجودہ کوڈ کولاتز قیاس کی تردید نہیں کرتا۔
رسمی تصدیق کے محقق Kiran Gopinathan نے مسئلے کو ایک مختصر قابلِ تکرار کوڈ تک محدود کیا اور 28 جولائی 2026 کو Lean کی ترقیاتی ٹیم کو اس کی اطلاع دی۔
یہ خامی کرنل کے “متداخل استقرائی اقسام” کو سنبھالنے والے حصے میں موجود تھی۔ اس کے باعث بعض اوقات “غیبی نوعیتی پیرامیٹرز” (یعنی ایسے پیرامیٹرز جو ڈیٹا اسٹرکچر کے اجزا میں براہِ راست ظاہر نہیں ہوتے) نظر انداز ہو جاتے تھے، اور وہ پیرامیٹرز جنہیں اصولاً غلط قرار دیا جانا چاہیے تھا، تصدیق سے بچ نکلتے تھے۔ Lean کے ڈویلپر Leonardo de Moura نے کہا کہ مسئلہ یہ تھا کہ کرنل کے نفاذ میں مطلوبہ جانچ مکمل نہیں کی گئی تھی۔
Lean ٹیم نے رپورٹ موصول ہونے کے تقریباً 1 گھنٹے بعد اصلاحی پل درخواست بنائی اور 28 جولائی کو Lean 4.32.2 ورژن جاری کیا، جس میں یہ مسئلہ دور کر دیا گیا۔