Termini tas-Servizz

Theorem.chat huwa operat minn Muddy Holdings LLC (aħna, us). Billi tuża s-servizz inti taqbel ma dawn it-termini.

1. X’jagħmel is-servizz

Inti tissottometti pretensjoni u standard. Aħna run dan minn panel ta AI mudelli inti tagħżel, flimkien ma mudell referee li regoli dwar kriterji ta’ aċċettazzjoni, u aħna jippruvaw jifformalizzaw ir-riżultat fil Lean 4 kontra Mathlib. Il-produzzjoni hija transkript, sett ta’ deċiżjonijiet, verdict, u fejn formalizzazzjoni kien tentattiv, ir-riżultat Lean.

2. X'inhu l-output u mhux

Ir-riżultat huwa ġġenerat minn mudelli tal-AI ta' partijiet terzi u mhuwiex parir. Dan mhuwiex parir legali, mediku, finanzjarju, inġinerija jew professjonali ta' kwalunkwe tip, u l-ebda relazzjoni professjonali ma tinħoloq bl-użu ta' dan is-servizz.

Ir-referee li jiddeċiedi li kriterju ġie ssodisfat huwa dikjarazzjoni dwar l-evidenza fuq ir-rekord f'dik il-logħba, iżda mhux garanzija ta' korrettezza. Il-mudelli tal-AI jagħmlu żbalji, jaqraw is-sorsi ħażin, u jistgħu jiffalsifikaw ċitazzjonijiet minkejja l-istruzzjonijiet biex ma jagħmlux dan. Għandek tivverifika b'mod indipendenti kull ma inti beħsiebek tistrieħ fuquDin hija għodda għall-ittestjar tal-pressjoni tax-xogħol, mhux sostitut għal reviżjoni umana kkwalifikata, u għalhekk ma tistax tissostitwixxi l-evalwazzjoni tal-kwalità tal-kontenut.

Formalizzazzjoni Lean b'suċċess tfisser li l-kernel Lean aċċetta prova tal-istqarrija li ġiet formalizzata, kontra l-verżjoni ta' Mathlib fl-użu f'dak iż-żmien. Dan ma jfissirx li dik l-istqarrija hija traduzzjoni fidila ta' dak li inti staqsejt, u l-għażla ta' dikjarazzjoni formali li ma jgħidx dak li inti tfisser huwa l-aktar mod komuni riżultat formali jiżgwida. Aqra l-istqarrija formali, mhux biss il-verdict.

3. Il-kontenut tiegħek

Inti żżomm is-sjieda tal-pretensjonijiet li tissottometti u tal-output prodott għalik. Inti tagħtina biss il-liċenzja meħtieġa biex topera s-servizz: biex tipproċessa s-sottomissjoni tiegħek, tittrasmettiha lill-fornituri tal-mudell li għażilt, u taħżen it-tqabbil li jirriżulta sabiex tkun tista' terġa' lura għalih.

Il-partiti huma privati b'mod awtomatiku. Jekk timmarka partita pubblika, din issir viżibbli għal kull min għandu l-link u tista' tidher fil-gallerija pubblika tagħna. Tpoġġix partita li fiha xi ħaġa kunfidenzjali.

Ma tissottomettix data personali dwar oħrajn, materjal kunfidenzjali li m'għandekx id-dritt taqsam, jew kontenut li huwa illegali.

4. Krediti u fatturazzjoni

Il-kreditu huwa mħallas minn qabel u jiġi kkunsmat hekk kif il-logħob isir. Kull logħba għandha limitu ta' nfiq li inti tistabbilixxi; meta tilħaq dan il-limitu, il-logħba titwaqqaf minflok ma tkompli tintefaq. Il-bilanċi mhumiex trasferibbli u, ħlief fejn meħtieġ mil-liġi, ma jistgħux jiġu rimborżati ladarba jiġu kkunsmati.

Jekk tikkonnettja l-inference key tiegħek, inti tħallas lill-fornitur tiegħek direttament u aħna ma niċċarġjawx għal kull token.Minn fuq l-allokazzjoni bla ħlas iddikjarata, tapplika tariffa tal-infrastruttura biex tkopri t-tħaddim tal-pannell, l-għodod u l-ħażna.

Nistgħu nbiddlu l-prezzijiet b'avviż. Il-bidliet qatt ma japplikaw għal kreditu diġà mixtri.

5. Użu aċċettabbli

Tużax is-servizz biex tiġġenera kontenut li jagħmel ħsara lil oħrajn, biex tipprova testraċċa l-istruzzjonijiet tas-sistema jew il-prompts tagħna, biex tevita l-limiti tal-infiq jew tar-rata, jew biex terġa' tbigħ l-aċċess mingħajr ftehim bil-miktub.L-għodda tal-eżekuzzjoni tal-kodiċi hija għall-verifika tat-talbiet; tużahx biex tattakkaw xi sistema.

6. Disponibbiltà

Aħna jiddependu fuq fornituri mudelli partijiet terzi. Fornituri jaqgħu, jibdlu mudelli, u obsoleti minnhom. Match interrott għal kwalunkwe raġuni hija sospiża u jistgħu jerġgħu jibdew; aħna ma jiċċarġjaw għal xogħol li ma ġara. Aħna ma jiggarantixxu d-disponibbiltà mingħajr interruzzjoni, u mudell inti użat qabel jistgħu jsiru mhux disponibbli.

7. Responsabbiltà

Sal-limitu massimu permess mil-liġi, is-servizz huwa pprovdut kif inhu mingħajr garanziji ta’ kwalunkwe tip. Ir-responsabbiltà totali tagħna għal kwalunkwe pretensjoni hija limitata għall-ammont li inti ħallast lilna fit-tliet xhur qabel il-pretensjoni tqajmet. Aħna m’aħniex responsabbli għal telf indirett jew konsegwenti, inkluż kwalunkwe telf li jirriżulta minn dipendenza fuq il-produzzjoni tal-mudell.

Terminazzjoni

Tista' tagħlaq il-kont tiegħek fi kwalunkwe ħin; aħna nirrifużaw il-kreditu mhux użat.Nistgħu nissospendu kontijiet li jiksru dawn it-termini jew li jqiegħdu s-servizz f'riskju.

9. Bidliet, lingwa u kuntatt

Nistgħu naġġornaw dawn it-termini; bidliet materjali se jiġu mħabbra fuq is-sit.

It-traduzzjonijiet ta' din il-paġna huma pprovduti għall-konvenjenza u huma prodotti mill-magni.Fejn traduzzjoni u l-verżjoni bl-Ingliż ivarjaw, il-verżjoni bl-Ingliż tiggverna.

Mistoqsijiet: Ikkuntattjana issa.