서비스 약관
1. 서비스가 하는 일
클레임과 표준을 제출하면, 귀하가 선택한 AI 모델 패널과 수용 기준을 규정하는 심판 모델을 통해 실행되고, Lean 4 대 Mathlib에서 결과를 공식화하려고 시도합니다. 출력은 녹음, 규정 세트, 판결, 공식화 시도가 있었던 경우 린 결과입니다.
2. 출력이 무엇이고 무엇이 아닌지
출력은 타사 AI 모델에 의해 생성되며 조언이 아닙니다. 이는 어떠한 법적, 의료적, 재정적, 엔지니어링 또는 전문적인 조언도 아니며, 이 서비스를 사용함으로써 전문적인 관계가 생성되지 않습니다.
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.
성공적인 린 형식화는 린 커널이 그 당시 사용되고 있던 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.
다른 사람에 대한 개인 데이터, 공유할 권한이 없는 기밀 자료 또는 불법 콘텐츠를 제출하지 마십시오.
4. 크레딧 및 청구
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.
자신의 추론 키를 연결하면 공급업체에 직접 지불하고 토큰당 요금이 없습니다. 명시된 무료 허용량을 초과하면 패널, 도구 및 스토리지를 실행하는 데 인프라 수수료가 적용됩니다.
당사는 통지 없이 가격을 변경할 수 있습니다. 변경 사항은 이미 구매한 크레딧에 적용되지 않습니다.
허용 가능한 사용
다른 사람에게 해를 끼치는 콘텐츠를 생성하거나, 프롬프트 또는 시스템 지침을 추출하거나, 지출 또는 요금 제한을 우회하거나, 서면 계약 없이 액세스를 재판매하는 등의 목적으로 서비스를 사용하지 마십시오. 코드 실행 도구는 주장을 확인하는 데 사용되며 시스템을 공격하는 데 사용해서는 안 됩니다.
6. 접근성
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. 책임의 제한
법률이 허용하는 최대한의 범위 내에서, 서비스는 어떠한 종류의 보증 없이 그대로 제공됩니다. 클레임에 대한 당사의 총 책임은 클레임 발생 전 3개월 동안 당사에 지불한 금액으로 제한됩니다. 당사는 모델 출력에 의존하여 발생하는 손실을 포함한 간접적 또는 결과적 손실에 대해 책임을 지지 않습니다.
8. 종료
귀하는 언제든지 계정을 폐쇄할 수 있으며, 사용되지 않은 크레딧을 환불받을 수 있습니다. 당사는 본 약관을 위반하거나 서비스를 위험에 빠뜨리는 계정을 일시 정지할 수 있습니다.
9. 변경, 언어 및 연락처
당사는 이러한 약관을 업데이트할 수 있으며, 중요한 변경 사항은 사이트에 발표됩니다.
이 페이지의 번역은 편의를 위해 제공되며 기계로 생성됩니다. 번역과 영어 버전이 다를 경우 영어 버전이 우선합니다.
질문: 저희에게 연락하십시오.