サービス条件
1. サービスの目的
クライアントはクレームと標準を提出します。 それを選択したAIモデルのパネルを通して実行します。 さらに、受容基準を決める審査員モデルを加え、Lean 4とMathlibの間で結果を形式化しようとします。 出力は、記録、判断の集合、判断、形式化を試みた場合は、リーン結果です。
２．出力の内容と内容のない内容
出力は第三者ＡＩモデルによって生成され，アドバイスではない。 法律的，医療的，財務的，技術的，またはどのような専門的な助言でもなく，このサービスを使用することでプロの関係を作り出すことはない。
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 はデフォルトでプライベートです。パブリック match をマークすると、リンクを持つ誰でも見ることができ、パブリックギャラリーに表示されるかもしれません。 機密情報を含む match を公開しないでください。
他人の個人情報や、共有権限がない機密資料、違法なコンテンツを送信しないでください。
クレジットと請求
クレジットは前払いであり、matches が動作すると消費されます。match はそれぞれ、設定した消費制限があり、それに達すると、match は消費を続ける代わりに一時停止します。残高は移動できません。法律で要求される場合を除いて、一度消費した後は返金できません。未使用のクレジットは要求に応じて返金できます。
これは、 ユーザが自分の推論キーを接続すると、 プロバイダに直接支払い、トークンごとの料金を請求しません。 指定されたフリーアクセスを超えると、 パネル、ツール、ストレージの運用にインフラストラクチャ料金が適用されます。
価格は変更されますが 既に購入したクレジットには 変更は適用されません
許容される使用
サービスを他人に害を与えるコンテンツを生成するために使用しないこと、プロンプトやシステム指示を抽出しようとすること、消費や料金制限を回避するために使用しないこと、書面上の合意なしにアクセスを再販売するために使用しないこと。コード実行ツールは主張を検証するためのものであり、システムを攻撃するために使用してはいけません。
利用可能性
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.
責任
法律で許される限り、サービスは保証なしに提供されます。クレームに対する我々の総責任は、クレームが発生する前の 3 ヶ月間にお客様が支払った金額に限られます。モデル出力を信頼することによって生じる損失を含む間接的または結果的な損失に対しては、我々は責任を負いません。
終了
あなたはいつでもアカウントを閉鎖できます。未使用クレジットは返金します。この条件を破ったり、サービスを危険にさらしたアカウントは停止されます。
9. 変更・言語・連絡
これらの条件は変更される場合がある。
このページの翻訳は便利さを目的として機械で作成されています。翻訳と英語版の違いがある場合は、英語版が優先されます。
質問: 連絡先.