About Theorem.chat
Theorem.chat 进行数学索赔并试图解决它。 您声明了索赔, 以及它必须达到的标准。 一组AI模型 — — 随你需要多少, 不论你来自哪个供应商 — — 攻击它, 并再攻击一个示范裁判。 然后,在Lean 4年对Mathlib中正式提出这个论点, 利恩内核决定它是否得到证实。 最后一步是产品。
为什么是内核,而不是另一种模式
询问模型的难题, 并获得一个精通的答案。 询问数个, 他们通常同意, 感觉像是证明, 而不是: 模型共享培训数据, 分享盲点。 第二个模型检查第一个模型仍然是同样的判断, 也可以进行圆的。 利恩内核不能。 它要么来自轴和Mathlib 的表达, 要么没有, 信任对结果没有影响 。
通常伪造正式证据的方式会被检查并拒绝。 留下sorry洞的证明被检测和拒绝,其中native_decide个是吸引native_decide个来让内核通过信任来计算,或者静悄悄地引入新正统的证据,而不是被算作成功。
面板实际上能做什么
Arguing is the cheap part. The panel works with the literature — arXiv, OpenAlex, Crossref — so a known result is cited rather than re-derived badly. It has SageMath and PARI/GP for computation, Z3 and CVC5 for SMT solving, OEIS lookup for identifying a sequence it has constructed, and a sandboxed Python environment with no network access. A conjecture can be tested against ten thousand cases before anyone spends a round trying to prove it, and a counterexample ends the discussion immediately.
证据,不是口才
A match is not scored on argument quality. The claim is decomposed into acceptance criteria, and a criterion is only settled when something behind it can be re-checked by a third party: a source with the relevant passage quoted, or code that was actually executed with its real output. The referee re-checks that evidence itself before ruling, and it cannot declare the match finished while a criterion is still open.
您设置了栏杆
标准是您选择的标准,裁判员可以完全持有。 询问一位谨慎的专家会接受什么, 你就会得到什么。 要求用每一个假设来进行完全的推论, 并且你得到一个相反的判断。 要求酒吧提供奖项会面临, 诚实的结果通常是对小组短缺之处的准确描述 — — 这比一个自信的主张更值得你反正也要检查自己。
坦率地说,这不是解决未决问题的机器,而是拒绝让争论在没有解决时就解决的机器,它告诉了你们哪个步骤失败了。
失败的正规化是有用的输出
当Lean不完成证据时,你就会得到剩下的确切目标。实际上,这几乎总是非正式论点手动跳动的地方,每个阅读流言版本的人都会点头。然后,这个目标被交给最适合攻击它的位置,连同已经尝试过的东西,其他的都没有。模型在卡住时会打,然后用全部费用重新确认;通过一个具体问题,而通常为一小部分Token物品解开障碍。
长期工作生存
Every lemma the panel establishes goes into a shared ledger with its proof, so results are written once and never re-derived, and dead ends are recorded so nobody walks back into them. Matches run server-side and pause cleanly — on budget, on a provider outage, or because you closed the tab — and resume exactly where they stopped.
这样做不是为了什么
理论论是一个推论词。 这个网站是为数学、逻辑、理论计算机科学、理论物理和经济理论 — — 即一项主张通过证明解决的领域 — — 建立的,生物学、医学、化学或社会科学方面的实证问题并不产生理论,它们产生结论,也不进行大量正规化决定。 我们的姐妹网站referee.chat没有利昂步骤,就这些问题运行同样的小组和裁判程序。