Anthropic 用 Claude 自动验证现有代码并生成数学证明

Anthropic 使用 Claude 为现有软件生成数学证明，并由独立验证程序 Rocq 自动检查；Anthropic 称，Claude 在数周内生成约 1.8 亿行证明代码。验证条件限于特定处理器架构、单线程程序和小于 64 MB 的输入，单项证明可能消耗数亿个 tokens。