کمپیوٹر سے حل ہونے والے مسائل: ریاضی کے مشہور مسائل جنہیں حل کرنے میں مشینوں نے مدد کی (1976–2026)

1976 میں الینوائے کے دو ریاضی دانوں نے اعلان کیا کہ انہوں نے ثابت کر دیا ہے کہ کسی بھی نقشے کو رنگنے کے لیے چار رنگ کافی ہیں، اور ان کے ثبوت کا ایک حصہ صرف کمپیوٹر ہی جانچ سکتا تھا۔ بہت سے ریاضی دان بے چین ہو گئے: اگر کوئی انسان اسے پورا پڑھ ہی نہیں سکتا تو کیا یہ واقعی ثبوت ہے؟ پچاس سال بعد سوال الٹ گیا ہے۔ 2026 میں AI نظاموں نے ان نتائج کے کلیدی خیالات ڈھونڈ لیے جو ماہرین دہائیوں تک نہیں ڈھونڈ سکے تھے۔ یہ مضمون یہ کہانی ترتیب سے سناتا ہے اور ہر مشہور مسئلے کے لیے ٹھیک ٹھیک بتاتا ہے کہ مشین نے کیا کیا، کیونکہ “کمپیوٹر سے حل ہوا” کے معنی بہت مختلف ہو سکتے ہیں۔

1976: چار رنگ، اور ایک ایسا ثبوت جسے کوئی پڑھ نہیں سکتا تھا

GCSE بنیادی

سوال اتنا آسان ہے کہ پرائمری اسکول کا بچہ بھی سمجھ لے: نقشے کو ایسے رنگیں کہ پڑوسی ملکوں کا رنگ کبھی ایک نہ ہو۔ کتنے رنگوں کی ضرورت پڑ سکتی ہے؟ فرانسس گتھری نے 1852 میں اندازہ لگایا: چار۔ یہ دیکھنا آسان ہے کہ چار کی ضرورت پڑ سکتی ہے (نیچے کی تصویر دیکھیں)، مگر یہ ثابت کرنا کہ ہر ممکن نقشے کے لیے چار رنگ ہمیشہ کافی ہیں، ریاضی دانوں سے 124 سال تک نہ ہو سکا۔

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

شک کیسے دور ہوا: 1996 میں ایک مختصر کمپیوٹر ثبوت آیا، اور 2005 میں ژورژ گونتیئے اور بنجامن ورنر نے پوری دلیل کو ثبوت معاون Coq میں تصدیق کیا۔ آج یہ ریاضی کے سب سے گہرائی سے تصدیق شدہ مسائل میں سے ایک ہے۔

1996: پہلا ثبوت جو کمپیوٹر نے خود ڈھونڈا

انڈر گریجویٹ توسیع

رابنز قیاس یہ پوچھتا تھا کہ کیا تین مختصر قواعد ٹھیک وہی الجبرا بیان کرتے ہیں جو بولین الجبرا بیان کرتا ہے، یعنی ہر کمپیوٹر چپ کے اندر کی سچ/جھوٹ منطق۔ الفریڈ تارسکی سمیت چوٹی کے منطق دان ساٹھ سال تک اسے حل نہیں کر سکے تھے۔ 1996 میں ولیم میک کیون کے خودکار ثبوت ساز EQP نے تقریباً آٹھ دن تک ممکنہ استدلالی سلسلے کھنگالے اور ایک ثبوت ڈھونڈ لیا۔ یہ 1976 سے مختلف نوعیت کی بات تھی: کسی نے کمپیوٹر کو نہیں بتایا تھا کہ دلیل کیسی ہونی چاہیے۔

1998–2014: کیپلر کے مالٹے

1611 میں یوہانس کیپلر نے دعویٰ کیا کہ پھل فروش جس طرح مالٹے سجاتے ہیں (ہر تہہ نیچے والی تہہ کے گڑھوں میں)، وہی برابر کُروں کو سب سے گھنا بھرنے کا طریقہ ہے۔ یہ تقریباً 74% جگہ بھر دیتا ہے (ٹھیک ٹھیک ⁦π/√18⁩)۔

تھامس ہیلز نے سیموئل فرگوسن کے ساتھ اس سوال کو ہزاروں بہتری (آپٹیمائزیشن) کے مسائل میں بدلا، انہیں کمپیوٹر سے حل کیا اور 1998 میں ثبوت کا اعلان کیا۔ جریدے کے مبصرین نے کہا کہ وہ “99% پُریقین” ہیں کہ یہ درست ہے، مگر ہر حساب نہیں جانچ سکتے۔ جواب میں ہیلز نے Flyspeck منصوبہ چلایا تاکہ سب کچھ ثبوت معاون سافٹ ویئر میں دوبارہ تصدیق ہو؛ یہ 2014 میں مکمل ہوا۔

2016: 200 ٹیرابائٹ کا ثبوت

GCSE بنیادی

یہ ایک پہیلی ہے جسے آپ خود آزما سکتے ہیں۔ ہر مکمل عدد کو سرخ یا نیلا رنگیں۔ کیا آپ ایسا کر سکتے ہیں کہ کوئی بھی فیثاغورثی تثلیث (تین اعداد جن میں ⁦a² + b² = c²⁩، جیسے 3، 4، 5) ایک ہی رنگ کی نہ ہو؟

