Claude نے Fermat کا ثبوت 11 دن میں جانچا، مگر نئی ریاضی ایجاد نہیں کی
Anthropic نے 4 ستمبر 2026 کو Fermat’s Last Theorem کی مکمل computer-checked formalization جاری کی۔ Anthropic کی تحقیقی تفصیل کے مطابق Claude نے بڑی حد تک خودکار طور پر 11 دن میں تقریباً 13 ملین سطریں Lean code لکھیں، مجموعی طور پر 30,300 درمیانی قضیے ثابت کیے اور ان میں سے لگ بھگ 29,500 آخری proof میں استعمال ہوئے۔
4 ستمبر کی اس پیش رفت کا مطلب یہ نہیں کہ Claude نے Fermat کا مسئلہ پہلی بار حل کیا یا Andrew Wiles کے کام سے الگ کوئی نیا ریاضیاتی استدلال دریافت کیا۔ TechTimes کی آزاد رپورٹ بھی اسے Wiles کے موجودہ استدلال کی machine-checkable encoding قرار دیتی ہے: Claude نے رسمی proof تیار کیا، جبکہ Lean اور اضافی checkers نے اس کی منطقی ساخت جانچی۔
Claude، انسانی ثبوت اور Lean کے کردار الگ ہیں
Fermat’s Last Theorem کہتا ہے کہ مثبت صحیح اعداد a، b اور c کے لیے aⁿ + bⁿ = cⁿ ممکن نہیں جب n دو سے بڑا ہو۔ اس theorem کا قبول شدہ انسانی ثبوت Wiles اور Richard Taylor کے کام سے پہلے ہی قائم تھا؛ نئی پیش رفت اسے ایسی رسمی زبان میں منتقل کرنا ہے جس میں ہر تعریف، مفروضہ اور منطقی نتیجہ کمپیوٹر کے سامنے واضح ہو۔
انسانی تحقیقی تحریر اکثر وہ مراحل مختصر کر دیتی ہے جنہیں ماہر قاری خود پُر کر سکتا ہے۔ Lean ایسی رعایت نہیں دیتا: ہر lemma کو پہلے سے موجود تعریف یا ثابت شدہ نتیجے سے جوڑنا پڑتا ہے۔ Claude agents نے اسی وسیع formalization کو انجام دیا، یعنی امیدوار proof terms، تعریفیں اور درمیانی قضیے تحریر کیے۔
Lean کا kernel دوسری سطح پر کام کرتا ہے۔ وہ ریاضیاتی خیال تجویز نہیں کرتا بلکہ یہ دیکھتا ہے کہ پیش کیا گیا formal term اپنے اعلان کردہ statement کی درست شہادت ہے یا نہیں۔ یوں خبر میں لفظ ”جانچا“ پوری Claude–Lean pipeline کا مختصر بیان ہے؛ فنی طور پر code Claude نے بنایا اور منطقی قبولیت Lean نے طے کی۔
FinalCheck اور comparator نے کس چیز کی توثیق کی
جاری کردہ GitHub artifact کے verification notes کے مطابق FinalCheck آخری theorem کو صرف Lean کے تین معیاری axioms—propext، Classical.choice اور Quot.sound—تک محدود کرتا ہے اور ”sorry“، اضافی axiom یا native_decide جیسے نامکمل یا متبادل راستے قبول نہیں کرتا؛ شروع سے build میں 60,475 modules کو Lean kernel نے check کیا، comparator نے ثابت شدہ statement اور اس کی constants کو Mathlib challenge سے ملایا، اور Rust میں لکھے آزاد nanoda kernel نے 1,052,234 declarations بلا خطا قبول کیں۔
ان checks کے کام مختلف ہیں۔ FinalCheck پوشیدہ یا غیر منظور شدہ مفروضوں کا راستہ بند کرتا ہے، comparator یہ روکتا ہے کہ کمزور یا بدلا ہوا statement ثابت کرکے اسے Fermat’s Last Theorem کہا جائے، اور دوسرے kernel سے replay ایک ہی implementation پر انحصار کم کرتا ہے۔ یہ مجموعہ اس دعوے کو مضبوط کرتا ہے کہ repository میں درج آخری formal statement واقعی متعین axioms سے اخذ ہوتا ہے۔
اس ضمانت کی حد بھی واضح ہے۔ Kernel statements اور proof terms کے باہمی تعلق کو جانچتا ہے، مگر یہ نہیں بتا سکتا کہ ہر machine-generated theorem کا نام اس کے انسانی mathematical meaning کی درست ترجمانی کرتا ہے۔ آخری FLT statement کے لیے comparator اہم حفاظت دیتا ہے؛ ہزاروں اندرونی نتائج کی معنوی افادیت اور توضیح پھر بھی انسانی مطالعے کا موضوع ہیں۔
لاکھوں سطریں نئی ایجاد نہیں، formalization کا پیمانہ ہیں
بڑی codebase کو نئی ریاضی کی مقدار سمجھنا درست نہیں۔ Formal proof میں انسانی exposition کے چھوڑے ہوئے مراحل، بنیادی تعریفیں، type conversions اور dependency links بھی صراحت سے لکھنے پڑتے ہیں؛ اسی لیے machine-generated formalization بہت طویل ہو سکتی ہے، چاہے اس کا مرکزی استدلال پہلے سے معلوم ہو۔
یہ کام خالی زمین پر شروع نہیں ہوا۔ اس نے Mathlib کی formal mathematics، Imperial College London کے Kevin Buzzard کی قیادت میں جاری FLT project، flt-regular project اور Darmon، Diamond اور Taylor کی Wiles-based تشریح سے فائدہ اٹھایا۔ Lean اور Mathlib خود سینکڑوں contributors کی برسوں کی محنت کا نتیجہ ہیں، اس لیے صرف Claude کو پورے علمی سلسلے کا مصنف کہنا انسانی اور open-source بنیاد کو غائب کر دے گا۔
Prove2Me نے agents کے درمیان theorem dependencies، مشترک project state، search اور کام کی تقسیم سنبھالی، جبکہ Anthropic کے محقق Tianyi Peng نے کبھی کبھار اعلیٰ سطح کی سمت دی۔ اس بنا پر 11 روزہ مدت کسی تنہا chatbot session کی نہیں بلکہ Claude agents، orchestration software، انسانی proof literature، موجودہ Lean libraries اور verification tools کی مشترک pipeline کی کارکردگی ہے۔
نتیجہ مکمل ہے، مگر اس کی نوعیت محدود ہے
جاری artifact میں Fermat’s Last Theorem کا end-to-end Lean proof موجود ہے، آخری statement کو Mathlib کے بیان سے ملایا گیا ہے اور proof environment دوسرے kernel سے بھی replay ہوا ہے۔ Repository اسے research artifact کہتی ہے: اسے برقرار رکھنے یا بیرونی contributions قبول کرنے کا وعدہ نہیں کیا گیا، اس لیے ”مکمل“ سے مراد theorem کی موجودہ machine-checked formalization ہے، مستقل community library کا درجہ نہیں۔
اس پیش رفت کی اصل اہمیت discovery کے بجائے رفتار اور scale ہے۔ ایک نہایت پیچیدہ، پہلے سے قائم انسانی argument کو ایسی صورت میں منتقل کیا گیا جس کی منطقی زنجیر software دوبارہ check کر سکتا ہے۔ جو بات ثابت نہیں ہوئی وہ یہ ہے کہ Claude نے Wiles کے متبادل کوئی نیا بنیادی خیال دیا، یا یہ کہ اتنی بڑی auto-generated codebase انسانی مطالعے، اختصار اور دوبارہ استعمال کے لیے پہلے ہی موزوں ہے۔
اب دستیاب شواہد ایک محتاط نتیجہ دیتے ہیں: theorem نیا نہیں، formal artifact نیا ہے؛ mathematical route انسانی ہے، اس کی وسیع encoding Claude نے تیار کی، اور formal correctness Lean-based checks نے آزمائی۔ آئندہ جائزے کا اہم سوال proof کے درست ہونے سے آگے اس کی معنوی ساخت، attribution اور قابلِ استعمال ہونے کا ہوگا۔
یہ بھی پڑھیں:
ہمارا نیوز لیٹر سبسکرائب کریں
ویب 3، AI اور کرپٹو کی تازہ خبریں براہ راست اپنے اِن باکس میں پائیں۔