فرما کا آخری مسئلہ کہتا ہے کہ جب n، 2 سے بڑا ہو تو xⁿ + yⁿ = zⁿ کا مثبت صحیح اعداد میں کوئی حل نہیں۔ پیئر دو فرما نے 1630 کی دہائی میں اسے کتاب کے حاشیے پر لکھا؛ اینڈریو وائلز نے 1990 کی دہائی میں اب تک لکھی گئی مشکل ترین ریاضی سے اسے ثابت کیا۔ 4 ستمبر 2026 کو Anthropic نے اعلان کیا کہ Claude نے 11 دنوں میں اس ثبوت کا پہلا مکمل کمپیوٹر سے جانچا گیا نسخہ تیار کیا[1]۔ یہ مضمون بتاتا ہے کہ اس کا کیا مطلب ہے، یہ ریاضی جتنی ہی کمپیوٹر سائنس کی کہانی کیوں ہے، اور اس کا کیا مطلب نہیں ہے۔
ٹائم لائن
- 1630 کی دہائیفرما ایسے ثبوت کا دعویٰ کرتے ہیں جس کے لیے "یہ حاشیہ بہت تنگ ہے"۔
- 1994–95اینڈریو وائلز (رچرڈ ٹیلر کے ساتھ) ثبوت مکمل کرتے ہیں۔
- 2024کیون بزرڈ امپیریل کالج لندن میں ثبوت کو Lean میں باضابطہ شکل دینے کا انسانی قیادت والا منصوبہ شروع کرتے ہیں۔
- اگست 2026Claude ایجنٹس 11 دنوں میں Lean میں مکمل باضابطگی مکمل کرتے ہیں۔
- 4 ستمبر 2026Anthropic نتیجے کا اعلان کرتا ہے؛ بزرڈ جائزہ لیتے ہیں۔
پروف اسسٹنٹ کیا کرتا ہے
GCSE بنیادی
انسان کا لکھا ثبوت چھوٹے قدم قاری پر چھوڑ دیتا ہے۔ ماہر جائزہ کار بھی کوئی خلا نظرانداز کر سکتے ہیں۔ Lean جیسا پروف اسسٹنٹ یہ خطرہ ختم کرتا ہے۔ آپ تعریفیں اور ثبوت کوڈ کی صورت لکھتے ہیں، اور ایک چھوٹا، قابلِ اعتماد جانچنے والا (کرنل) تصدیق کرتا ہے کہ ہر قدم منطق اور پچھلے نتائج سے نکلتا ہے۔ اگر کوڈ کمپائل ہو جائے تو مسئلہ تصدیق شدہ ہے۔ یہ ایسے کمپائلر کی طرح ہے جو آپ کا پروگرام تب تک نہیں چلاتا جب تک وہ ثابت شدہ طور پر درست نہ ہو۔
باضابطہ ثبوت ایک درخت ہے: آخری مسئلہ بڑے درمیانی نتائج پر ٹکا ہے، وہ لیما پر، اور لیما تعریفوں اور بنیادی حقائق پر۔ Lean ہر کڑی جانچتا ہے۔ بنیاد سے شروع کر کے درخت جانچنے کے لیے بٹن دبائیں۔ اسکیمی خاکہ؛ اصل درخت میں تقریباً 29,500 مسائل ہیں۔
Claude نے اصل میں کیا کیا
A-Level توسیع
- اس نے وائلز کے ثبوت کے ایک سادہ نسخے کو باضابطہ شکل دی، جو ڈارمن، ڈائمنڈ اور ٹیلر کا ہے[1]۔
- نتیجے میں تقریباً 1.3 کروڑ لائنیں Lean اور تقریباً 30,300 مسائل ہیں (آخری ثبوت میں تقریباً 29,500 استعمال ہوئے)، جو Mathlib سے پانچ گنا سے بھی بڑا ہے[1]۔
- درجنوں Claude ایجنٹس نے 11 دن متوازی کام کیا، ایک اندرونی تحقیقی ماڈل کے تقریباً چھ ارب آؤٹ پٹ ٹوکن استعمال کر کے[1]۔
- انسانی ریاضیاتی حصہ Anthropic کے محقق تیانی پینگ کی کبھی کبھار کی اعلیٰ سطحی ہدایات تک محدود رہا[1]۔
- ثبوت صرف Lean کے تین معیاری مسلّمات پر ٹکا ہے، اور ایک موازنہ کار نے تصدیق کی کہ آخری مسئلہ بالکل وہی کہتا ہے جو Mathlib کا اپنا فرما کے آخری مسئلے کا بیان کہتا ہے[1]۔
- اس نے امپیریل کالج لندن میں کیون بزرڈ کے FLT منصوبے کے حصے دوبارہ استعمال کیے، اور بزرڈ نے مکمل ثبوت کا جائزہ لیا[1]۔
فوری جانچ
Lean میں ثبوت کے "کمپائل" ہونے کا کیا مطلب ہے؟
بیان جانچنا کیوں ضروری ہے
کمپیوٹر سے جانچا گیا ثبوت تبھی مفید ہے جب وہ درست بیان ثابت کرے۔ اگر Lean میں مسئلہ ذرا غلط لکھا ہوتا تو غلط بات کا مکمل ثبوت بے کار ہوتا۔ اسی لیے ٹیم نے موازنہ کار سے تصدیق کی کہ بیان Mathlib کے آزادانہ لکھے نسخے سے ملتا ہے، اور اسی لیے "کوئی اضافی مسلّمہ نہیں" والی جانچ اہم ہے: یہ دکھاتی ہے کہ کچھ بھی محض فرض نہیں کیا گیا[1]۔ قدموں کی تصدیق اور تفصیل کی توثیق دو الگ کام ہیں، بالکل سافٹ ویئر ٹیسٹنگ کی طرح۔
وہ فرق جسے طلبہ اکثر گڈمڈ کر دیتے ہیں
درست کا مطلب خوش نما (یا نیا) نہیں۔
امتحان طرز کا سوال
فرما کے آخری مسئلے کے باضابطہ ثبوت کو مثال بنا کر تصدیق (verification) اور توثیق (validation) کا فرق سمجھائیں۔ [4 نمبر]
نمونہ جواب اور نمبروں کی تقسیم دکھائیں
- تصدیق جانچتی ہے کہ پروڈکٹ درست طریقے سے بنی ہے، یعنی اپنی تفصیل پر پورا اترتی ہے (1 نمبر)
- یہاں Lean تصدیق کرتا ہے کہ ثبوت کا ہر قدم منطقی طور پر درست ہے (1 نمبر)
- توثیق جانچتی ہے کہ درست پروڈکٹ بنائی گئی ہے، یعنی تفصیل واقعی ضروری چیز سے ملتی ہے (1 نمبر)
- یہاں Lean بیان کا Mathlib کے آزاد FLT بیان سے موازنہ جانچتا ہے کہ ثبوت مطلوبہ مسئلہ ہی ثابت کرتا ہے (1 نمبر)
ممتحن کس بات پر توجہ دیتا ہے: دونوں اصطلاحات کی تعریف کریں اور ہر ایک کو مثال کے کسی خاص حصے سے جوڑیں۔
عام غلطی: دونوں الفاظ کو مترادف سمجھنا۔ کوئی پروگرام ہر تصدیقی جانچ پاس کر کے بھی غلط کام کر سکتا ہے۔
منطق، ثبوت اور ٹیسٹنگ A-Level ریاضی اور کمپیوٹر سائنس کو جوڑتے ہیں۔ ہمارا مضمون کیا AI واقعی ریاضی کر سکتا ہے؟ بڑی تصویر دکھاتا ہے، اور ملینیم انعامی مسائل بتاتے ہیں کہ کون سے سوال اب بھی کھلے ہیں۔
ماخذ اور مزید مطالعہ کے لیے
- Anthropic: Formalizing Fermat's Last Theorem (4 Sep 2026) — پیمانہ، ایجنٹس، مسلّمات، انسانی حصہ، بزرڈ کا جائزہ، احتیاطیں
- AI Weekly: Claude formalized Fermat's Last Theorem in 11 days — خبری کوریج
- Lean community: Mathlib — Lean کی ریاضی لائبریری
- Imperial College London: Fermat's Last Theorem formalisation project (Kevin Buzzard) — انسانی قیادت والا منصوبہ
آخری جائزہ: 5 اکتوبر 2026۔ اعداد عمومی طور پر شائع شدہ عام قدریں ہیں، اور قواعد تبدیل ہو سکتے ہیں۔ امتحان کی زبان ہر اسپیسیفیکیشن کے مطابق مختلف ہو سکتی ہے، اس لیے اپنا اسپیسیفیکیشن ضرور دیکھیں۔
عمومی سوالات
کیا AI نے فرما کا آخری مسئلہ ثابت کیا؟
نہیں: اسے 1990 کی دہائی میں اینڈریو وائلز نے ثابت کیا۔ 2026 میں یہ ہوا کہ Claude ایجنٹس نے اس ثبوت کے ایک نسخے کو Lean میں ترجمہ کیا، ایک پروگرامنگ زبان جس کا جانچنے والا ہر منطقی قدم کی تصدیق کرتا ہے۔ 4 ستمبر 2026 کو Anthropic کا اعلان کردہ یہ نتیجہ مسئلے کا پہلا مکمل، کمپیوٹر سے جانچا گیا ثبوت ہے۔
Lean کیا ہے؟
ایک پروف اسسٹنٹ: ایسی پروگرامنگ زبان جس میں تعریفیں، مسائل اور ثبوت کوڈ کی صورت لکھے جاتے ہیں۔ ایک چھوٹا قابلِ اعتماد پروگرام، کرنل، جانچتا ہے کہ ہر قدم منطق کے اصولوں اور پچھلے نتائج سے نکلتا ہے۔ اگر ثبوت کمپائل ہو جائے تو صرف Lean میں شامل مسلّمات مان کر مسئلہ تصدیق شدہ ہے۔
ثبوت کتنا بڑا تھا؟
تقریباً 1.3 کروڑ لائنیں Lean کوڈ اور تقریباً 30,000 مسائل (آخری ثبوت میں تقریباً 29,500 استعمال ہوئے)، جو Lean کی مرکزی برادری کی ریاضی لائبریری Mathlib سے پانچ گنا سے بھی بڑا ہے۔ اس میں 11 دن لگے، درجنوں Claude ایجنٹس متوازی کام کرتے رہے اور Anthropic کے محقق تیانی پینگ نے کبھی کبھار اعلیٰ سطحی رہنمائی دی۔
کیا AI کا لکھا ثبوت اچھا ہے؟
اس معنی میں درست ہے کہ Lean نے اسے جانچا ہے، اور امپیریل کالج لندن میں انسانی قیادت والے FLT باضابطگی منصوبے کی سربراہی کرنے والے کیون بزرڈ نے اس کا جائزہ لیا۔ مگر Anthropic کہتا ہے کہ یہ غالباً ضرورت سے کہیں لمبا ہے، اور ناکام کوششوں نے اس کی غیر بوائلرپلیٹ لائنوں کا تقریباً 7% چھوڑ دیا۔ درست اور خوش نما الگ چیزیں ہیں۔
قارئین کی درجہ بندی اور تبصرے
اس مضمون کو کئی مختلف پہلوؤں پر درجہ دیں — آپ کی درجہ بندی دوسرے قارئین کی مدد کرتی ہے، اور ہمیں بہتر بنانے میں مدد کرتی ہے۔
کیا یہ مضمون مفید تھا؟
ہمیں اپنی رائے بتائیں — کوئی اصلاح، کوئی سوال جس کا جواب نہیں ملا، یا کوئی موضوع جسے آپ اگلی بار کور ہوتے دیکھنا چاہتے ہیں۔
بات کرنا پسند کریں گے؟ اپنی سہولت کے وقت مفت ویڈیو کال بک کریں: فوری سوال کے لیے 15 منٹ، باقی کے لیے 30 منٹ۔ اوقات آپ کے اپنے ٹائم زون میں دکھائے جاتے ہیں۔
مصنف کے بارے میں
Sudershan Soni
موسٹک سروسز میں بانی اور مرکزی استاد — MSc اہلیت یافتہ ریاضی، سائنس، کمپیوٹر سائنس اور STEM کے استاد، 20 سال سے زائد پیشہ ورانہ تجربے کے ساتھ، 11+ اور GCSE سے A-Level اور اس سے آگے تک کے طلبہ کو دنیا بھر میں آن لائن پڑھاتے ہیں۔
مکمل پروفائل پڑھیں