O Theorem.chat
Theorem.chat berie matematické tvrdenie a snaží sa ho vyriešiť. Vy vyjadríte tvrdenie a štandard, ktorý musí spĺňať. Panel modelov AI – koľko len chcete, od akéhokoľvek dodávateľa – ho napadne a ešte jeden model ho posudí. Potom sa argument formalizuje v Lean 4 proti Mathlib a Lean kernel rozhodne, či je dokázateľný. Posledným krokom je produkt.
Prečo jadro, a nie iný model
Spýtajte sa modelu na ťažkú otázku a dostanete plynulú odpoveď, či je správna alebo nie. Spýtajte sa viacerých a často sa zhodnú, čo sa zdá ako potvrdenie, ale nie je: modely zdieľajú tréningové dáta a zdieľajú slepé miesta. Druhý model kontrolujúci prvý je stále rovnaký druh úsudku a dá sa o ňom hovoriť. Lean kernel nemôže. Buď odvodí výrok z axióm a Mathlib, alebo nie a dôvera nemá žiadny vplyv na výsledok.
Dôkaz, ktorý zanecháva dieru v sorry, dôkaz, ktorý apeluje na native_decide, aby jadro prijalo výpočet na základe dôvery, alebo dôkaz, ktorý ticho zavádza novú axiómu, je detekovaný a odmietnutý namiesto toho, aby bol považovaný za úspešný.
Čo panel skutočne dokáže
Panel pracuje s literatúrou – arXiv, OpenAlex, Crossref – takže známy výsledok je citovaný skôr ako zle odvodený. Má SageMath a PARI/GP pre výpočet, Z3 a CVC5 pre riešenie SMT, OEIS pre vyhľadávanie pre identifikáciu sekvencie, ktorú vytvoril, a sandboxové prostredie Pythonu bez prístupu k sieti. Domnienku možno otestovať proti desiatim tisícom prípadov skôr, ako sa niekto pokúsi o jej dokázanie, a protipríklad okamžite ukončí diskusiu.
Dôkaz, nie výrečnosť
Súboj nie je hodnotený na základe kvality argumentu, tvrdenie je rozdelené na akceptačné kritériá a kritérium je vyriešené len vtedy, keď niečo za ním môže byť znovu overené treťou stranou: zdroj s citovanou relevantnou pasážou, alebo kód, ktorý bol skutočne vykonaný s jeho skutočným výstupom. Rozhodca znovu skontroluje tento dôkaz sám pred rozhodnutím a nemôže vyhlásiť súboj za ukončený, kým je kritérium stále otvorené.
Nastavila si latku
Štandard je na vás, aby ste si vybrali a rozhodca to drží doslovne. Požiadajte o to, čo by starostlivý odborník prijal a dostanete to. Požiadajte o úplný deduktívny argument s každým uvedeným predpokladom a namiesto toho budete posudzovaný podľa toho. Požiadajte o bar, ktorému by čelila cena, a čestný výsledok je zvyčajne presný výpočet, kde panel nedosiahol - čo stojí viac ako sebavedomé tvrdenie, ktoré by ste si museli skontrolovať sami.
Aby sme to vysvetlili jasne: toto nie je stroj, ktorý rieši otvorené problémy, je to stroj, ktorý odmieta argumentovať ako vyriešený, keď nie je, a ktorý vám presne povie, ktorý krok zlyhal.
Neúspešná formalizácia je užitočným výstupom
Keď Lean neuzavrie dôkaz, dostanete presný cieľ, ktorý zostáva. V praxi je to takmer vždy miesto, kde neformálny argument mával rukou - krok, ktorý každý, kto čítal prózu, by prikývol. Tento cieľ je potom odovzdaný na miesto, ktoré je najlepšie umiestnené na jeho napadnutie, spolu s tým, čo už bolo vyskúšané, a nič iné. Modely sa vrhnú, keď sa zaseknú, opätovne sa vysvetľujú za plnú cenu; zodpovedanie jednej konkrétnej otázky namiesto toho zvyčajne odblokuje za zlomok žetónov.
Dlhá práca prežije
Každé lemma, ktoré panel vytvorí, sa dostane do zdieľanej knihy s dôkazom, takže výsledky sa zapíšu raz a nikdy sa neodvodia znova a slepé uličky sa zaznamenajú, takže sa nikto nevráti späť.Zodpovedajúce zápasy bežia na strane servera a sú čisto pozastavené - na rozpočet, na výpadok poskytovateľa alebo preto, že ste zatvorili kartu - a pokračujú presne tam, kde skončili.
Na čo to nie je určené
Táto stránka je vytvorená pre matematiku, logiku, teoretickú informatiku, teoretickú fyziku a ekonomickú teóriu – oblasti, kde sa tvrdenie vyrovná dôkazom. Empirické otázky v biológii, medicíne, chémii alebo spoločenských vedách nevytvárajú vety, vytvárajú zistenia a žiadne množstvo formalizácie ich nerozhodne. Naša sesterská stránka referee.chat prevádzkuje rovnaký proces panelu a referencie bez kroku Lean, presne pre tieto otázky.