প্রযুক্তি বিষয়ক গণমাধ্যম Gigazine গতকাল (৩ আগস্ট) একটি ব্লগ পোস্ট প্রকাশ করে জানিয়েছে যে AI-এর সহায়তায় সম্পন্ন এবং কোলাটজ অনুমানকে খণ্ডন করার দাবি করা একটি Lean আনুষ্ঠানিক প্রমাণকে অকার্যকর বলে নিশ্চিত করা হয়েছে।
দ্রষ্টব্য: কোলাটজ অনুমান (অড-ইভেন স্বাভাবিকীকরণ অনুমান / 3n+1 অনুমান নামেও পরিচিত) জার্মান গণিতবিদ লোথার · কোলাটজ (Lothar Collatz) 1937 সালে প্রস্তাব করেন। এটি অত্যন্ত সরল ভাষায় প্রকাশ করা হলেও এখনো অমীমাংসিত একটি গাণিতিক সমস্যা। এতে বলা হয়, যেকোনো ধনাত্মক পূর্ণসংখ্যাকে নির্দিষ্ট নিয়মে বারবার প্রয়োগ করলে শেষ পর্যন্ত তা অবশ্যই 1-এ ফিরে আসবে।
যেকোনো ধনাত্মক পূর্ণসংখ্যা n-এর জন্য নিয়মগুলো হলো:
n জোড় হলে, তাকে 2 দিয়ে ভাগ করতে হবে (n ÷ 2)।
n বিজোড় হলে, তাকে 3 দিয়ে গুণ করে 1 যোগ করতে হবে (3n + 1)।
নতুন সংখ্যা পাওয়ার পর ফলাফল 1 না হওয়া পর্যন্ত ওপরের ধাপগুলো পুনরাবৃত্তি করতে হবে।
উদাহরণ হিসেবে 6 নেওয়া যাক:
6 জোড়, 2 দিয়ে ভাগ করলে 3 পাওয়া যায়
3 বিজোড়, 3 দিয়ে গুণ করে 1 যোগ করলে 10 পাওয়া যায়
10 জোড়, 2 দিয়ে ভাগ করলে 5 পাওয়া যায়
5 বিজোড়, 3 দিয়ে গুণ করে 1 যোগ করলে 16 পাওয়া যায়
16-কে ধারাবাহিকভাবে 2 দিয়ে ভাগ করলে 8, 4, 2, 1 পাওয়া যায়
চূড়ান্ত ধারা হলো: 6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1।
আনুষ্ঠানিক যাচাইকরণ বিশেষজ্ঞ Ramana Kumar ২৫ জুলাই GitHub-এ একটি প্রকল্প প্রকাশ করেন। শুরুতে তিনি দাবি করেছিলেন যে AI-এর সহায়তায় কোলাটজ অনুমানকে খণ্ডন করা হয়েছে। প্রকল্পটিতে কোনো নির্দিষ্ট পাল্টা উদাহরণ হিসেবে পূর্ণসংখ্যা দেওয়া হয়নি; শুধু Lean (উপপাদ্য প্রমাণের সহায়ক ব্যবস্থা)-এ “1-এ পৌঁছাতে পারে না এমন একটি সংখ্যা বিদ্যমান”—এটি প্রমাণ করা হয়েছিল।
Lean একটি উপপাদ্য প্রমাণের সহায়ক ব্যবস্থা। এটি ব্যবহারকারীদের গাণিতিক সূত্র ও যুক্তিকে প্রোগ্রাম হিসেবে লিখতে এবং কম্পিউটারের মাধ্যমে প্রমাণের নির্ভুলতা যাচাই করতে সহায়তা করে। ব্যবহারকারীর লেখা Lean কোড গাণিতিক প্রস্তাব ও প্রমাণকে যাচাইযোগ্য প্রোগ্রামে রূপান্তর করে, আর কার্নেল প্রকার ও যুক্তির সামঞ্জস্য যাচাই করে।
তবে পরে তিনি খণ্ডনমূলক বিষয়বস্তু পর্যালোচনা করার সময়发现 করেন যে সংশ্লিষ্ট পদ্ধতি Lean-কে কোনো শর্ত ছাড়াই “False” গ্রহণ করাতেও সক্ষম, যেখানে এটি মিথ্যা প্রস্তাব বোঝায়। তাই সংশ্লিষ্ট কোড বর্তমানে কোলাটজ অনুমানকে খণ্ডন করতে পারে না।
আনুষ্ঠানিক যাচাইকরণ গবেষক Kiran Gopinathan সমস্যাটিকে একটি ছোট পুনরুৎপাদনযোগ্য কোডে নামিয়ে আনেন এবং 2026 সালের 28 জুলাই Lean উন্নয়ন দলকে তা জানান।
ত্রুটিটি কার্নেলের “নেস্টেড ইন্ডাক্টিভ টাইপ” প্রক্রিয়াকরণ অংশে ছিল। এর ফলে কখনো কখনো “গোস্ট টাইপ প্যারামিটার” উপেক্ষিত হতো, অর্থাৎ এমন প্যারামিটার যা সরাসরি ডেটা স্ট্রাকচারের উপাদানে উপস্থিত নয়। ফলে মূলত ভুল হিসেবে শনাক্ত হওয়া উচিত এমন প্যারামিটার যাচাই এড়িয়ে যেতে পারত। Lean-এর ডেভেলপার Leonardo de Moura জানান, কার্নেল বাস্তবায়নে প্রয়োজনীয় যাচাই সম্পূর্ণ না থাকাই সমস্যার কারণ।
রিপোর্ট পাওয়ার প্রায় 1 ঘণ্টার মধ্যে Lean দল একটি সংশোধনী পুল রিকোয়েস্ট তৈরি করে এবং 28 জুলাই Lean 4.32.2 সংস্করণ প্রকাশ করে, যেখানে এই সমস্যা সংশোধন করা হয়েছে।