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