গাণিতিক যুক্তি, মডেল থিওরি ও অসম্পূর্ণতার ২০ খণ্ডের এই মহাকাব্যিক পরিক্রমার শেষে আমরা দাঁড়িয়ে আছি মানবজাতির জ্ঞানতাত্ত্বিক ইতিহাসের সবচেয়ে বৈপ্লবিক সন্ধিক্ষণে: একক মানব মস্তিষ্কের মাধ্যমে গণিত যাচাইকরণের যুগের অবসান। আধুনিক গণিতের প্রমাণগুলো আজ এমন দানবীয় আকারে পৌঁছেছে—হাজার হাজার পৃষ্ঠা, কম্পিউটার-চালিত লাখ লাখ হিসাব, কিংবা এত উচ্চমাত্রার বিমূর্ততা যা কোনো একক মানুষের পক্ষে আজীবন পরিশ্রম করেও শতভাগ নিশ্চিত করা অসম্ভব। এই সংকট থেকে উত্তরণে গণিত আবার ফিরে যাচ্ছে তার গোড়ার শিকড়ে, তবে এবার এক নতুন সঙ্গীকে নিয়ে: ইন্টারেক্টিভ থিওরেম প্রুভার (Interactive Theorem Provers)। Lean 4, Coq এবং Isabelle-এর হাত ধরে গণিতের সত্যতা রূপান্তরিত হচ্ছে ওপেন-সোর্স, কম্পিউটার-যাচাইকৃত এক অভ্রান্ত মহাজাগতিক প্রসাদে।
১. মানুষের পিয়ার-রিভিউ ব্যবস্থার গভীর সংকট
একবিংশ শতাব্দীতে এসে মানুষের তৈরি ঐতিহ্যবাহী জার্নাল ও পিয়ার-রিভিউ ব্যবস্থা তার সহনশীলতার চরম সীমায় পৌঁছেছে:
- ফাইনাইট সিম্পল গ্রুপের শ্রেণীবিন্যাস: কয়েক দশক ধরে শতাধিক গণিতবিদের লেখা ১৫,০০০-এর বেশি পৃষ্ঠার সমন্বয়। বারবার এর ভেতরে সূক্ষ্ম ফাঁকফোকর বেরিয়েছে যা ঠিক করতে বছরের পর বছর লেগেছে।
- কেপলার অনুমান (থমাস হেলস, ১৯৯৮): গোলক সাজানোর এই প্রমাণটি ছিল ৩০০ পৃষ্ঠার টেক্সট এবং বিশাল কম্পিউটার কোডের সমষ্টি। বিশ্বসেরা ১২ জন বিশেষজ্ঞের একটি দল চার বছর ধরে চুলচেরা বিশ্লেষণ করে রিপোর্ট দেন যে তাঁরা “৯৯% নিশ্চিত” প্রমাণটি সঠিক, কিন্তু প্রতিটি লাইন যাচাই করা তাঁদের পক্ষে মানবীয়ভাবে অসম্ভব। ক্ষুব্ধ হয়ে হেলস ট্র্যাডিশনাল জার্নাল ছেড়ে ফ্লাইস্পেক প্রকল্প (Flyspeck Project) শুরু করেন এবং ২০১৪ সালে সম্পূর্ণ প্রমাণটি কম্পিউটারে আনুষ্ঠানিকভাবে যাচাই করেন।
- মোচিজুকির আইইউটিটি প্রমাণ (২০১২): এবিসি কনজেকচারের ৫০০ পৃষ্ঠার এই প্রমাণ নিয়ে এক দশক ধরে বিশ্বের শীর্ষ গণিতবিদরা দ্বিধাবিভক্ত; কেউ নিশ্চিত করে বলতে পারছেন না এর একটি নির্দিষ্ট ধাপ আদৌ সঠিক কিনা।
ক্লান্তি, মনস্তাত্ত্বিক পক্ষপাত এবং সামাজিক কর্তৃত্বের কাছে জিম্মি মানুষের মস্তিষ্ক আজ আর গণিতের চরম নিশ্চয়তা দিতে সক্ষম নয়।
২. আধুনিক থিওরেম প্রুভারের মাইক্রোকার্নেল আর্কিটেকচার
লিন ৪ (Lean 4) এবং কক (Coq)-এর মতো আধুনিক থিওরেম প্রুভার এই সমস্যার সমাধান করেছে ডি ব্রুইন নীতি (de Bruijn Criterion)-এর ওপর ভিত্তি করে তৈরি একটি দ্বিমুখী আর্কিটেকচারের মাধ্যমে:
বিশ্বস্ত মাইক্রোকার্নেল কাঠামো
- বাইরের খোলস (AI ও ট্যাকটিক ইঞ্জিন): এটি একটি সুবিশাল সফটওয়্যার যা মানুষের কোড পড়ে, এআই দিয়ে প্রমাণ খোঁজে এবং জটিল হিসাব-নিকাশ চালায়। এই অংশে কোনো ত্রুটি বা বাগ থাকলেও গণিতের সত্যতা কখনো বিনষ্ট হতে পারে না।
- বিশ্বস্ত মাইক্রোকার্নেল (The Trusted Microkernel): এটি মাত্র ১,০০০ থেকে ২,০০০ লাইনের একটি অতি-ক্ষুদ্র, কঠোরভাবে পরীক্ষিত সি++ বা ওক্যামল কোড। এর একমাত্র কাজ হলো কারি-হাওয়ার্ড সাদৃশ্যের ভিত্তিতে টাইপ পরীক্ষা করা ($p : P$)।
বাইরের এআই যত ভুলভাল যুক্তিই তৈরি করুক না কেন, মাইক্রোকার্নেলের প্রবেশদ্বারে এসে টাইপ অমিল হলেই তা সাথে সাথে আটকে যায়। কার্নেল যে প্রমাণকে সবুজ সংকেত দেয়, তা শতভাগ নির্ভুল হতে বাধ্য।
৩. পিটার শলৎসের লিকুইড টেনসর পরীক্ষা (২০২১)
২০২০ সালের ডিসেম্বরে ২০১৮ সালের ফিল্ডস মেডেল বিজয়ী গণিতবিদ পিটার শলৎস তাঁর উদ্ভাবিত কনডেন্সড ম্যাথমেটিক্স-এর একটি অত্যন্ত জটিল উপপাদ্যের (থিওরেম ৯.৪) সত্যতা নিয়ে নিজের অজান্তেই দ্বিধাদ্বন্দ্বে পড়েন। তিনি প্রকাশ্যে বিশ্বের লিন বিশেষজ্ঞদের চ্যালেঞ্জ জানান তাঁর প্রমাণটি কম্পিউটারে যাচাই করে দেওয়ার জন্য।
ইয়োহান কমেলাইনের নেতৃত্বে একদল গণিতবিদ মাত্র ছয় মাসে সম্পূর্ণ প্রমাণটি লিন-এ এনকোড করেন (The Liquid Tensor Experiment)। প্রমাণ সফল হওয়ার পর শলৎস মন্তব্য করেন:
“যন্ত্র যখন আমার জটিল লেমাটি সফলভাবে যাচাই করল, তখন আমি এমন এক মানসিক নিশ্চয়তা পেলাম যা শতবার মানুষ দিয়ে রি-রিড করালেও কোনোদিন পাওয়া সম্ভব ছিল না। ফর্মাল ভেরিফিকেশন আজ এক অবিচ্ছেদ্য গাণিতিক বাস্তবতায় পরিণত হয়েছে।”
৪. ম্যাথলিব (Mathlib): আধুনিক আলেকজান্দ্রিয়ার ডিজিটাল লাইব্রেরি
এই আন্দোলনের সবচেয়ে গৌরবময় ফসল হলো ম্যাথলিব (Mathlib)—গিটহাবে হোস্ট করা গণিতের এক সার্বজনীন ওপেন-সোর্স লাইব্রেরি। চিরাচরিত বইপত্রে যেখানে একেক লেখক একেক নোটেশন ব্যবহার করেন, ম্যাথলিবে প্রতিটি নতুন উপপাদ্যকে সমগ্র গণিতের প্রাচীনতম সংজ্ঞার সাথে সামঞ্জস্য রেখে কোড করতে হয়। সংখ্যাতত্ত্ব, টপোলজি, অ্যাবস্ট্রাক্ট অ্যালজেব্রা এবং ডিফারেনশিয়াল ম্যানিফোল্ড আজ একক, সচল কম্পিউটার কোডের জালে আবদ্ধ।
৫. মহাজাগতিক মিলন: এআই, আনুষ্ঠানিক যুক্তি ও প্রমাণের ভবিষ্যৎ
আমাদের এই সিরিজের সমাপ্তিলগ্নে মানব ইতিহাসের তিনটি মহত্তম বুদ্ধিবৃত্তিক স্রোত একবিন্দুতে এসে মিলিত হয়েছে:
- মডেল থিওরি ও প্রথম-স্তরের যুক্তি: ভাষার যৌক্তিক সীমানা এবং কাঠামোর স্বরূপ উন্মোচন।
- ডিপ লার্নিং ও এআই: মানুষের মতো অন্তর্দৃষ্টি দিয়ে প্রমাণের নতুন ধারণা ও অনুমান উদ্ভাবন।
- ইন্টারেক্টিভ থিওরেম প্রুভার: পরম ক্রিপ্টোগ্রাফিক নিশ্চয়তা প্রদানকারী অকাট্য বিচারক।
হাজার বছর ধরে গণিত আবদ্ধ ছিল মানুষের ক্ষণস্থায়ী স্মৃতি আর ভঙ্গুর অনুমানের শিকলে। আজ কম্পিউটার-যাচাইকৃত টাইপ থিওরির মাধ্যমে গণিত লাভ করেছে তার অমর রূপ। লিবনিজ, হিলবার্ট ও গোডেল যে অভ্রান্ত সত্যের মন্দিরের স্বপ্ন দেখেছিলেন, তা আজ আর কোনো কালির অক্ষরে আবদ্ধ নয়—তা স্পন্দিত হচ্ছে অনন্ত, অবিনশ্বর কোডের জীবন্ত ছন্দে।
