一位数学家持有为期五年的资助，用于形式化费马大定理。而这一工作已在十一天内为他完成，他表示这一结果对数学本身毫无启示。Anthropic于周五发布了该证明。

数十个Claude代理编写了1300万行Lean代码，并证明了30,300个中间定理。他们使用了29,500个……