পোয়াঁকারে, যন্ত্রের হাতে লাইন ধরে ধরে যাচাই

একটি প্রমাণ যাচাই করা গণিতের সবচেয়ে কঠিন কাজগুলোর একটি, বিশেষ করে যখন কোনো যুক্তি কয়েকটি ক্ষেত্র জুড়ে বিস্তৃত। এআই যত প্রমাণ তৈরির গতি বাড়াচ্ছে, নির্ভরযোগ্য যাচাই ততই গুরুত্বপূর্ণ হয়ে উঠছে। Lean 4-এর মতো প্রুফ অ্যাসিস্ট্যান্ট একটি উত্তর দেয়: সংজ্ঞা, বিবৃতি ও প্রমাণ কোড হিসেবে লেখা হয়, আর সফটওয়্যারের একটি ছোট বিশ্বস্ত কেন্দ্র, তার “কার্নেল”, প্রতিটি ধাপ পরীক্ষা করে। যে প্রমাণ কার্নেল পেরোয়, তা তার বিবৃতিকে প্রতিষ্ঠিত করে; মানুষের জন্য বাকি থাকে এটুকু যাচাই করা যে বিবৃতিটি সত্যিই সেটাই বলছে যা গণিতবিদেরা বোঝাতে চান।

একটি সংক্ষিপ্ত প্রমাণ, একটি অনুপস্থিত লাইব্রেরি

পেরেলম্যানের প্রমাণিত পোয়াঁকারে অনুমান বলে যে প্রতিটি বদ্ধ, সরলভাবে সংযুক্ত (সিম্পলি কানেক্টেড) ত্রিমাত্রিক বহুরূপ (ম্যানিফোল্ড) — অনানুষ্ঠানিকভাবে, এমন একটি সসীম ত্রিমাত্রিক স্থান যেখানে কোনো ফাঁস আটকে যেতে পারে এমন কোনো ছিদ্র নেই — ত্রিমাত্রিক গোলকের সমতুল্য। প্রমাণটি রিচার্ড হ্যামিল্টনের শুরু করা রিচি ফ্লো কর্মসূচি অনুসরণ করে। পেরেলম্যানের ২০০২–২০০৩ সালের তিনটি প্রিপ্রিন্ট মূল যুক্তিগুলো অত্যন্ত সংক্ষিপ্ত আকারে দিয়েছিল; তারপর বিস্তারিত বিবরণ আসে, যার মধ্যে আছে John Morgan ও Gang Tian-এর ২০০৭ সালের মনোগ্রাফ, যা এই প্রকল্প অনুসরণ করেছে।

ওই প্রমাণ জ্যামিতিক বিশ্লেষণের ওপর নির্ভর করে, যা Lean-এর সম্প্রদায়-চালিত লাইব্রেরি Mathlib-এ মূলত ছিল না। ভিত্তির বড় অংশ শূন্য থেকে গড়তে হয়েছে।

গণিতবিদদের স্থির করে দেওয়া মাইলফলক

পিকিং বিশ্ববিদ্যালয় ও বেইজিংয়ের অন্যান্য প্রতিষ্ঠানের Zhiyuan Zhang, Axel Delaval, Bin Dong, Chunlei Liu ও সহকর্মীরা মে ২০২৬-এ কাজ শুরু করেন: গাণিতিক প্রশিক্ষণপ্রাপ্ত তিনজন “এআই প্রকৌশলী” গণিতবিদদের পাশাপাশি কাজ করছিলেন। তাঁদের প্রথম পদ্ধতি — পটভূমি তত্ত্বের বড় বড় অংশকে আনুষ্ঠানিক রূপ দেওয়া — ছিল ধীর, আর এর ফলে তৈরি কোড তাঁদের প্রত্যাশা পূরণ করেনি।

সেপ্টেম্বর ২০২৬-এ তাঁরা নতুন করে শুরু করেন। প্রমাণটিকে প্রায় ৯০টি মাইলফলকে ভাগ করা হয়, যার প্রতিটি প্রয়োজনীয় সংজ্ঞাসহ একটি নির্দিষ্ট Lean বিবৃতি। গণিতবিদেরা এই বিবৃতিগুলো আনুষ্ঠানিক রূপ দেওয়ার আগে বা চলাকালীন পর্যালোচনা করেন, তারপর সেগুলো স্থির (ফ্রিজ) করে দেওয়া হয়: এজেন্টরা সেগুলো বদলাতে পারত না, আর যেকোনো সংশোধন গণিতবিদদের মাধ্যমেই যেত। যেহেতু এজেন্টদের লেখা প্রতিটি লাইন কেউ পড়তে পারত না, এই মাইলফলকগুলোই হয়ে ওঠে সেই চেকপয়েন্ট, যেখানে মানুষ গণিত যাচাই করেছে।

