About Theorem.chat
Theorem.chat takes a mathematical claim and tries to settle it. You state the claim, and the standard it has to meet. A panel of AI models — as many as you want, from whichever vendors you want — attacks it, and one more model referees. Then the argument is formalised in Lean 4 against Mathlib, and the Lean kernel decides whether it is proved. That last step is the product.
কেন একটি কার্নেল, এবং অন্য মডেল না
একটি মডেলকে কঠিন প্রশ্ন জিজ্ঞেস করুন এবং আপনি একটি নিরপেক্ষ উত্তর পাবেন তা সঠিক কিনা তা জানতে । একাধিক প্রশ্ন জিজ্ঞেস করুন এবং তারা প্রায়শই একমত হবে, যা অনুমোদনের মত অনুভূত হয় এবং তা নয়: মডেলগুলি প্রশিক্ষণ তথ্য এবং অন্ধ স্থানের অংশীদারিত্ব ভাগ করে নেয় । প্রথমটি পরীক্ষা করে দ্বিতীয় মডেলটি এখনও একই ধরনের বিচার, এবং এটি ঘুরে বলা যেতে পারে । লিন কার্নেল পারে না । এটি হয়ত Mathlib এবং Mathlib থেকে বিবৃতি উদ্ভূত করে, অথবা না করে, এবং বিশ্বাসের ফলাফলটিতে কোন প্রভাব নেই ।
The usual ways to fake a formal proof are checked for and refused. A proof that leaves a hole with sorry, one that appeals to native_decide to make the kernel take a computation on trust, or one that quietly introduces a new axiom, is detected and rejected rather than counted as a success.
প্যানেলটি আসলে কি করতে পারে
Arguing is the cheap part. The panel works with the literature — arXiv, OpenAlex, Crossref — so a known result is cited rather than re-derived badly. It has SageMath and PARI/GP for computation, Z3 and CVC5 for SMT solving, OEIS lookup for identifying a sequence it has constructed, and a sandboxed Python environment with no network access. A conjecture can be tested against ten thousand cases before anyone spends a round trying to prove it, and a counterexample ends the discussion immediately.
প্রমাণ, উক্তি নয়
একটি ম্যাচ যুক্তিগত গুণগত মান দ্বারা স্কোর করা হয় না। দাবি গ্রহণযোগ্যতা মাপকাঠিতে বিভক্ত করা হয়, এবং একটি মাপকাঠি শুধুমাত্র তখনই নির্ধারিত হয় যখন এর পেছনে কিছু তৃতীয় পক্ষের দ্বারা পুনরায় পরীক্ষা করা যায়: একটি উৎস যেখানে সংশ্লিষ্ট অংশ উদ্ধৃত করা হয়, অথবা কোড যা বাস্তবে তার বাস্তব আউটপুট সহ চালানো হয়েছিল। রেফারি সিদ্ধান্ত নেওয়ার আগে প্রমাণ নিজেই পুনরায় পরীক্ষা করে, এবং এটি ম্যাচ শেষ ঘোষণা করতে পারে না যখন একটি মাপকাঠি এখনও খোলা আছে।
তুমিই বাঁধ সাজাও
মান আপনার বেছে নেওয়া, আর রেফারি তা আক্ষরিক অর্থে ধরে রাখে। একজন সতর্ক বিশেষজ্ঞ যা গ্রহণ করবে তা জিজ্ঞেস করুন আর আপনি তা পাবেন। প্রতিটি ধারণার সাথে একটি সম্পূর্ণ যুক্তি জিজ্ঞেস করুন আর এর পরিবর্তে আপনি তার বিরুদ্ধে বিচার পেতে পারেন। পুরস্কার প্রদান করা প্রতিযোগিতার বার জিজ্ঞেস করুন, আর সৎ ফলাফল সাধারণত একটি সঠিক ব্যাখ্যা যেখানে প্যানেল কম ছিল - যা একটি আত্মবিশ্বাসী দাবির চেয়ে বেশি মূল্যবান যা আপনাকে যে কোনভাবেই হোক নিজেকে পরীক্ষা করতে হবে।
এটার ব্যাপারে পরিষ্কারভাবে বলতে গেলে: এটি এমন একটি মেশিন নয় যা উন্মুক্ত সমস্যা সমাধান করে। এটি এমন একটি মেশিন যা একটি যুক্তিকে সমাধান হিসাবে পাস করতে অস্বীকার করে যখন তা না হয়, এবং যা আপনাকে ঠিক কোন পদক্ষেপ ব্যর্থ হয়েছে তা বলে।
একটি ব্যর্থ ফরমালাইজেশন হল ব্যবহারযোগ্য আউটপুট
যখন লিন প্রমাণ বন্ধ করে না, তখন আপনি ঠিক সেই লক্ষ্যটা পাবেন যা বাকি আছে। প্রয়োগে প্রায় সব সময়ই এই জায়গাটাতে অপ্রকাশিত যুক্তি হাত বাড়িয়ে দেয়ার জায়গা হয়ে থাকে - যে পদক্ষেপটি প্রত্যেকে পদ্য সংস্করণ পড়ে গিয়ে ঘাড় ঝুঁকিয়ে দিয়েছে। এই লক্ষ্যটা তখন যে কোন আসনে দেয়া হয় যেখানে সেটা আক্রমণ করার জন্য সবচেয়ে ভালো অবস্থান, যা আগে থেকেই চেষ্টা করা হয়েছে, আর আর কিছু নয়। মডেলরা যখন আটকে পড়ে তখন ঝাঁপিয়ে পড়ে, নিজেদেরকে সম্পূর্ণ খরচে পুনরায় প্রকাশ করে; এর পরিবর্তে একটা নির্দিষ্ট প্রশ্ন পাস করা সাধারণত টোকেনের একটা অংশের জন্য ব্লক খুলে দেয়।
দীর্ঘ কাজ বেঁচে থাকে
প্রতিটি ল্যামপা প্যানেল প্রতিষ্ঠিত একটি শেয়ারড লেজারে তার প্রমাণের সাথে যায়, তাই ফলাফল একবার লেখা হয় এবং কখনোই পুনরায় উদ্ভূত হয় না, এবং অন্ধকারের শেষ রেকর্ড করা হয় যাতে কেউ তাদের মধ্যে ফিরে যেতে পারে না। ম্যাচ সার্ভার-পাশে চলছে এবং পরিষ্কারভাবে স্থগিত হয় - বাজেট, প্রদানকারীর অকার্যকরতার কারণে, বা আপনি ট্যাব বন্ধ করে দিয়েছেন - এবং ঠিক যেখানে তারা থামে সেখানেই পুনরায় শুরু হয়।
এটা কিসের জন্য নয়
Theorem is a deductive word. This site is built for mathematics, logic, theoretical computer science, theoretical physics and economic theory — fields where a claim is settled by proof. Empirical questions in biology, medicine, chemistry or the social sciences do not produce theorems, they produce findings, and no amount of formalisation will decide them. Our sister site referee.chat runs the same panel-and-referee process without the Lean step, for exactly those questions.