Око 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.
Доказ, не елоквенција
А match није постигнуто на квалитету аргумента. Тврђење се распада у критеријуме прихватања, а критеријум се решава само када нешто иза њега може поново проверити трећа страна: извор са релевантним одласком цитираним, или код који је заправо извршен са правим излазом. Судија поново проверава да је доказ сам пре превладе, а не може прогласити да је match завршено док је критеријум још увек отворен.
Ти си поставио траку.
Стандард је на вама да изаберете, а судија га држи буквално. Питајте за оно што би пажљиви стручњак прихватио и добили то. Питајте за потпуну дедуктивну аргументу са сваком наведеном претпоставком и уместо тога вас процењују. Тражите бар за подношење награде, а поштени исход је обично прецизан налог о томе где панел није удаљен, што вреди више од самоувереног тврдње да ћете морати да проверите себе.
Да буде јасно: ово није машина која решава отворене проблеме, већ машина која одбија да прође као што је расправљано када није, а која вам говори тачно који корак није успео.
Пропала формализација је корисни излаз
Када Леан неће затворити доказ, добићете тачан циљ који остаје. У пракси, то је скоро увек место где је неформални аргумент ручно таласао — корак који сви читају верзију прозе би климнуо прошлошћу. Тај циљ се онда преда коме год седишту је најбоље помештено да га нападне, заједно са оним што је већ испробано, и ништа друго. Модели се тркају када се заглавили, реставрујући се по пуној цени; пролази једно посебно питање уместо тога, обично се одблокира за део жетона.
Дуг посао преживљава
Свака лема која се успостави улази у заједничку књигу са доказом, па резултати пишу једном и никада не буду поново нађени, и ћорсокак се снима тако да нико не улази у њих. Matches покрени сервер-страницу и паузирај чисто — на буџету, на провајдеру, или зато што сте затворили језичак - и настави тачно где су стајали.
Шта није за то?
Теорема је дедуктивна реч. Овај сајт је изграђен за математику, логику, теоретску компјутерску науку, теоретску физику и економску теорију — поља где тврдња решава доказом. Емпирична питања у биологији, медицини, хемији или друштвеним наукама не производе теореме, они доносе налаза, и никаква формализација неће их одлучити. Наша сестра сајт referee.chat води исти процес панела и рефереса без Лиан корака, за тачно та питања.