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.
بۆچی کەرێکی تر و نە مۆدێلێکی تر
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.
چی هەیە لە ڕاستیدا پانێلەکە بیکات
وتووێژ کردن بەشێکی گرانە. ئەم پانێلە لەگەڵ کتێبەکاندا کاردەکات - arXiv، ئۆپن ئەلێکس، کرۆسڕێف - بۆیە ئەنجامێکی ناسراو ئاماژە پێ دەکرێت نەک بە خراپ. SageMath و PARI/GP بۆ حسابکردن هەیە، Z3 و CVC5 بۆ چارەسەرکردنی SMT، OEIS بۆ دۆزینەوەی زنجیرەیەک کە دروستی کردووە، و ژینگەی پیتۆنێکی تەنکی کە هیچ پەیوەندییەکی نەماوە. دەتوانرێت گێڕانەوەیەک تاقی بکرێتەوە لە بەرامبەر دە هەزار حاڵەتدا پێش ئەوەی کەسێک هەوڵ بدات بسەلمێنێت، وە نمونەیەکی دژ بە ئەوە بە خێرایی کۆتایی بە گفتوگۆکە دێت.
بەڵگە، نەک قسەکردن
گرێبەستێک لەسەر بایەخی گێڕانەوەکان نادرێت. داواکە دابەش دەکرێت بۆ مەرجەکانی قبوڵکردن، وە مەرجێک تەنها کاتێک چارەسەر دەکرێت کە شتێکی پشتەوەی بتوانرێت تاقی بکرێتەوە لەلایەن سێیەم کەسەوە: سەرچاوەیەک لەگەڵ بڕگە پەیوەندیدارەکان کە باسکراوە، یان کۆدێک کە بەڕاستی ئەنجامدراوە لەگەڵ دەرکەوتنی ڕاستەقینەی. دادوەر ئەو بەڵگەیە تاقی دەکاتەوە پێش ئەوەی بڕیار بدات، و ناتوانێ گرێبەستەکە تەواو بکات کاتێک مەرجەکە هێشتا کراوەیە.
تۆ ڕیزبەندیت دیاری کرد
ستانداردەکە بۆ خۆت هەڵدەبژێریت، وە دادوەرەکە بە واتایەکی ڕاستەوخۆ دەیگرێت. پرسیار بکە بۆ ئەوەی کە شارەزایەکی ئاگادار قبوڵی بکات و ئەوەت پێدەدرێت. پرسیار بکە بۆ گێڕانەوەی تەواو لەگەڵ هەموو پێشبینییەکدا کە باسکراوە و تۆ لە جیاتی ئەوە دادوەر دەبی. پرسیار بکە بۆ ئەو بارەی کە خەڵاتەکە ڕووبەڕووی دەبێتەوە، و ئەنجامی ڕاستەقینە بە شێوەیەکی گشتی حسابێکی ڕاستەقینەیە بۆ ئەوەی کە پانێلەکە چەند کورت بوو - کە زیاتر لە داواکارییەکی متمانەپێکراو کە دەبێت بە هەر شێوەیەک بێت خۆت تاقی بکەیتەوە.
بۆ ئەوەی ڕوون بێت دەربارەی ئەوە: ئەمە ئامێرێک نیە کە کێشەی کراوە چارەسەر بکات. ئەمە ئامێرێکە کە ڕەت دەکاتەوە کە بڵێت گفتوگۆیەک بە شێوەیەکی چارەسەرکراو تێپەڕ دەبێت کاتێک کە ناکرێت و ئەوە بەڕاستی پێت دەڵێت کە کام هەنگاو شکستی هێناوە.
شێواندنی شکستخواردوو دەرکەوتنێکی بەکارهێنەرانە
کاتێک کە لیەن بەڵگە نەدەکاتەوە، ئامانجی ڕاستەقینە بەدەست دەهێنیت کە ماوەتەوە. لە کرداردا ئەوە نزیکەی هەمیشە ئەو شوێنەیە کە باسەکە بە بێ بنەما بوو کە دەست دەجوڵێت - هەنگاوەکە هەموو کەسێک کە وەرگێڕانی شیعری دەخوێنێتەوە بە سەرنجەوە تێدەپەڕێت. ئەو ئامانجە پاشان دەدرێت بە هەر شوێنێک کە باشترین شوێنە بۆ هێرشکردنە سەر، لەگەڵ ئەوەی کە پێشتر تاقیکراوەتەوە، هیچی تر. مۆدێلەکان کاتێک گیر دەبن، خۆیان بە تەواوی نرخەکە دەگێڕنەوە؛ تێپەڕاندنی پرسیارێکی تایبەت لە جیاتی ئەوە بە شێوەیەکی ئاسایی بۆ بەشێک لە تیکەکان بەستراوەتەوە.
کارێکی درێژ ژیانێکی درێژی هەیە
هەر لۆمایەک کە پانێلەکە دادەنێت دەچێتە ناو پەڕەیەکی هاوبەش لەگەڵ بەڵگەکەی، بۆیە ئەنجامەکان یەکجار دەنووسرێن و هەرگیز دووبارە نابنەوە، وە کۆتاییە بێماناکان تۆمار دەکرێن کەواتە کەس ناگەڕێتەوە بۆ ناویان. گرێدانەکان لەلای سەرپەرشتیاریدا دەڕۆن و بە پاکی ڕادەوەستن - لەسەر بودجە، لەسەر دابینکەرێک کە وەستاوە، یان لەبەرئەوەی پەڕەکەت داخست - وە بەردەوام دەبن لەوێدا کە ڕایانگرتبوو.
ئەمە بۆ چی نیە
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.