حدود 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.
چرا یک هسته، نه یک مدل دیگر
Ask a model a hard question and you get a fluent answer whether or not it is right. Ask several and they often agree, which feels like corroboration and is not: models share training data and share blind spots. A second model checking the first is still the same kind of judgement, and it can be talked round. The Lean kernel cannot. It either derives the statement from the axioms and Mathlib, or it does not, and confidence has no effect on the outcome.
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.