标签
作者赞同 poteto 的观点，批评让 Sub-agent 互相对抗式代码审查（Adversarial Review）纯属浪费 Token，指出其存在无意义 nitpicking、过度设计和算力错配三大死穴，并认为顶级团队正转向实测、形式化验证与真实红队来发现问题。
一名伊利诺伊大学厄巴纳-香槟分校（UIUC）的学生正在为 Loxeon 寻求算力赞助。Loxeon 是一个计划采用 Apache-2.0 许可证的运行时，使用 Rust 编写，并对照形式化规约进行验证；AI 智能体团队可通过形式化定义的原语（身份、能力委托、角色重新绑定、树形管理，以及基于 epoch/ticket 的消息验证）实现自组织。其目标是通过公平的基准测试，评估多智能体团队在真实编程任务中的表现是否优于单个智能体（小规模测试约需 200 美元，完整测试约需 1,500 美元）；无论结果如何，代码、日志和测试结果都将公开。
一个由研究人员参与的流程结合了大语言模型引导的程序演化、精确评估和 Lean 形式化证明检查，发现了一个新的纠缠辅助量子纠错码族，以 115 条经验证的记录和 10 项经认证的不存在性结果，填补了已归档的纠缠辅助量子纠错码（EAQECC）表中的 54 处空白。
Lauren (poteto) 为结束与 OpenAI 的 Tibo 的 28 天互怼挑战，用 Grok Bot 和 Cursor 花 4 天开发了一个可嵌入 X 推文卡片的类吸血鬼幸存者网页游戏，技术复盘展示了 1150 个 Agent PR、TLA+ 形式化验证、零内存分配 lint 约束和确定性引擎等硬核 AI 辅助工程实践。
LeanGuard 是一种运行时系统，依据具有时序逻辑语义的 Lean4 策略验证语言模型智能体的每一次工具调用，减少违规调用和提示注入的成功，同时支持在证明指导下修复被拒绝的操作。
QwenBend 是一个实验性项目，Qwen 在其中编写 Bend 程序，依据 Bend2 规则对其进行类型检查，并在自身的前向传播过程中，使用一个拥有 5300 万个权重的 CPU（16 个寄存器、8k RAM、基于 SwiGLU 的逻辑门）执行该程序，无需外部解释器或编译器。
Meta 和纽约大学的一篇新论文表明，h1 这一为模型提供快速 Lean 反馈和搜索工具的简单智能体循环，能够匹敌甚至超越人工设计的定理证明工作流：它以更低的成本在 PutnamBench 上超过了 Goedel-Architect（解出 598 题，后者为 597 题）；搭配 Opus 4.8 时，它解出了 100 道高难度代数题中的 83 道，而 Claude Code 解出了 63 道。
OpenFrontiers 推出了一个跨学科语料库，包含 12,151 个尚未解决的研究问题，以及一个由 200 个近期已解决的数学问题组成的回溯性基准，这些问题均附有 Lean 4 形式化陈述。该研究评估了七个大语言模型智能体，发现它们在闭卷条件下重新发现研究级成果的情况仍然罕见，而在实时联网条件下取得的成功则主要源于检索已发表的解答。
Lasm 将 Lean 4 程序提前编译为 WebAssembly，使形式化验证的 Web 应用能够通过单一代码库部署到 Node、Serverless 和边缘平台，其旗舰示例 Conduit 已证明了 117 条定理。
通过一份由神经符号大证明模型（LPM）生成、经 Lean 4 内核检验的证明，证明了 Kullmann（2010）提出的长期悬而未决的猜想 W(2;3,21) = 416。该证明涵盖 209 个案例和 3860 万个叶节点公式，并附有一个 13.6 GB 的可验证证据包。
播客访谈：Lean 创始人 Leo de Moura 谈 AI 如何让形式化验证走向实用、验证 AI 生成代码与自主智能体的必要性，以及构建经过验证的软件栈的愿景。
包括 &Truth（7000万美元）、Harmonic（2.95亿美元）以及与 Anthropic 合作的 Theorem 在内的一批初创公司，正押注生成式 AI 能让软件形式化验证变得切实可行，从而可能彻底改变验证 AI 生成代码可靠性的方式。
AdaCore 展示了利用 AI（无需直接人工干预）在 SPARK 中生成经过形式化证明的 AES、SHA-256 和 HMAC-SHA-256 实现，正确性通过四种独立方式验证，呼应 Anthropic 关于 LLM 用于形式化软件验证的研究。
论文提出了EasyProver——一个基于递归智能体和异步搜索的Lean证明系统，使用现成的前沿模型即可在PutnamBench和IMO基准上接近饱和；同时还提出Aegis，一个将竞赛编程转化为更具挑战性的真实世界Rust到Lean验证任务的流水线，可用于基准测试和强化学习。
Anthropic 发布了 formal-math GitHub 仓库，收录了经机器验证的 Lean 4 形式化证明。其中，Claude 生成的证明在 Lean 中形式化了一种计算 k-CNF 公式满足赋值数量的算法，从而推翻了指数时间假设（ETH）；仓库还包含黎曼 ζ 函数零点以及 3SUM/APSP 等相关结果的形式化证明。
Lanyon AI 从 11 月 1 日起向早期客户和测试者推出 Lanyon 的预发布版本，并在旧金山和芝加哥同时举办公开演示，致力于构建可形式化验证的科学模型。
该论文确定了在独立非同分布噪声和两两非负相关噪声下，选择最大噪声分数所产生的“赢家偏差”的尖锐常数界，并将全部定理在 Lean 4 中形式化验证，同时在 448 个模型选择流程上验证了结论的实际意义。
本文介绍 PaperFormalizer——一个基于 Lean 的作者参与式自动形式化流程，可从 LaTeX 论文出发构建语句依赖图、审计语句并将其形式化证明，同时在语义存在歧义时让作者做出决策，从而产出经 Lean 验证的论文版本。
一篇论文展示了简单智能体框架（h1）配合高效的 Lean 4 反馈接口，在 PutnamBench、FATE-X 和 FormalConjectures 上达到了最先进的形式定理证明结果，不逊于甚至超越了专门设计的多步工作流，并解决了八个公开问题。作者认为执行接口比复杂的编排更为重要，并警告在未用高效反馈评测前沿模型之前，不要过早规定结构化工作流。
一个社区研究仓库报告了整数乘法更严格的指数上界，在 OpenAI #109 框架下实现了 T(n)=O(n(log n)^(1-κ))，其中 κ=0.0023；该结果以未经验证的假设为前提，尚未构成完整的 Lean 证明。