شرایط خدمت
1. کار اين خدمت چيه؟
شما یک ادعا و یک استاندارد را ارسال می‌کنید. ما آن را از طریق یک پنل از مدل‌های هوش مصنوعی که انتخاب کرده‌اید، به علاوه یک مدل داور که معیارهای پذیرش را تعیین می‌کند، اجرا می‌کنیم و تلاش می‌کنیم نتیجه را در Lean 4 در مقابل Mathlib رسمی کنیم. خروجی یک رونوشت، مجموعه ای از حکم‌ها، یک حکم و جایی که رسمی سازی تلاش شده، نتیجه Lean است.
خروجی چیست و چی نیست؟
خروجی توسط مدل‌های هوش مصنوعی طرف سوم تولید می‌شود و توصیه نیست. این خدمات شامل مشاوره حقوقی، پزشکی، مالی، مهندسی یا حرفه‌ای در هر نوع نیست و هیچ رابطه حرفه‌ای با استفاده از این خدمات ایجاد نمی‌شود.
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.
یک فرمول‌بندی Lean موفق به این معنی است که هستۀ Lean اثبات جمله را که فرمول‌بندی شده بود ، در برابر نسخه Mathlib در آن زمان پذیرفت. به این معنی نیست که آن جمله ترجمۀ دقیقی از آنچه که خواستید است ، و انتخاب یک جمله رسمی که آنچه را که منظورتان است نمی‌گوید ، رایج‌ترین راه گمراه کردن نتیجه رسمی است. جمله رسمی را بخوانید ، نه فقط حکم.
محتوای شما
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.
اطلاعات شخصی در مورد دیگران، مواد محرمانه که حق اشتراک ندارید یا محتوایی که غیرقانونی است را ارسال نکنید.
اعتبارات و قبض
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.
اگر کلید استنتاج خود را متصل کنید، مستقیماً به ارائه‌دهنده پرداخت می‌کنید و ما هیچ هزینه‌ای برای هر توکن دریافت نمی‌کنیم. پس از مجوز آزاد اعلام شده، هزینه زیرساخت برای پوشش اجرای پنل، ابزارها و ذخیره‌سازی اعمال می‌شود.
ما ممکنه با اطلاع قبلي قيمت ها رو تغيير بديم تغييرات هيچوقت به اعتباري که قبلاً خريده شده نياز نداره
استفاده قابل قبول
از این سرویس برای تولید محتوایی که به دیگران آسیب می‌رساند، برای تلاش برای استخراج دستورالعمل‌های سیستم یا دستورالعمل‌های ما، برای دور زدن محدودیت‌های هزینه یا نرخ، یا برای بازفروش دسترسی بدون توافق‌نامهٔ کتبی استفاده نکنید. ابزار اجرای کد برای تأیید ادعاها است؛ برای حمله به هر سیستمی از آن استفاده نکنید.
در دسترس بودن
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.
مسئولیت
تا حدی که قانون اجازه می‌دهد، خدمات به صورتی که هستند و بدون هیچگونه تضمین ارائه می‌شود. مسئولیت کل ما برای هرگونه ادعایی به مقداری که در سه ماه قبل از بروز ادعا پرداخت کرده‌اید محدود است. ما برای خسارت غیرمستقیم یا نتیجه ای، از جمله هرگونه خسارت ناشی از اعتماد به خروجی مدل، مسئول نیستیم.
پایان
شما می‌توانید حساب خود را در هر زمان ببندید؛ ما اعتبار استفاده نشده را بازپرداخت می‌کنیم. ما می‌توانیم حساب‌هایی را که این شرایط را نقض می‌کنند یا خدمات را در معرض خطر قرار می‌دهند تعلیق کنیم.
9. تغییرات، زبان و تماس
ما ممکن است این شرایط را به روز کنیم؛ تغییرات اساسی در سایت اعلام خواهد شد.
ترجمه‌های این صفحه به منظور راحتی فراهم شده‌اند و توسط ماشین تولید شده‌اند. در صورتی که ترجمه و نسخه انگلیسی با هم تفاوت داشته باشند، نسخه انگلیسی حاکم است.
سوالات: با ما تماس بگیرید.