অ্যানথ্রোপিক জানিয়েছে, ক্লড ফার্মার শেষ উপপাদ্যের প্রথম সম্পূর্ণ ফর্মাল প্রমাণ সম্পন্ন করেছে। এটি এই উপপাদ্যটি পুনরাবিষ্কার করা নয়, বরং বিদ্যমান প্রমাণটিকে কম্পিউটারের দ্বারা প্রতিটি লাইনে যাচাইয়ের জন্য যুক্তিসঙ্গত কোডে রূপান্তরিত করা। কোম্পানি বলেছে, এই কাজটি করতে ১১ দিন সময় লেগেছে এবং শেষ পর্যন্ত প্রায় ১.৩ কোটি লাইন তৈরি হয়েছে।
ফর্মাল প্রমাণের গুরুত্ব হলো গাণিতিক যুক্তিকে মেশিন দ্বারা পরীক্ষা করা যায় এমন ভাষায় লেখা। পারম্পরিক পেপার প্রমাণগুলির জন্য পিয়ার-রিভিউ করতে বছরের পর বছর লাগে, এবং যদি কোনো ধাপে ফাঁক থাকে, তবে এটি মেরামত করতে মাস বা এমনকি বছরের পর বছর লাগতে পারে। ১৯৯৫ সালে ব্রিটিশ গণিতবিদ অ্যান্ড্রুয়াস ওয়াইলস ফার্মার শেষ উপপাদ্যের প্রমাণ সম্পন্ন করেন, কিন্তু এই প্রমাণটিকে সম্পূর্ণভাবে মেশিন-চেকযোগ্য সংস্করণে রূপান্তরিত করা সবসময়ই একটি অত্যন্ত শক্তিশালী ইঞ্জিনিয়ারিং প্রকল্প হিসেবে বিবেচিত হয়েছে।
11 দিনে দীর্ঘমেয়াদি প্রকল্পের লক্ষ্য পূরণ করুন
লন্ডন ইম্পেরিয়াল কলেজের গণিতবিদ কেভিন বাজার্ড ২০২৪ সাল থেকে এই প্রকল্পটি চালু করেছেন, যার লক্ষ্যও হল Wiles-এর প্রমাণটিকে Lean প্রমাণ সহায়কে পুনর্লিখন করা। মূল পরিকল্পনা অনুযায়ী, এই কাজটি দীর্ঘমেয়াদি সহযোগিতার প্রয়োজন হবে, এবং ২০২৯ সাল পর্যন্ত অর্থায়ন নিশ্চিত করা হয়েছে।
অ্যানথ্রোপিক জানায়, ক্লড এই কাজে অনুরূপ লক্ষ্যগুলি আগেই সম্পন্ন করেছে। বাজার্ড পর্যালোচনা করে বলেন, এই প্রমাণটি অতিরিক্ত ধারণার উপর নির্ভর না করেই প্রতিষ্ঠিত হতে পারে, অর্থাৎ শুধুমাত্র গণিতের সবচেয়ে মৌলিক অক্ষরসমূহের উপর ভিত্তি করে এটি যাচাই করা যায়।
একাধিক এজেন্ট দ্বারা সমান্তরালে সম্পন্ন হয়
অ্যানথ্রোপিকের বর্ণনা অনুযায়ী, কলম্বিয়া বিশ্ববিদ্যালয়ের গবেষক তিয়ানই পেঙ্গের দল একাধিক Claude এজেন্টকে সমান্তরালভাবে কাজ করানোর মাধ্যমে সংজ্ঞা লেখা, ছোট উপসংহারগুলির প্রমাণ দেওয়া এবং ধাপে ধাপে বড় প্রমাণ কাঠামোগুলি তৈরি করার কাজ করেছে। মানব হস্তক্ষেপ কম, মূলত পর্যায়ক্রমিক অগ্রাধিকারের ক্রম নির্ধারণ করা।
প্রাথমিক অগ্রগতি সুসংগঠিত ছিল না। এনথ্রোপিক বলেছে, কিছু এজেন্ট একসময় সম্পন্ন করা কনটেন্ট শেয়ার করতে অক্ষম হয়েছিল এবং পুনরায় কাজ করছিল। তারপর, টিমটি Prove2Me নামক একটি টুল ব্যবহার করে, প্রতিটি এজেন্টের জন্য একটি একক কাজের তালিকা এবং ফাইল সংগঠনের ব্যবস্থা করেছে, এবং তাদের পরস্পরের ফলাফল পুনর্ব্যবহারের জন্য প্রাকৃতিক ভাষার মন্তব্যগুলি সংরক্ষণ করেছে।
- 30,000 এর বেশি সমর্থন থিওরেম
- বিলিয়ন টোকেন পর্যন্ত মোট খরচ হয়েছে
- চূড়ান্ত প্রমাণ প্রায় 1300 মিলিয়ন লাইন
যাচাইযোগ্যতার উপর জোর দিন, নতুন উপপাদ্যের উপর নয়
এই সাফল্যের মূল বিষয় হল নতুন গাণিতিক উপপাদ্য আবিষ্কার করা নয়, বরং পূর্বে প্রমাণিত গুরুত্বপূর্ণ উপপাদ্যগুলিকে কম্পিউটার দ্বারা ধাপে ধাপে যাচাইযোগ্য ভার্সনে রূপান্তরিত করা। গাণিতিক পেপার এবং AI-জেনারেটেড কনটেন্টের বৃদ্ধির সাথে সাথে মানুষের দ্বারা প্রমাণগুলি ধাপে ধাপে যাচাইয়ের খরচও বৃদ্ধি পাচ্ছে, ফলে ফরমালাইজেশন টুলসগুলির প্রতি আরও বেশি মনোযোগ দেওয়া হচ্ছে।
অ্যানথ্রোপিক আরও জানায়, এই প্রমাণের আকার গণিতের ক্ষেত্রে সাধারণত ব্যবহৃত শেয়ার্ড লাইব্রেরি Mathlib-এর চেয়ে পাঁচগুণের বেশি। পূর্ণাঙ্গ ফাইলটি GitHub-এ আপলোড করা হয়েছে, যেখানে গবেষকরা এর কাঠামো এবং সঠিকতা পর্যায়ক্রমে পরীক্ষা করতে পারবেন।