Околу Theorem.chat
Theorem.chat зема математичко тврдење и се обидува да го реши тоа. Вие го наведувате тврдењето и стандардот што мора да го исполни. Paneл на модели на ВИ — колку што сакате, од кој и да е продавач — го напаѓа и уште еден модел судија. Потоа аргументот е формализиран во Lean 4 против Mathlib, а јадрото на линијата одлучува дали е докажано.
Зошто кернел, а не друг модел
Поставете макета тешко прашање и добивате течен одговор дали е исправно. Прашајте неколку и тие често се согласуваат, што е како потврда и не е: моделите ги споделуваат податоците за обука и споделуваат слепи точки. Вториот модел за проверка на првиот е ист вид на пресуда, и може да се зборува круг. Лиано јадрото не може. Или ја добива изјавата од аксиомите и Mathlib или не, и самодовербата нема ефект на исходот.
Доказот што остава дупка со sorry, еден што се повикува на native_decide да се натера кернелот да земе пресметање на довербата, или оној што тивко воведува нов аксиом, се открива и отфрла наместо да се смета за успех.
Што всушност може да направи панелот
Расправањето е евтин дел. Панелата работи со литературата — arXiv, OpenAlex, Crossref — така што познатиот резултат е наведен наместо лошо. Таа има SageMath и PARI/GP за пресметување, Z3 и CVC5 за решавање на SMT, OEIS барање за идентифицирање на секвенца што ја изградила, и питонска средина без пристап на мрежата. Нагаѓање може да се тестира против десет илјади случаи пред некој да потроши круг обиди да го докаже, и контрапример завршува разговорот веднаш.
Доказ, не елоквенција
А match не се добиваат на квалитет на аргументите. Тврдењето се распаѓа во критериумите за прифаќање, а критериумот се решава само кога нешто зад него може да биде повторно проверено од страна на трета страна: извор со релевантниот пасус цитиран или код кој е всушност извршен со неговото реално производство. Судијата повторно го проверува самиот доказ пред одлуката, и не може да го прогласи за завршено match додека критериумот е сé уште отворен.
Ти го постави барот.
Прашај што би прифатил еден внимателен експерт и го добиваш тоа.
Да бидеме јасни: ова не е машина која решава отворени проблеми туку машина која одбива да дозволи аргументот да поминат како решен кога не е, и тоа ви кажува кој чекор точно не успеа.
Неуспешната формализација е корисен излез
Кога Лиан нема да го затвори доказот, ќе ја добиете точната цел која останува. Во практика тоа е речиси секогаш местото каде што неформалниот аргумент се фрлаше рачно — чекорот кој секој што го читаше верзијата на прозата ќе го кима минатото. Тогаш таа цел е предадена на кое место е најдобро да се нападне, заедно со она што веќе е испробано, и ништо друго. Моделите се стиснат кога се заглавија, се реставрираат себеси по целосна цена; поминуваат едно конкретно прашање наместо тоа, обично се одблокираат за дел од жетоните.
Долга работа преживеа
Секоја лема што ја поставува панелот оди во заедничка книга со нејзиниот доказ, така резултатите се запишани еднаш и никогаш не се повторуваат, и ќорсокакот се снимаат така што никој не се враќа назад во нив. Matches трчајте на серверот и паузирајте чисто — на буџетот, на провајдерски прекин, или затоа што го затворивте ливчето — и продолжите точно каде што застанаале.
Зошто не е ова?
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.