清华姚班大牛再厉害，也离不开美国工具！

[sjtuvincent]

Anthropic Claude完成了 Fermat’s Last Theorem 首个端到端、可由计算机完整检查的形式化证明，整个过程仅用了11天

Claude在此期间写下约1300万行Lean代码，一共产出了约30300个可由计算机验证的定理，其中29500个中间定理进入最终证明。最终代码量已经达到Lean核心数学库Mathlib的5倍以上，也是迄今规模最大的Lean证明项目。

这项工作的发起者，是Anthropic研究员Tianyi Peng，本科毕业于清华大学姚班，博士毕业于麻省理工学院

[dealfinder10]

为什么不在国内读研究生，为什么不回国？哈哈

[Burlingame]

为什么不在国内读研究生，为什么不回国？哈哈

为什么不用DeepSeek，为什么不用华为的AI芯片，速度快还便宜

[macarthur]

为什么不在国内读研究生，为什么不回国？哈哈

你看看，我就说得限制出境吧？不能让这些小崽子们朝外跑。。。

[uws]

为什么不在国内读研究生，为什么不回国？哈哈

没有廉颇和娃的话， 分分钟就回去了
杨直麟的例子摆在那里