حدود Theorem.chat
Theorem.chat یک ادعای ریاضی را می‌گیرد و سعی می‌کند آن را حل کند. شما ادعا را بیان می‌کنید و استانداردی که باید برآورده کند. یک گروه از مدل‌های هوش مصنوعی — هرچند که شما بخواهید ، از هر فروشنده‌ای که بخواهید — به آن حمله می‌کند ، و یک داور مدل بیشتر. سپس استدلال در Lean 4 در برابر Mathlib رسمی می‌شود ، و هسته Lean تصمیم می‌گیرد که آیا اثبات شده است یا نه. آن گام آخر محصول است.
چرا یک هسته، نه یک مدل دیگر
از یک مدل یک سوال سخت بپرسید و پاسخی روان دریافت می‌کنید که درست است یا نه. از چند نفر بپرسید و اغلب آنها موافقت می‌کنند، که احساس تأیید می‌شود و نیست: مدل‌ها داده‌های آموزشی را به اشتراک می‌گذارند و نقاط کور را به اشتراک می‌گذارند. یک مدل دوم که اولین را چک می‌کند هنوز همان نوع قضاوت است، و می‌تواند در اطراف صحبت کند. هسته Lean نمی‌تواند. یا این که جمله را از اصول و Mathlib بدست می‌آورد، یا این که نمی‌آورد، و اعتماد هیچ تأثیری بر نتیجه ندارد.
روش‌های معمول برای ساختن اثبات رسمی بررسی و رد می‌شوند. اثباتی که یک حفره در sorry ایجاد می‌کند، یا به native_decide مراجعه می‌کند تا باعث شود هسته یک محاسبات بر اساس اعتماد انجام دهد، یا به صورت خاموش یک اصل موضوع جدید را معرفی می‌کند، شناسایی و رد می‌شود و به جای آن به عنوان موفقیت در نظر گرفته می‌شود.
چيزايي که اين پنل مي تونه انجام بده
بحث بخش ارزان است. این پنل با ادبیات کار می‌کند - arXiv، OpenAlex، Crossref - بنابراین یک نتیجه شناخته شده به جای بدست آوردن بدست آمده است. این SageMath و PARI/GP برای محاسبه، Z3 و CVC5 برای حل SMT، OEIS Lookup برای شناسایی یک دنباله که ساخته شده است، و یک محیط sandboxed Python بدون دسترسی به شبکه دارد. یک حدس می‌تواند در برابر ده هزار مورد قبل از اینکه کسی یک دور را صرف تلاش برای اثبات آن کند، آزمایش شود، و یک مثال مخالف بحث را بلافاصله به پایان می‌رساند.
شواهد، نه فصاحت
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 همان فرایند پانل و داور را بدون گام Lean، دقیقاً برای آن سوالات اجرا می‌کند.