Theorem.chat পরিচিতি
Theorem.chat একটি গাণিতিক দাবি গ্রহণ করে এবং এটি সমাধান করার চেষ্টা করে। আপনি দাবিটি উল্লেখ করেন, এবং এটির মান পূরণ করতে হবে। AI মডেলের একটি প্যানেল - আপনি যে পরিমাণ চান, যে কোন বিক্রেতা থেকে আপনি চান - এটি আক্রমণ করে, এবং আরো একটি মডেল রিফার। তারপর যুক্তি Lean 4 এর বিরুদ্ধে Mathlib-এ সরকারি করা হয়, এবং লিন কার্নেল সিদ্ধান্ত নেয় এটি প্রমাণিত কিনা। শেষ পদক্ষেপটি হল উৎপাদন।
কেন একটি কার্নেল, এবং অন্য মডেল না
একটি মডেলকে কঠিন প্রশ্ন জিজ্ঞেস করুন এবং আপনি একটি নিরপেক্ষ উত্তর পাবেন তা সঠিক কিনা তা জানতে । একাধিক প্রশ্ন জিজ্ঞেস করুন এবং তারা প্রায়শই একমত হবে, যা অনুমোদনের মত অনুভূত হয় এবং তা নয়: মডেলগুলি প্রশিক্ষণ তথ্য এবং অন্ধ স্থানের অংশীদারিত্ব ভাগ করে নেয় । প্রথমটি পরীক্ষা করে দ্বিতীয় মডেলটি এখনও একই ধরনের বিচার, এবং এটি ঘুরে বলা যেতে পারে । লিন কার্নেল পারে না । এটি হয়ত Mathlib এবং Mathlib থেকে বিবৃতি উদ্ভূত করে, অথবা না করে, এবং বিশ্বাসের ফলাফলটিতে কোন প্রভাব নেই ।
একটি আনুষ্ঠানিক প্রমাণের নকল করার সাধারণ পদ্ধতি পরীক্ষা করা হয় এবং প্রত্যাখ্যান করা হয়। একটি প্রমাণ যা sorry-এর সাথে একটি গর্ত ছেড়ে দেয়, একটি যা native_decide-কে আবেদন করে কার্নেলকে বিশ্বাসের উপর একটি গণনা গ্রহণ করতে, অথবা একটি যা নিঃশব্দে একটি নতুন স্বতন্ত্রতা প্রবর্তন করে, সনাক্ত করা হয় এবং সফল হিসাবে গণনা করার পরিবর্তে প্রত্যাখ্যান করা হয়।
প্যানেলটি আসলে কি করতে পারে
বিতর্ক করা সস্তা অংশ। প্যানেল সাহিত্যের সাথে কাজ করে - arXiv, OpenAlex, Crossref - তাই একটি পরিচিত ফলাফলকে উদ্ধৃত করা হয় না খারাপভাবে পুনরায় উদ্ভূত করার পরিবর্তে। এটি SageMath এবং PARI/GP গণনা করার জন্য, Z3 এবং CVC5 SMT সমাধানের জন্য, OEIS অনুসন্ধান করার জন্য একটি ধারা যা এটি নির্মাণ করেছে তা চিহ্নিত করার জন্য, এবং একটি sandboxed পাইথন পরিবেশ কোন নেটওয়ার্ক অ্যাক্সেস ছাড়া। কেউ এটি প্রমাণ করার চেষ্টা করার আগে একটি অনুমান দশ হাজার ক্ষেত্রে পরীক্ষা করা যেতে পারে, এবং একটি প্রতিউদাহরণ আলোচনার অবিলম্বে শেষ করে।
প্রমাণ, উক্তি নয়
A match is not scored on argument quality. The claim is decomposed into acceptance criteria, and a criterion is only settled when something behind it can be re-checked by a third party: a source with the relevant passage quoted, or code that was actually executed with its real output. The referee re-checks that evidence itself before ruling, and it cannot declare the match finished while a criterion is still open.
তুমিই বাঁধ সাজাও
মান আপনার বেছে নেওয়া, আর রেফারি তা আক্ষরিক অর্থে ধরে রাখে। একজন সতর্ক বিশেষজ্ঞ যা গ্রহণ করবে তা জিজ্ঞেস করুন আর আপনি তা পাবেন। প্রতিটি ধারণার সাথে একটি সম্পূর্ণ যুক্তি জিজ্ঞেস করুন আর এর পরিবর্তে আপনি তার বিরুদ্ধে বিচার পেতে পারেন। পুরস্কার প্রদান করা প্রতিযোগিতার বার জিজ্ঞেস করুন, আর সৎ ফলাফল সাধারণত একটি সঠিক ব্যাখ্যা যেখানে প্যানেল কম ছিল - যা একটি আত্মবিশ্বাসী দাবির চেয়ে বেশি মূল্যবান যা আপনাকে যে কোনভাবেই হোক নিজেকে পরীক্ষা করতে হবে।
এটার ব্যাপারে পরিষ্কারভাবে বলতে গেলে: এটি এমন একটি মেশিন নয় যা উন্মুক্ত সমস্যা সমাধান করে। এটি এমন একটি মেশিন যা একটি যুক্তিকে সমাধান হিসাবে পাস করতে অস্বীকার করে যখন তা না হয়, এবং যা আপনাকে ঠিক কোন পদক্ষেপ ব্যর্থ হয়েছে তা বলে।
একটি ব্যর্থ ফরমালাইজেশন হল ব্যবহারযোগ্য আউটপুট
যখন লিন প্রমাণ বন্ধ করে না, তখন আপনি ঠিক সেই লক্ষ্যটা পাবেন যা বাকি আছে। প্রয়োগে প্রায় সব সময়ই এই জায়গাটাতে অপ্রকাশিত যুক্তি হাত বাড়িয়ে দেয়ার জায়গা হয়ে থাকে - যে পদক্ষেপটি প্রত্যেকে পদ্য সংস্করণ পড়ে গিয়ে ঘাড় ঝুঁকিয়ে দিয়েছে। এই লক্ষ্যটা তখন যে কোন আসনে দেয়া হয় যেখানে সেটা আক্রমণ করার জন্য সবচেয়ে ভালো অবস্থান, যা আগে থেকেই চেষ্টা করা হয়েছে, আর আর কিছু নয়। মডেলরা যখন আটকে পড়ে তখন ঝাঁপিয়ে পড়ে, নিজেদেরকে সম্পূর্ণ খরচে পুনরায় প্রকাশ করে; এর পরিবর্তে একটা নির্দিষ্ট প্রশ্ন পাস করা সাধারণত টোকেনের একটা অংশের জন্য ব্লক খুলে দেয়।
দীর্ঘ কাজ বেঁচে থাকে
Every lemma the panel establishes goes into a shared ledger with its proof, so results are written once and never re-derived, and dead ends are recorded so nobody walks back into them. Matches run server-side and pause cleanly — on budget, on a provider outage, or because you closed the tab — and resume exactly where they stopped.
এটা কিসের জন্য নয়
প্রমিত একটি নিরপেক্ষ শব্দ। এই সাইটটি গণিত, যুক্তি, তাত্ত্বিক কম্পিউটার বিজ্ঞান, তাত্ত্বিক পদার্থবিজ্ঞান এবং অর্থনৈতিক তত্ত্বের জন্য তৈরি করা হয়েছে - যেখানে একটি দাবি প্রমাণের মাধ্যমে সমাধান করা হয়। জীববিজ্ঞান, চিকিৎসা, রসায়ন বা সামাজিক বিজ্ঞানের অভিজ্ঞতাগত প্রশ্ন প্রমিত তৈরি করে না, তারা আবিষ্কার তৈরি করে, এবং কোন পরিমাণ সরকারিকরণের মাধ্যমে তাদের সিদ্ধান্ত নেওয়া যাবে না। আমাদের ভাই সাইট referee.chat একই প্যানেল-এন্ড-রিফার প্রক্রিয়া চালায়, লিন পদক্ষেপ ছাড়া, ঠিক সেই প্রশ্নগুলোর জন্য।