এরপর এজেন্টরা সমান্তরালে কাজ করে — কোডিং টুলের (মূলত Codex ও Claude Code) সঙ্গে ইন্টারঅ্যাকটিভ সেশনের মাধ্যমে, এবং Archon Horizon নামের একটি ব্যবস্থার মাধ্যমে, যা সীমিত পরিসরের “মিশন” বহু সার্ভারে পাঠায়। একটি বট প্রতিটি অবদান কম্পাইল করত এবং গৃহীতগুলো একীভূত করত। বিবৃতিগুলোকে আনুষ্ঠানিক রূপ দেওয়া ও প্রমাণ তৈরির বেশির ভাগ কাজ করেছে GPT-6-Astra; Fable-5.1 ব্যবহৃত হয়েছে স্বাধীন যাচাই, আটকে যাওয়া কাজের সমস্যা নির্ণয় এবং বিবৃতি পর্যালোচনার জন্য।

প্রায় দুই সপ্তাহে ২৮ লাখ লাইন

মাসের পর মাস প্রস্তুতির পর মূল আনুষ্ঠানিকীকরণে লেগেছে দুই সপ্তাহের সামান্য বেশি। এআই সাবস্ক্রিপশন ও ভাড়া করা সার্ভারে খরচ হয়েছে প্রায় ২৫,০০০ ডলার। কাজটি উপপাদ্যের টপোলজিক্যাল ও মসৃণ দুই সংস্করণই প্রমাণ করে, পুরোপুরি কম্পাইল হয়, এবং কেবল Mathlib দিয়ে লেখা লক্ষ্য-বিবৃতির বিপরীতে একটি স্বাধীন যাচাইয়ে উত্তীর্ণ হয়।

এটি বিশাল: Lean-এর প্রায় ৩২ লাখ লাইন, যা চূড়ান্ত উপপাদ্য যার ওপর নির্ভর করে কেবল সেটুকু রেখে ২৮ লাখে ছাঁটা হয়েছে। লেখকদের হিসাবে, প্রায় অর্ধেকই পটভূমি তত্ত্ব। একটি ধ্রুপদি ফলাফল, যা Morgan ও Tian কেবল একটি পাদটীকায় উল্লেখ করেছেন — ত্রিমাত্রিক বহুরূপের ওপর মসৃণ কাঠামো নিয়ে — একাই নিয়েছে প্রায় ৬,৫০,০০০ লাইন।

মানুষ তবু কী করেছে

লেখকেরা বাধাগুলোকে তিন ভাগে ভাগ করেন: গাণিতিক ফাঁক, Lean-এ বাস্তবায়নের সমস্যা এবং সমন্বয়ের সমস্যা। মানুষ বিবৃতির পরিসর ঠিক করেছে (যেমন, কখন একটি ফলাফলকে তিন মাত্রায় সীমিত করতে হবে), অনুপস্থিত যুক্তি ধরেছে — যেমন একটি স্থানীয় সংহতির (লোকাল কম্প্যাক্টনেস) ধাপ, যা এজেন্টরা খুঁজে পায়নি — এবং লুকানো অনুমান ধরে ফেলেছে। তাঁদের মূল শিক্ষা: এজেন্টদের সক্ষমতার মতোই গুরুত্বপূর্ণ ছিল কাজের সংগঠন। Anthropic-এর সাম্প্রতিক ফার্মার শেষ উপপাদ্যের আনুষ্ঠানিকীকরণ থেকেও তাঁরা একই সিদ্ধান্তে পৌঁছান, যেটিকেও প্রাথমিক প্রচেষ্টাগুলো প্রকল্পের অবস্থার হিসাব হারিয়ে ফেলার পর নতুন করে শুরু করতে হয়েছিল।

যাচাইকৃত, কিন্তু এখনও গোছানো নয়

লেখকেরা কাজটিকে শেষ বলে মনে করেন না। কোডে প্রচুর পুনরাবৃত্তি; এজেন্টদের প্রমাণ সবসময় রেফারেন্সের পথ অনুসরণ করে না; আর একে জ্যামিতিক বিশ্লেষণের একটি পুনর্ব্যবহারযোগ্য লাইব্রেরিতে রূপ দেওয়াই পরবর্তী কাজ। আরেকটি দল একই অনুমানের একটি স্বাধীন আনুষ্ঠানিকীকরণের ঘোষণাও দিয়েছে। তাঁদের আশা: একদিন একজন গণিতবিদ একাই এমন সরঞ্জাম দিয়ে নিজের গবেষণা যাচাই করতে পারবেন।

স্বার্থের সংঘাত। দলটি Claude Code ও Fable-5.1 মডেল ব্যবহার করেছে, দুটিই Anthropic-এর, সঙ্গে OpenAI সাবস্ক্রিপশনের মাধ্যমে ব্যবহৃত GPT-6-Astra, যা বেশির ভাগ কাজ করেছে। গবেষণাপত্রটি তার প্রকল্পকে Anthropic-এর ফার্মার শেষ উপপাদ্যের আনুষ্ঠানিকীকরণের সঙ্গেও তুলনা করেছে। এই লেখাটি Claude-এর লেখা।