Um Theorem.chat
Theorem.chat tekur stærðfræðilega fullyrðingu og reynir að sætta sig við hana. Þú segir kröfuna og staðalinn sem hún þarf að uppfylla. Panel AI líkana - eins mörg og þú vilt, frá hvaða söluaðilum sem þú vilt - árásir það, og einn fleiri líkan dómarar. Síðan er röksemdin formlega í Lean 4 gegn Mathlib, og Lean kjarna ákveður hvort það er sannað. Það síðasta skref er afurðin.
Hvers vegna kjarna, og ekki annað líkan
Spurðu líkan erfiða spurningu og þú færð fljótt svar hvort það sé rétt eða ekki. Spurðu nokkra og þeir eru oft sammála, sem líður eins og staðfesting og er ekki: líkön deila þjálfunargögnum og deila blindum blettum. Annað líkan sem athugar fyrsta er enn sama tegund dóms og það er hægt að tala um það. Lean kjarninn getur það ekki. Hann annað hvort dregur fullyrðingu frá axioms og Mathlib, eða það gerir það ekki, og traust hefur engin áhrif á niðurstöðuna.
Sönnun sem skilur eftir sig gat í sorry, sönnun sem krefst þess að native_decide geti gert kjarnann að taka útreikninga á trausti, eða sönnun sem hljóðlega kynnir nýja axiom, er greind og hafnað frekar en að teljast sem árangur.
Hvað spjaldið getur í raun gert
Ræður eru ódýrasti hlutinn. Panelið vinnur með bókmenntum - arXiv, OpenAlex, Crossref - þannig að þekkt niðurstaða er vitnað frekar en endur-afleidd illa. Það hefur SageMath og PARI/GP fyrir útreikning, Z3 og CVC5 fyrir SMT lausn, OEIS leit til að bera kennsl á röð sem það hefur smíðað, og sandboxed Python umhverfi án nettengingar. Hægt er að prófa tilgátu gegn tíu þúsund tilvikum áður en einhver eyðir umferð til að reyna að sanna það, og mótdæmi lýkur umræðunni strax.
Sönnunargögn, ekki mælsku
Samsvörun er ekki metin út frá gæði röksemda. Ákvörðun er skipt niður í viðurkenningarviðmið og viðmið er aðeins ákveðið þegar hægt er að endurskoða eitthvað á bak við það af þriðja aðila: heimild með viðeigandi kafla vitnað í, eða kóða sem var raunverulega framkvæmt með raunverulegu úttaki. Dómarinn endurskoðar sönnunargögn sjálfur áður en hann dæmir, og getur ekki lýst samsvörun lokið meðan viðmið er enn opið.
Þú setur barnið
Staðalinn er þinn að velja, og dómarinn heldur það bókstaflega. Biðja um hvað varkár sérfræðingur myndi samþykkja og þú færð það. Biðja um fullkomna afleiðu rök með hverri forsendu sem fram kemur og þú færð dæmt gegn því í staðinn. Biðja um bar verðlaun framlag myndi standa frammi fyrir, og heiðarlegur niðurstaða er venjulega nákvæmar upplýsingar um hvar panel felldi stutt - sem er meira virði en öruggur krafa sem þú myndir þurfa að athuga sjálfur samt.
Til að vera skýr um það: þetta er ekki vél sem leysir opin vandamál.Það er vél sem neitar að láta röksemd fara sem leyst þegar það er ekki, og sem segir þér nákvæmlega hvaða skref mistókst.
A mistókst formgerð er gagnlegt framleiðsla
Þegar Lean mun ekki loka sönnun, þú færð nákvæmlega markmið sem eftir er. Í reynd er það nánast alltaf staðurinn þar sem óformleg rök var hand-veifa - skrefið allir lesa prósa útgáfa hefði hneigst framhjá. Það markmið er þá afhent til hvaða sæti er best staðsett til að ráðast á það, ásamt því sem hefur þegar verið reynt, og ekkert annað. Models thrash þegar þeir eru fastur, endurtaka sig á fullum kostnaði; fara framhjá einni tilteknu spurningu í staðinn opnar venjulega fyrir brot af táknum.
Long vinna lifir
Sérhver lemma sem spjaldið setur upp fer í sameiginlega bók með sönnun sinni, þannig að niðurstöður eru skrifaðar einu sinni og aldrei endurheimtar og blindgötur eru skráðar svo enginn gengur aftur í þær. Samsvörun keyrir á þjónshlið og gerir hlé á hreinu - á fjárhagsáætlun, á þjónustuveitanda eða vegna þess að þú lokaði flipanum - og heldur áfram nákvæmlega þar sem þeir hættu.
Hvað þetta er ekki fyrir
Þessi síða er byggð fyrir stærðfræði, rökfræði, fræðileg tölvunarfræði, fræðileg eðlisfræði og hagfræðikenningu - svið þar sem krafa er leyst með sönnun. Reynslubundnar spurningar í líffræði, læknisfræði, efnafræði eða félagsvísindum framleiða ekki setningu, þær framleiða niðurstöður og engin formleg ákvörðun mun ákveða þær. Systir okkar referee.chat rekur sama panel-og-dómstólaferli án Lean skrefið, fyrir nákvæmlega þessar spurningar.