رونالڈ گراہم نے جواب کے لیے 100 ڈالر کا انعام رکھا تھا۔ 2016 میں مارین ہیولے، اولیور کلمان اور وکٹر ماریک نے سپر کمپیوٹر Stampede پر تقریباً دو دن ایک SAT سالور (بہت بڑی سچ/جھوٹ منطقی پہیلیاں حل کرنے والا سافٹ ویئر) چلایا۔ جواب: 1 سے 7,824 تک ہر عدد محفوظ طریقے سے رنگا جا سکتا ہے، مگر 1 سے 7,825 تک نہیں۔ اس بات کا ثبوت کہ 7,825 اعداد کی کوئی بھی رنگائی کام نہیں کرتی، 200 ٹیرابائٹ کا تھا، جسے اُس وقت Nature نے اب تک کا سب سے بڑا ریاضیاتی ثبوت قرار دیا۔ اسی تکنیک نے 2019 میں سات جہتوں میں مکعبوں سے خلا کو ڈھانپنے والے کیلر قیاس کا فیصلہ کیا۔

2025–2026: AI خیالات ڈھونڈنے لگا

پوسٹ گریجویٹ توسیع

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

اکائی فاصلے کا قیاس (مئی 2026)۔ 1946 میں پال ایردوش نے پوچھا: اگر آپ ایک ہموار سطح پر n نقطے رکھیں تو کتنے جوڑے ٹھیک 1 اکائی کے فاصلے پر ہو سکتے ہیں؟ ان کا خیال تھا کہ جواب n سے بس ذرا سا تیز بڑھتا ہے۔ OpenAI کے ایک اندرونی ماڈل نے الجبری نظریۂ اعداد کے گہرے اوزاروں سے نقطوں کے مجموعوں کا ایک لامحدود خاندان ڈھونڈا جو اس حد کو n کی ایک حقیقی قوت سے پار کر جاتا ہے۔ فیلڈز میڈل یافتگان ٹموتھی گاورز اور جیکب تسیمرمین سمیت نو چوٹی کے ریاضی دانوں نے اسے جانچا اور ایک ساتھی مقالہ لکھا، اور ول ساوِن نے اس اضافے کو واضح شکل دی۔ گل کلائی نے اس کی اہمیت کا موازنہ 1976 کے چار رنگوں کے ثبوت سے کیا۔

AlphaProof Nexus (مئی 2026)۔ Google DeepMind نے اپنے ایجنٹ کو، جو Gemini ماڈل کو Lean کے ساتھ جوڑتا ہے، ایردوش مسائل کے ڈیٹا بیس کے 353 کھلے مسائل پر لگایا۔ اس نے 9 حل کیے، جن میں دو 56 سال سے کھلے تھے، اور عددی سلسلوں کے آن لائن انسائیکلوپیڈیا ⁦(OEIS)⁩ کے 44 قیاس ثابت کیے۔ ہر ثبوت Lean میں کمپائل ہوتا ہے۔ مگر کامیابی کی شرح پر غور کریں: تقریباً 2.5%۔

Astra (اگست 2026)۔ OpenAI نے اپنے اگلے، غیر جاری شدہ ماڈل کے دس نتائج کا اعلان کیا، جن میں غیر سوفک گروہ کی پہلی تعمیر (میخائل گروموف کے 1999 میں اٹھائے گئے سوال کا جواب)، ایردوش کے تین مسائل، اور 1978 کے بعد پہلی بار کُروں کو بھرنے کی ایک عمومی حد میں بہتری شامل تھی۔ ہر نتیجے کے ساتھ Lean کی سند تھی۔ ایک آزاد انسانی آڈٹ کو مرکزی نتائج میں کوئی تصدیق شدہ بڑی غلطی نہیں ملی، اگرچہ ایک نتیجے پر ایک ماہر نے بڑی نظرثانی کی درخواست کی، اور لکھتے وقت تک جریدوں کا ہم مرتبہ جائزہ مکمل نہیں ہوا تھا۔

پچاس سال، ایک ٹائم لائن میں

اگر آپ ریاضی سیکھ رہے ہیں تو اس کا کیا مطلب ہے

اس مضمون کا ہر نتیجہ پھر بھی انسانوں پر منحصر تھا: کسی کو مسئلہ درست طور پر بیان کرنا تھا، طے کرنا تھا کہ کون سا طریقہ آزمانے کے قابل ہے، جانچنا تھا کہ کمپیوٹر نے جو مسئلہ ثابت کیا وہی اصل میں اہم ہے، اور سمجھانا تھا کہ وہ سچ کیوں ہے۔ ٹھیک یہی مہارت اسکول کی ریاضی تب بناتی ہے جب وہ آپ سے حل کے مراحل دکھانے کو کہتی ہے، اور یہی ہمارے مضمون کیا AI واقعی ریاضی کر سکتا ہے؟ کا موضوع ہے۔ ابھی کھلے مسائل کے لیے، اور ان حل شدہ مسائل کی کارڈ بہ کارڈ فہرست کے لیے، ہمارا حل نہ ہونے والی ریاضیاتی پہیلیوں کا مرکز دیکھیں۔