【陶哲轩用Claude Code解题，两度宕机，因为token不够用】

近日，菲尔兹奖得主、#加州大学洛杉矶分校# （UCLA）数学系教授陶哲轩（Terence Tao）在 YouTube 发布了一段时长约 26 分钟的实操视频，详细演示了如何利用 Anthropic 推出的 Claude Code 代理工具，在 Lean 定理证明器中完成一项数学证明的形式化全过程。

#陶哲轩# 在视频开始就明确了任务目标：将集合论中的“单例定律”（Singleton Law）从非形式化的自然语言描述，转化为 Lean 系统能够编译和严格验证的代码。简而言之，该定律论证了对于任意集合 A 和元素 x，单例集合 {x}属于 A 的条件等价于某些特定的子集属性。

尽管这在数学概念上这属于较为基础的引理，但要在类型论严苛的 Lean 系统中完成形式化，却伴随着大量琐碎且对语法要求极高的代码编写工作。

这并非陶哲轩首次处理这一任务。大约九个月前，他曾在其主导的“方程理论”（Equation Theories）项目中，已经利用当时的主流工具（如 GitHub Copilot）手动完成了该证明。

戳链接查看详情：http://t.cn/AXViLK77