Diensterme
1. Wat die diens doen
U stuur 'n eis en 'n standaard. Ons loop verby' n paneel van KI-modelle wat u kies, en 'n verwysingsmodel wat reëls oor aanvaarding kriteria bepaal, en ons probeer om die resultaat in Lean 4 teen Mathlib te verwoord. Die afvoer is 'n transkripsie,' n stel beslissings, 'n uitspraak en waar aformalisasie probeer is, die Lean resultaat.
2. Wat die afvoer is en nie is nie
Uitset word deur derde-part-KI modelle voortgebring en is nie advies nie. Dit is nie wettig, mediese, finansiële, ingenieurs - of professionele raad van enige aard nie, en geen professionele verhouding word deur middel van hierdie diens geskep nie.
The referee ruling a criterion met is a statement about the evidence on record in that match. It is not a guarantee of correctness. AI models make mistakes, misread sources, and can fabricate citations despite instructions not to. You must independently verify anything you intend to rely on, particularly before publishing it, submitting it, or acting on it. This is a tool for pressure-testing work, not a substitute for qualified human review.
'n Suksesvolle Lean formalisasie beteken dat die Lean kernel 'n bewys aanvaar het van die verklaring wat geformaliseer is, teen die weergawe van Mathlib in gebruik op daardie tyd. Dit beteken nie dat stelling 'n getroue vertaling is van wat jy gevra het nie, en kies' n formele verklaring wat nie sê wat jy bedoel het die algemeenste manier is om 'n formele resultaat mislei. Lees die formele verklaring, nie net die uitspraak nie.
3. Jou inhoud
You keep ownership of the claims you submit and of the output produced for you. You grant us only the licence needed to operate the service: to process your submission, transmit it to the model providers you selected, and store the resulting match so you can return to it.
Matches are private by default. If you mark a match public it becomes visible to anyone with the link and may appear in our public gallery. Do not publish a match containing anything confidential.
Moenie persoonlike gegewens oor ander, vertroulike materiaal wat jy nie geregtig is om te deel of tevrede te wees wat onwettig is nie.
4. Krediet en rekeningneming
Credit is prepaid and is consumed as matches run. Every match has a spending limit you set; reaching it pauses the match rather than continuing to spend. Balances are not transferable and, except where required by law, are non-refundable once consumed. Unused credit is refundable on request.
As jy jou eie inference-sleutel verbind, betaal jy jou verskaffer direk en ons maak geen per-totken lading op. Pas die verklaarde vrye toelae van 'n infrastruktuurgeld af om die paneel, gereedskap en berging te bedek nie.
Veranderinge is nooit van toepassing op krediet wat reeds gekoop is nie.
5. Aanvaarbaar gebruik
Moenie die diens gebruik om inhoud op te wek wat ander benadeel, om ons killes of stelselopdragte te probeer uitpak, om die besteding of tempobeperkings te omseil of om toegang sonder 'n geskrewe ooreenkoms te herverkoop. Die kode-uitvolg program is om bewerings te bevestig; moenie dit gebruik om enige stelsel aan te val nie.
6. Ondeundheid
We depend on third-party model providers. Providers go down, change models, and deprecate them. A match interrupted for any reason is paused and resumable; we do not charge for work that did not happen. We do not guarantee uninterrupted availability, and a model you used before may become unavailable.
7. Bemanheid
In die volste mate wat deur die wet toegelaat word, word die diens voorsien soos dit geen lasbejawighede van enige aard is nie. Ons algehele aanspreeklikheid vir enige eis is beperk tot die bedrag wat jy ons betaal het in die drie maande voordat die eis ontstaan het.
8. Bemintering
Jy kan jou rekening enige tyd sluit; ons sal die ongebruikte krediet herwin. Ons kan 'n kruisafvalsende rekening maak wat hierdie voorwaardes breek of wat die diens in gevaar stel.
9. Veranderinge, taal en kontak
Ons kan hierdie terme bywerk; materiële veranderinge sal op die perseel aangekondig word.
Vertalings van hierdie bladsy word voorsien vir gerief en word masjienproduksie. Waar 'n vertaling en die Engelse weergawe verskil, regeer die Engelse weergawe.
Vrae: Kontak ons.