AI 数学推理验算
提交一段 AI 数学对话，立即得到主张依赖图、可运行检验和最早的可疑推理步骤。
研究者把一段与 AI 讨论数学问题的完整对话贴进来，也可附上自己引用的定理和笔记。系统先把定义、假设、引理、计算和结论拆成可折叠的主张节点，连成一张推理依赖图。
每个节点会被分到不同的检查路径：数值上可试验的推导生成小规模反例搜索或计算脚本；引用外部定理的地方要求补上准确出处；纯文字跳步则被标为待人工审查。用户点开任一结论，都能一路回溯它依赖了对话中的哪几句话。
最重要的输出不是整段回答的真假分数，而是“最早可疑步骤”。如果某个定义被偷换，或某项条件在中途消失，后续所有依赖它的漂亮推导都会被连带标记。研究者修正一个节点后，只需重查受它影响的分支。
起步版本服务于符号推理和可明确列出前提的数学对话，不替代同行评审，也不宣称自动证明或推翻猜想。它帮助研究者先找到最值得亲手验算的那一步。
为什么是现在
7月22日，陶哲轩公开的对话登上 Hacker News 第2名，快照录得549分和349条评论。S1 研究者更可能直接阅读并复用长篇 AI 数学对话，也更需要定位最早失效的前提或推导。
目标用户
核心用户是会用大模型探索证明思路的研究者、博士生和形式化数学工程师。当对话已经延伸数十轮，且结论开始依赖早期定义时，他们最容易失去全局把握。此时重新通读成本很高，直接形式化整段内容又太慢。他们需要先找出最值得亲手验算的节点，再决定是否投入完整证明。
最小切入点
先让模型按固定 JSON 结构抽取定义、假设、引理和结论。每个节点必须保留原句位置，并声明直接依赖。用 NetworkX 维护有向无环图，修改节点后只重跑后继分支。多项式恒等式、有限枚举和数值代入交给 SymPy，并在受限容器中执行。外部定理先接 TheoremGraph API 或 LeanSearch 检索候选出处。S3S4 首版不尝试把整段对话自动翻成 Lean，只允许用户把关键节点送入 Lean 复核。这样可先验证“最早可疑步骤”是否真的节省验算时间。
以小博大
先选公开的 AI 数学对话，发布可交互的推理图和复查过程。每个案例只展示一个被定位的前提缺口，方便研究者判断价值。做一个 ChatGPT 分享链接导入器，降低首次尝试成本。随后在 Lean Zulip、Mathlib 社区和相关 Hacker News 讨论中发布技术复盘，并邀请用户提交匿名失败案例。
竞品与缝隙
怎么赚钱
按个人工作区订阅收费，包含固定的对话解析与重查额度。超出额度后按任务计费，团队版再提供共享批注和私有资料库。
反方视角
最危险的问题是主张抽取本身出错。一个依赖边连错，就可能把无辜步骤标成源头，让研究者浪费更多时间。自然语言到符号表达的转换也会遗漏量词、定义域和例外条件。外部定理可能只有相似名称，错误匹配会制造虚假的出处感。自动生成的脚本还需要隔离执行，并限制资源与可访问文件。若系统频繁把表达省略当成数学错误，用户很快会忽略告警。继续推进前，应先用专家标注对话检验节点、依赖边和最早错误三项准确性。