Околу 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 или не, и самодовербата нема ефект на исходот.
Доказот што остава дупка со sorry, еден што се повикува на native_decide да се натера кернелот да земе пресметање на довербата, или оној што тивко воведува нов аксиом, се открива и отфрла наместо да се смета за успех.
Што всушност може да направи панелот
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.