CANTO 数学与可信推理

让数学的创造力，
与证明的严谨性同行。

提交一个命题与它的证明，得到有依据的诊断。我们关注结论是否成立，以及每一步论证能否支撑它。

这是 CantoMath 的测试性网站，欢迎大家试用。每个公网 IP 限试用一次。

此刻，为什么需要 Canto

答案愈发易得，正确性核验愈显稀缺。

在 AI 加速改变知识生产的当下，得到答案越来越容易，确认答案是否正确却依然需要严谨的审视。Canto 恰逢其时：我们致力于帮助数学家减轻繁琐核验的负担，解放注意力，让更多精力回到数学本身。

我们的愿景

Canto 长期探索从理解问题、寻找论证到计算机检查的自动化证明体系，让数学知识更可靠，也更容易积累与复用。这是我们的研究目标，并不意味着已经实现任意命题的自动判定。

认识 Lean

Lean 是开源的证明助手与编程语言。当定义、假设、结论和证明被精确表达后，计算机可以逐步检查推理。Lean 检查的是形式化证明，而非文字是否流畅。

当前服务

我们帮助你判断命题是否成立、证明是否有效。发现问题时，指出具体位置并解释原因，必要时提供反例，让判断有据可查。

核验的边界

证明有漏洞，并不说明命题一定错误。未找到证明，也不构成反驳。忠实对应原文的假设与量词仍是关键；局部检查不能替代完整证明，材料不精确时会要求补充说明。

人工智能正在深刻改变数学研究的方式。从定理证明到命题发现，AI 已深度介入数学研究的各个环节——这既是机遇，也是挑战：AI 生成的证明是否可靠？机器产出的结论如何核验？我们认为，数学研究者不应回避这场变革，而应主动拥抱它，同时守住数学最根本的标准——严格性与正确性。

正是在这样的背景下，AI4MATH-GXU研究小组建立了一个面向数学命题正确性核验的网站，希望为 AI 时代的数学研究提供可靠性的基础设施。我们的工作理念与陶哲轩等数学家发起的 SAIR 计划一致，也与 AXIOMMATH 的愿景相通。

除 AI for Math 外，我们同样关注其他对安全性、可靠性、正确性有高度要求的领域中的工程实践。欢迎交流合作。