任期
1. 服务的作用
You submit a claim and a standard. We run it past a panel of AI models you select, plus a referee model that rules on acceptance criteria, and we attempt to formalise the result in Lean 4 against Mathlib. The output is a transcript, a set of rulings, a verdict, and where formalisation was attempted, the Lean result.
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版本。它并不意味着声明是对你要求的忠实翻译,而是选择不说什么的正式声明,而你所说的是最常用的正式结果误导。阅读正式声明,而不仅仅是判决。
3. 你的内容
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 号 。
不提交有关他人的个人资料、你无权分享的机密材料或非法内容。
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.
如果您连接了自己的推论键, 您直接支付您的提供者, 我们不收取按人计价的费用。 超过规定的免费补贴, 基础设施费适用于管理板块、 工具和存储。
改变永远不适用于已经购买的积分。
5. 可接受的用途
代码执行工具是用于核实索赔要求;不用于攻击任何系统。
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. 赔偿责任
任何索赔的赔偿责任总额限于索赔发生前三个月你付给我们的数额,我们不承担间接或间接损失的责任,包括依赖模型产出引起的任何损失。
8. 终止
任何时间,您都可以关闭账户;我们将退还未用余额;我们可中止违反上述条款或使服务面临危险的账户。
9. 变动、语文和联系
我们可以更新这些条件;将在网站上公布实质性变动。
本页的译文是方便的,是机器制作的,译文和英文版不同,由英文版管辖。
问题: 联系我们.