Syarat Perkhidmatan
1. Apa yang servis ini lakukan
Anda menghantar tuntutan dan piawaian. Kami jalankan ia melalui panel model AI yang anda pilih, ditambah model hakim yang memerintah kriteria penerimaan, dan kami cuba untuk formalkan hasil dalam Lean 4 berbanding Mathlib. Output adalah transkripsi, set keputusan, keputusan, dan di mana formalisasi telah dicuba, hasil Lean.
2. Apa output adalah dan tidak
Output dihasilkan oleh model AI pihak ketiga dan bukan nasihat. Ia bukan nasihat undang-undang, perubatan, kewangan, kejuruteraan atau profesional apa-apa jenis, dan tiada hubungan profesional dicipta dengan menggunakan perkhidmatan ini.
Penilai yang memutuskan kriteria yang dipenuhi adalah satu kenyataan mengenai bukti dalam rekod dalam perlawanan itu. Ia bukan jaminan kebenaran. Model AI membuat kesilapan, salah baca sumber, dan boleh mencipta rujukan walaupun arahan tidak. Anda mesti secara bebas mengesahkan apa-apa yang anda berniat bergantung pada, terutamanya sebelum menerbitkannya, menghantarnya, atau bertindak atasnya. Ini adalah alat untuk kerja ujian tekanan, bukan pengganti untuk tinjauan manusia yang berkelayakan.
Peformalan Lean yang berjaya bermakna kernel Lean menerima bukti bagi pernyataan yang telah diformalkan, berbanding versi Mathlib yang digunakan pada masa itu. Ia tidak bermakna pernyataan itu adalah terjemahan yang tepat bagi apa yang anda minta, dan memilih pernyataan formal yang tidak menyatakan apa yang anda maksudkan adalah cara paling biasa bagi hasil formal yang mengelirukan. Baca pernyataan formal, bukan hanya keputusan.
3. Kandungan anda
Anda menyimpan hak milik tuntutan yang anda hantar dan output yang dihasilkan untuk anda. Anda hanya berikan kami lesen yang diperlukan untuk menjalankan perkhidmatan: untuk memproses hantaran anda, menghantarnya ke pembekal model yang anda pilih, dan simpan hasil yang sepadan supaya anda boleh kembali kenya.
Padanan adalah peribadi secara lalai. Jika anda tandakan padanan sebagai awam ia akan kelihatan kepada sesiapa yang mempunyai pautan dan mungkin muncul dalam galeri awam kami. Jangan terbitkan padanan yang mengandungi apa-apa yang rahsia.
Jangan hantar data peribadi mengenai orang lain, bahan rahsia yang anda tidak berhak untuk berkongsi, atau kandungan yang tidak sah.
4. Kredit dan bil
Kredit adalah prabayar dan digunakan semasa perlawanan berjalan. Setiap perlawanan mempunyai had perbelanjaan yang anda tetapkan; mencapainya menghentam perlawanan daripada terus menghabiskan. Saldo tidak boleh dipindahkan dan, kecuali di mana dikehendaki oleh undang-undang, tidak boleh dikembalikan selepas digunakan. Kredit tidak digunakan boleh dikembalikan pada permintaan.
Jika anda sambungkan kekunci kesimpulan anda sendiri, anda membayar pembekal anda secara langsung dan kami tidak membayar sebarang caj per-token. Selepas had percuma yang dinyatakan, bayaran infrastruktur dikenakan untuk menutup pelaksanaan panel, alat dan storan.
Kami boleh ubah harga dengan notis. Perubahan tidak pernah digunakan untuk kredit yang telah dibeli.
Penggunaan yang boleh diterima
Jangan guna servis ini untuk menghasilkan kandungan yang merosakkan orang lain, untuk cuba mengekstrak prompt atau arahan sistem kami, untuk mengelak had perbelanjaan atau kadar, atau untuk menjual semula akses tanpa persetujuan bertulis. Alat laksana kod adalah untuk mengesahkan tuntutan; jangan gunanya untuk menyerang sistem mana-mana.
Kebolehcapaian
Kami bergantung pada pembekal model pihak ketiga. Pembekal jatuh, ubah model, dan membuangnya. Sebuah perbandingan yang terganggu untuk apa-apa sebab dijeda dan boleh dilanjutkan; kami tidak membayar untuk kerja yang tidak berlaku. Kami tidak menjamin ketersediaan tanpa terganggu, dan model yang anda gunakan sebelum ini mungkin tidak tersedia.
Liabiliti
Sejauh mana yang dibenarkan oleh undang-undang, perkhidmatan ini disediakan sepertimana ianya tanpa sebarang jaminan. Kewajipan kami terhadap sebarang tuntutan adalah terhad kepada jumlah yang anda bayar kepada kami dalam tiga bulan sebelum tuntutan timbul. Kami tidak bertanggungjawab terhadap kerugian tidak langsung atau akibat, termasuk kerugian yang timbul daripada bergantung pada output model.
Penghujungan
Anda boleh tutup akaun anda bila-bila masa; kami akan mengembalikan kredit yang tidak digunakan. Kami boleh menangguhkan akaun yang melanggar syarat ini atau yang meletakkan perkhidmatan dalam risiko.
Perubahan, bahasa dan kenalan
Kami boleh kemaskini syarat-syarat ini; perubahan material akan diumumkan di laman web.
Terjemahan halaman ini disediakan untuk kemudahan dan dihasilkan oleh mesin. Di mana terjemahan dan versi Bahasa Inggeris berbeza, versi Bahasa Inggeris berkuasa.
Soalan: Hubungi kami.