产品应用8

Claude形式化弱哥猜并修正11处错误

AI思想会2026-11-13

AI 摘要

Charlie Reams 借助 Claude Code 编写 19.4万行 Lean 4 代码，完成了弱哥德巴赫猜想证明的机器形式化验证。

错误修正：修正了常数抄错、积分越界等11处问题

外部依赖：纯逻辑全覆盖，外部仅依赖2项既有数值验证

关注公众号

扫码关注
第一时间收到每日精选

公众号专辑

Anthropic 前研发：写死规则拖垮新模型

Anthropic Claude Code 前核心研发 Thariq 披露，针对旧模型写的规则库正成为过度约束新模型的负资产，建议零规则起步。

Anthropic 公开 Claude 长期记忆设计，提出四层记忆模型与离线整理机制。这套方案已用于 Claude Code，通过对照原始底账定期纠错，解决经验丢失与错误继承问题。

清华姚期智团队提出代数世界模型（AWM），让 AI 探索陌生环境规律，并用 Lean 4 严格证明任务无解。在 ARC-AGI-3 关卡中全部构造出可独立检查的封闭证明。

开源社区推出 5 个面向设计任务的 Claude 工具，涵盖界面生成、组件规格图绘制、获奖网站参考检索、设计系统搭建及品牌方案生成，均适配 Claude Code。