Condizioni di servizio
1. Cosa fa il servizio
Lei presenta un reclamo e uno standard. Lo facciamo passare attraverso un pannello di modelli AI che si seleziona, più un modello arbitro che regola i criteri di accettazione, e cerchiamo di formalizzare il risultato in Lean 4 contro Mathlib. L'output è una trascrizione, una serie di sentenze, un verdetto, e dove è stata tentata la formalizzazione, il risultato Lean.
2. Che cosa l'uscita è e non è
L'output è generato da modelli di AI di terze parti e non è un consiglio. Non è legale, medico, finanziario, ingegneristico o consulenza professionale di qualsiasi tipo, e nessun rapporto professionale viene creato utilizzando questo servizio.
L'arbitro che decide un criterio soddisfatto è una dichiarazione circa le prove in archivio in quel match. Non è una garanzia di correttezza. I modelli AI fanno errori, le fonti di lettura errata, e possono fabbricare citazioni nonostante le istruzioni di non. È necessario verificare indipendentemente qualsiasi cosa si intende fare affidamento su, in particolare prima di pubblicarlo, di presentarlo o di agire su di esso. Si tratta di uno strumento per il lavoro di prova di pressione, non un sostituto per la revisione umana qualificata.
Una formalizzazione Lean riuscita significa che il kernel Lean ha accettato una prova della dichiarazione che era stata formalizzata, contro la versione di Mathlib in uso in quel momento. Non significa che la dichiarazione sia una traduzione fedele di ciò che hai chiesto, e scegliere una dichiarazione formale che non dice ciò che intendevi è il modo più comune in cui un risultato formale inganna. Leggere la dichiarazione formale, non solo il verdetto.
3. Il contenuto
Mantieni la proprietà dei crediti che sottoponi e dell'output prodotto per te. Ci concedi solo la licenza necessaria per gestire il servizio: per elaborare la tua presentazione, trasmetterla ai fornitori di modelli selezionati e memorizzare i risultati match in modo da poter tornare ad esso.
Matches sono privati per impostazione predefinita. Se segnate un pubblico match diventa visibile a chiunque abbia il link e può comparire nella nostra galleria pubblica. Non pubblicare un match contenente nulla di riservato.
Non inviare dati personali su altri, materiale riservato non hai il diritto di condividere o contenuti illegali.
4. Crediti e fatturazione
Il credito viene pagato in anticipo e consumato come matches run. Ogni match ha un limite di spesa impostato; raggiungendolo si ferma il match anziché continuare a spendere. I saldi non sono trasferibili e, salvo quanto previsto dalla legge, non sono rimborsabili una volta consumati. Il credito non utilizzato è rimborsabile su richiesta.
Se si collega la propria chiave di inferenza, si paga direttamente il fornitore e noi fatturano nessun costo per-token. Passato il previsto quota gratuita una tassa infrastruttura si applica per coprire l'esecuzione del pannello, strumenti e stoccaggio.
Possiamo cambiare i prezzi con preavviso. Le modifiche non si applicano mai al credito già acquistato.
5. Uso accettabile
Non utilizzare il servizio per generare contenuti che danneggiano gli altri, per cercare di estrarre i nostri suggerimenti o istruzioni di sistema, per aggirare i limiti di spesa o di tasso, o per rivendere l'accesso senza un accordo scritto. Lo strumento di esecuzione del codice è per verificare le richieste; non usarlo per attaccare qualsiasi sistema.
6. Disponibilità
Dipendiamo da fornitori di modelli di terze parti. I fornitori scendono, cambiano modelli e li deprecano. Un match interrotto per qualsiasi motivo è sospeso e riutilizzabile; non ci facciamo pagare per lavori che non sono avvenuti. Non garantiamo la disponibilità ininterrotta, e un modello che avete usato prima potrebbe diventare non disponibile.
7. Responsabilità
Nella misura massima consentita dalla legge, il servizio viene prestato come senza garanzie di alcun tipo. La nostra responsabilità totale per qualsiasi reclamo è limitata all'importo che ci hai pagato nei tre mesi precedenti la richiesta. Non siamo responsabili per perdite indirette o conseguenti, incluse eventuali perdite derivanti dalla dipendenza dal modello di output.
8. Denuncia
L'utente può chiudere il proprio account in qualsiasi momento; noi rimborseremo il credito non utilizzato. Possiamo sospendere i conti che violano questi termini o che mettono il servizio a rischio.
9. Modifiche, lingua e contatto
Possiamo aggiornare questi termini; modifiche materiali saranno annunciate sul sito.
Le traduzioni di questa pagina sono fornite per comodità e sono prodotte in macchina. Se una traduzione e la versione inglese differiscono, la versione inglese governa.
Domande: Contattaci.