Claude نے Lean میں Fermat's Last Theorem کو فارملائز کیا
Anthropic نے حال ہی میں ایک بہت بڑا تحقیقی کام مکمل کیا ہے۔ ایک اندرونی ماڈل نے Lean 4 اثبات کی زبان (proof language) کا استعمال کرتے ہوئے Fermat's Last Theorem کو فارملائز کرنے کے لیے 11 دن تک کام کیا۔
یہ کوئی نئی ریاضیاتی دریافت نہیں ہے۔ Andrew Wiles نے 1995 میں اس تھیورم کو ثابت کیا تھا۔ Anthropic نے جو کیا وہ اس موجودہ ثبوت کو کوڈ میں تبدیل کرنا تھا۔ اس سے کمپیوٹر کو مکمل یقین کے ساتھ ہر منطقی قدم کی جانچ کرنے کی اجازت ملتی ہے۔
اس پروجیکٹ کا پیمانہ بہت بڑا ہے: • ماڈل نے Lean کوڈ کی 13 ملین لائنیں تیار کیں۔ • اس نے 30,300 درمیانی