Aproximativ Theorem.chat
Theorem.chat ia o cerere matematică și încearcă să o rezolvi. A se spune afirmația, și standardul pe care trebuie să-l îndeplinească. Un panou de modele de IA – câte vrei, de la orice vânzători doriți – atacă-l, și un alt arbitru model. Apoi argumentul este formalizat în Lean 4 împotriva Mathlib, iar nor Lean decide dacă este dovedit. Acest ultimul pas este produsul.
De ce un kernel, și nu un alt model
Întreabă mai multe și adesea sunt de acord, care se simte ca o corborare și nu este: modelele împărtășesc date de formare și împărtășesc puncte orbe. Un al doilea model care verifică primul este tot același tip de judecată, și poate fi discutat rotund. Nu se poate. Ori devine declarația de la axiome și Mathlib, ori nu, și încrederea nu are efect asupra rezultatului.
Modurile obişnuite de a falsifica o dovadă oficială sunt verificate şi refuzate. O dovadă care lasă o gaură cu sorry, care apelează la native_decide pentru a face că nurul ia un calcul pe încredere, sau unul care introduce în linişte un nou axiom, este detectat şi respins, mai degrabă decât numărat ca un succes.
Ce poate face panoul de fapt
Argumentul este partea ieftin. Panoul lucrează cu literatura — arXiv, OpenAlex, Crossref — deci un rezultat cunoscut este citat mai degrabă decât re-deridat rău. Are SageMath și PARI/GP pentru calcul, Z3 și CVC5 pentru soluționarea SMT, OEIS pentru identificarea unei secvențe pe care le-a construit, și un mediu Python fără sabbox fără acces la rețea. O conjectură poate fi testată împotriva zece mii de cazuri înainte ca cineva să petrecă o rundă încercând să-l dovedească, și un contraexemplu se termină imediat discuția.
Dovezi, nu elocvențe
Un match nu este marcat pe calitatea argumentelor. Susținerea este decompusă în criterii de acceptare, și un criteriu este stabilit doar atunci când ceva din spatele acestuia poate fi re-controlat de o terță parte: o sursă cu pasajul relevant citat, sau codul care a fost de fapt executat cu rezultatul său real. Arbitrul verifică de fapt că dovezi în sine înainte de a decide, și nu poate declara match terminat în timp ce un criteriu este încă deschis.
Ai set bar
Standardul este al tău de a alege, iar arbitrul o deține literalmente. Întreabă pentru ce un expert atent ar accepta și obține asta. Întreabă pentru un argument deductiv complet cu fiecare presupunere declarată și te va fi judecat împotriva că. Întreabă pentru bar o supunere de premiu ar face față, și rezultatul sincer este de obicei un cont precis despre unde panoul a căzut – care merită mai mult decât o afirmație încrezătoare ar trebui să te verifice oricum.
Pentru a fi clar despre el: aceasta nu este o maşină care rezolvă problemele deschise. Este o maşină care refuză să lase un argument să treacă ca stabilit atunci când nu este, și care vă spune exact ce pas eșuat.
O formalizare eșuată este rezultatul util
Când Lean nu va închide dovada, vei obţine scopul exact care rămâne. În practică, acesta este aproape întotdeauna locul în care argumentul informal a fost de a leagă la mână – pasul oricine citi versiunea prose ar fi dat în pat trecut. Acest obiectiv este apoi predat la orice loc este cel mai bine plasat pentru atac, împreună cu ceea ce a fost deja încercat, și nimic altceva. Modelele când sunt blocate, se reafirmă la costul complet; trece o întrebare specifică în schimb de obicei deblocare pentru o fracție de jet.
Munca lungă supravieţuieşte
Fiecare lemma care stabilește panoul intră într-un ghid comun cu dovezile sale, așa că rezultatele sunt scrise o dată și nu se re-deruie, și se înregistrează capetele moarte astfel încât nimeni nu se întoarce în ele. Matches rulează pe partea server- și se oprește curat — pe buget, pe o depășire a furnizorului, sau pentru că ați închis tab – și relua exact unde s-au oprit.
Ce nu este pentru asta
Theorem este un cuvânt deductiv. Acest site este construit pentru matematică, logică, teoretică informatică, fizică teoretică și teorie economică – domenii în care o cerere este stabilită prin dovada. Întrebări empirice în biologie, medicina, chimie sau științe sociale nu produc teoreme, acestea produc descoperiri, și nici o cantitate de formalizare le va decide. site-ul surorii noastre referee.chat execută același proces de panouri și de referință fără pasul Lean, pentru exact aceste întrebări.