গণিতচর্চার দীর্ঘ ইতিহাসে ‘ভুল প্রমাণ’ কোনো অচেনা ঘটনা নয়। বহু উপপাদ্য বছরের পর বছর সঠিক বলে প্রচলিত ছিল, কিন্তু পরবর্তীকালে সূক্ষ্ম যৌক্তিক ফাঁক ধরা পড়েছে। এর সবচেয়ে পরিচিত দৃষ্টান্ত হলো ফোর কালার থিওরেম। ১৮৭৯ সালে আলফ্রেড কেম্পে এই উপপাদ্যের প্রমাণ দাবি করেছিলেন; প্রায় এক দশক পর দেখা যায় তাঁর যুক্তির একটি গুরুত্বপূর্ণ অংশে ত্রুটি ছিল। পরবর্তী সময়ে, ১৯৭৬ সালে কেনেথ অ্যাপেল ও উলফগ্যাং হাকেন কম্পিউটারের সাহায্যে হাজার হাজার সম্ভাব্য ক্ষেত্র যাচাই করে নতুন একটি প্রমাণ উপস্থাপন করেন। তবু সেই প্রমাণের একটি বড় অংশ এমন প্রোগ্রামের ওপর নির্ভরশীল ছিল, যা হাতে-কলমে মানুষের পক্ষে সম্পূর্ণ যাচাই করা প্রায় অসম্ভব। তাই ২০০৫ সালে মাইক্রোসফট রিসার্চের জর্জ গঁতিয়ে ও ইনরিয়ার বেঞ্জামিন ওয়ার্নার ‘কক’ নামে একটি প্রুফ অ্যাসিস্ট্যান্টে থিওরেমটির সম্পূর্ণ প্রমাণ নতুন করে লিখে ফেলেন। এবার কম্পিউটার শুধু হিসাব করেনি; প্রমাণের প্রতিটি ধাপ নিজেই যুক্তির নিয়ম মেনে পরীক্ষা করেছে। ২০২৫ সালের মার্চ পর্যন্ত এই সফটওয়্যার বিশ্বব্যাপী ‘কক’ নামেই পরিচিত ছিল; পরবর্তীতে এটি ‘রক প্রুভার’ নামে নতুন পরিচয় লাভ করে। নাম পরিবর্তিত হলেও এর মৌলিক লক্ষ্য অপরিবর্তিত—এমন প্রমাণ তৈরি ও যাচাই করা, যেখানে কোনো যৌক্তিক ফাঁক থাকার অবকাশই নেই।
একটি প্রুফ অ্যাসিস্ট্যান্ট কীভাবে কাজ করে, তা বোঝার জন্য লেগো খেলার তুলনা দেওয়া যেতে পারে। লেগোতে যেমন একটি টুকরা কেবল নির্দিষ্ট ধরনের আরেকটি টুকরার সঙ্গেই জোড়া লাগে, তেমনি এই সফটওয়্যারেও প্রতিটি যৌক্তিক ধাপের জন্য সুনির্দিষ্ট নিয়ম নির্ধারিত থাকে। জোর করে কোনো অংশ বসানোর সুযোগ নেই। এখানে গণিতের স্বীকার্য ও অনুমিতির নিয়ম আগে থেকেই স্থির করা থাকে। প্রমাণ লেখার সময় একের পর এক যৌক্তিক ‘টুকরা’ জোড়া লাগাতে হয়। যদি কোনো ধাপ পূর্ববর্তী ধাপ থেকে যৌক্তিকভাবে না আসে, তবে সফটওয়্যার সঙ্গে সঙ্গে সেটি থামিয়ে দেয়। মানুষের মতো ‘ঠিকই তো মনে হচ্ছে’ বলে এড়িয়ে যাওয়ার পথ এখানে বন্ধ। কিন্তু সফটওয়্যারটি কীভাবে বুঝবে যে একটি ধাপ সত্যিই সঠিক? এর উত্তর লুকিয়ে আছে টাইপ থিওরি নামক ধারণায়। এখানে প্রতিটি গাণিতিক বিবৃতিকে একটি টাইপ হিসেবে ধরা হয়, আর সেই বিবৃতির প্রমাণকে ওই টাইপের একটি বৈধ মান হিসেবে গণ্য করা হয়। কম্পিউটার প্রোগ্রাম যেমন বুঝতে পারে কোথায় সংখ্যা বসানো উচিত, তেমনি প্রুফ অ্যাসিস্ট্যান্টও পরীক্ষা করে দেখে যে কোনো প্রমাণ সত্যিই তার দাবি করা উপপাদ্যের সঙ্গে মেলে কি না। কম্পিউটার বিজ্ঞান ও যুক্তিবিদ্যায় এই সম্পর্ককে কারি–হাওয়ার্ড সমরূপতা বলা হয়—যেখানে প্রোগ্রাম ও গাণিতিক প্রমাণ একই মৌলিক কাঠামোর দুটি ভিন্ন প্রকাশ।
এই পুরো প্রক্রিয়াটি খুব সংক্ষিপ্ত কয়েকটি ধাপে ঘটে। প্রতিটি নতুন যুক্তি প্রথমে কার্নেল বা মূল প্রসেসরের কাছে যায়। কার্নেল সেটিকে আগে থেকে নির্ধারিত নিয়মের সঙ্গে মিলিয়ে দেখে। নিয়ম মানলে পরবর্তী ধাপে যাওয়ার অনুমতি মেলে; সামান্য অসংগতি থাকলেও পুরো প্রমাণ সেখানেই আটকে যায়। রক বা কক দেখিয়ে দিয়েছিল যে কম্পিউটার দিয়ে গাণিতিক প্রমাণ যাচাই করা সম্ভব। কিন্তু এরপর আরও বড় একটি প্রশ্ন সামনে আসে—পুরো গণিতকেই কি ধীরে ধীরে কম্পিউটারের ভাষায় লেখা সম্ভব? এই প্রশ্নের উত্তর খুঁজতেই ২০১৩ সালে লিওনার্দো দ্য মোরা তৈরি করেন ‘লিন’। শুরুতে এটি ছিল কম্পিউটার বিজ্ঞানীদের জন্য একটি প্রুফ অ্যাসিস্ট্যান্ট; কিন্তু কয়েক বছরের মধ্যেই এটি সম্পূর্ণ ভিন্ন পথে হাঁটতে শুরু করে। ২০১৭ সালের দিকে ইম্পেরিয়াল কলেজ লন্ডনের অধ্যাপক কেভিন বাজার্ড একটি সাহসী ধারণা সামনে আনেন—বিশ্ববিদ্যালয়ের পুরো আন্ডারগ্র্যাজুয়েট গণিত কি লিনে লেখা সম্ভব? এই স্বপ্ন থেকেই জন্ম নেয় ম্যাথলিব, যা লিনের জন্য তৈরি একটি উন্মুক্ত গাণিতিক গ্রন্থাগার। আজ বিশ্বের পাঁচ শতাধিক গবেষক, শিক্ষক ও শিক্ষার্থী একসঙ্গে এতে অবদান রেখেছেন। তাঁদের সম্মিলিত প্রচেষ্টায় এই লাইব্রেরির আকার এখন প্রায় ১৯ লাখ লাইন কোডে পৌঁছেছে। সংখ্যাটি বিশাল মনে হতে পারে, কিন্তু এর প্রকৃত গুরুত্ব বোঝা যায় যখন দেখা যায়, এখানকার প্রতিটি নতুন লাইন শুধু কোড নয়; এটি একটি নতুন সংজ্ঞা, উপপাদ্য বা প্রমাণ, যা কম্পিউটার নিজেই যাচাই করতে পারে।
এই প্রযুক্তির প্রভাব শুধু তত্ত্বগত নয়, বাস্তব গবেষণাতেও স্পষ্ট। ২০২০ সালে ফিল্ডস মেডেলজয়ী গণিতবিদ পিটার শলৎসে নিজের একটি অত্যন্ত জটিল উপপাদ্যের প্রমাণ নিয়ে একটি অস্বস্তিকর সত্য স্বীকার করেন। প্রমাণটি এত দীর্ঘ ও জটিল ছিল যে তিনিও নিশ্চিত ছিলেন না, এর কোথাও কোনো সূক্ষ্ম ভুল রয়ে গেছে কি না। তাই তিনি মানুষের কাছে প্রমাণটি আবার পড়ে দেখার অনুরোধ না করে, বিশ্বের গণিতবিদদের আহ্বান জানান সেটিকে লিনে রূপান্তর করতে। ইয়োহান কমেলিনের নেতৃত্বে একদল স্বেচ্ছাসেবী গবেষক প্রায় দুই বছর ধরে সেই কাজ করেন। অবশেষে ২০২২ সালের জুলাইয়ে ‘লিকুইড টেনসর এক্সপেরিমেন্ট’ নামে সেই কাজ সম্পন্ন হয়। লিনের কার্নেল নিশ্চিত করে যে শলৎসের প্রমাণে কোনো যৌক্তিক ফাঁক নেই। এই সাফল্য অনেকের কাছেই একটি প্রতীকী মুহূর্ত—প্রুফ অ্যাসিস্ট্যান্ট যে কেবল শিক্ষার জন্যই নয়, বরং আধুনিক গবেষণারও একটি নির্ভরযোগ্য সহকারী হতে পারে, সেটি স্পষ্ট হয়ে ওঠে। তাছাড়া, ২০২৩ সাল থেকে কেভিন বাজার্ডের নেতৃত্বে আরও উচ্চাকাঙ্ক্ষী একটি উদ্যোগ শুরু হয়েছে—অ্যান্ড্রু ওয়াইলসের ঐতিহাসিক ফার্মার শেষ উপপাদ্যের সম্পূর্ণ প্রমাণ লিনে ফরমালাইজ করা। প্রকল্পটি এখনো চলমান; সফল হলে তা হবে আধুনিক গণিতের সবচেয়ে বিখ্যাত প্রমাণগুলোর একটি, যার প্রতিটি ধাপ কম্পিউটার নিজেই যাচাই করতে পারবে।
তবে এই প্রযুক্তির প্রয়োজন কি শুধু গণিতবিদদের মধ্যেই সীমাবদ্ধ? একেবারেই নয়। এমন অনেক ক্ষেত্র আছে, যেখানে সফটওয়্যারের একটি ছোট ভুলও বড় দুর্ঘটনার কারণ হতে পারে। বিমানের নিয়ন্ত্রণব্যবস্থা, ট্রেনের সিগন্যালিং সফটওয়্যার কিংবা মেডিকেল ডিভাইস—এসব জায়গায় ‘মোটামুটি ঠিক’ বলে কোনো কিছু পার পাওয়ার সুযোগ নেই। প্রতিটি নির্দেশ সঠিকভাবে কাজ করতেই হবে। এই কারণেই ফরমাল ভেরিফিকেশন এখন নিরাপত্তাপূর্ণ সফটওয়্যার তৈরির একটি গুরুত্বপূর্ণ পদ্ধতি হয়ে উঠছে। এর একটি উল্লেখযোগ্য উদাহরণ হলো কম্পসার্ট। ফ্রান্সের বিজ্ঞানী জাভিয়ে লেরোয়া কক ব্যবহার করে সি প্রোগ্রামিং ভাষার জন্য এমন একটি কম্পাইলার তৈরি করেছেন, যার প্রতিটি ধাপ গাণিতিকভাবে যাচাই করা যায়। নির্দিষ্ট শর্তের মধ্যে এটি প্রোগ্রামারের কোড ভুলভাবে অনুবাদ করবে না—এই দাবিরও একটি আনুষ্ঠানিক প্রমাণ রয়েছে। তাই আজ বিমান, রেলপথ, মহাকাশপ্রযুক্তি কিংবা চিকিৎসার সফটওয়্যারের মতো সংবেদনশীল ক্ষেত্রগুলোতে এমন ‘প্রমাণসহ’ সফটওয়্যারের গুরুত্ব ক্রমশ বাড়ছে।
অন্যদিকে, গুগলের অ্যালফাপ্রুফ আন্তর্জাতিক গণিত অলিম্পিয়াডের সমস্যা সমাধান করতে সক্ষম হয়েছে। কিন্তু এর সবচেয়ে বড় শক্তি কোথায়? উত্তরটি খুবই সরল। অ্যালফাপ্রুফ যখন কোনো সম্ভাব্য সমাধান তৈরি করে, তখন সেটিকে সরাসরি ‘সঠিক’ বলে ধরে নেওয়া হয় না। বরং সেই সমাধানের প্রতিটি ধাপকে লিনের কার্নেল একে একে পরীক্ষা করে। কোথাও একটি ধাপ আগের ধাপ থেকে যৌক্তিকভাবে না এলে পুরো প্রমাণই বাতিল হয়ে যায়। এখানেই মানুষ ও প্রুফ অ্যাসিস্ট্যান্টের পার্থক্য। একজন গণিতবিদ হয়তো কোনো ধাপকে ‘স্পষ্ট’ ধরে নিয়ে এগিয়ে যেতে পারেন; কিন্তু লিন কোনো কিছু অনুমান করে নেয় না। প্রতিটি দাবির জন্য তাকে যুক্তি দেখাতে হয়। এই কঠোর যাচাই প্রক্রিয়াই অ্যালফাপ্রুফের তৈরি প্রমাণকে এতটা নির্ভরযোগ্য করে তোলে।
বাংলাদেশের জন্য এই পরিবর্তনের অর্থ বেশ গুরুত্বপূর্ণ। আমাদের দেশে এখনো অলিম্পিয়াড কিংবা বিশ্ববিদ্যালয় পর্যায়ে প্রমাণ লেখা শেখানো হয় মূলত কাগজ-কলমে এবং শিক্ষকের মূল্যায়নের মাধ্যমে। এই পদ্ধতি অবশ্যই প্রয়োজনীয়। কিন্তু ভবিষ্যতের গবেষণায় এর সঙ্গে আরও একটি দক্ষতা যোগ হতে পারে। একজন শিক্ষার্থী হয়তো আজ কাগজে একটি সুন্দর প্রমাণ লিখতে শিখছে। আগামী দশকে সেই একই শিক্ষার্থীকে হয়তো নিজের যুক্তি লিন বা রকের মতো একটি প্রুফ অ্যাসিস্ট্যান্টের সামনে উপস্থাপন করতে হবে। সেখানে ‘এটা তো পরিষ্কার’ বলে কোনো ধাপ এড়িয়ে যাওয়া যাবে না। প্রতিটি যুক্তিকে শেষ পর্যন্ত যৌক্তিকভাবে প্রতিষ্ঠা করতে হবে। গণিত শেখার ধরন হয়তো বদলাবে না, কিন্তু গণিত যাচাই করার পদ্ধতি নিঃসন্দেহে বদলাতে শুরু করেছে। গণিতের সৌন্দর্য কখনোই শুধু সঠিক উত্তরে থাকে না; বরং সেই উত্তরে পৌঁছানোর যুক্তির মধ্যেই লুকিয়ে থাকে এর আসল সৌন্দর্য। সেই যুক্তি এত দিন যাচাই করতেন মানুষ। এখন সেই কাজের একটি অংশ ধীরে ধীরে ভাগ করে নিচ্ছে কম্পিউটার। এর অর্থ এই নয় যে যন্ত্র গণিতবিদদের স্থান দখল করে নিচ্ছে। নতুন ধারণা, নতুন উপপাদ্য কিংবা নতুন অন্তর্দৃষ্টি—এসব এখনো মানুষের কল্পনাশক্তিরই ফসল। কিন্তু সেই ধারণাগুলোকে নিখুঁতভাবে যাচাই করার ক্ষেত্রে প্রুফ অ্যাসিস্ট্যান্ট এক নতুন মানদণ্ড তৈরি করছে। হয়তো আগামী প্রজন্মের গণিতবিদেরা কেবল কাগজে নয়, কি-বোর্ডেও প্রমাণ লিখবেন। তাঁদের পাশে থাকবে এমন এক সহকারী, যে কখনো ক্লান্ত হয় না, কখনো অনুমান করে না, আর একটি ভুল ধাপও ক্ষমা করে না। গণিতের ভাষা বদলাচ্ছে না; বদলাচ্ছে সেই ভাষা যাচাই করার পদ্ধতি। আর সেই পরিবর্তনের সাক্ষী হয়েই আমরা হয়তো গণিতচর্চার এক নতুন যুগে প্রবেশ করছি।
