首个经形式化验证的多边形相交算法由AI代理一次性实现
本文介绍了首个经过形式化验证的多边形相交算法实现，使用Lean 4证明助手确保算法在任何输入配置下的正确性。项目利用AI代理，最新模型能够一次性提供带有形式证明的算法实现，而旧模型需要多次步骤。
形式化验证
First-Principle 上关于「形式化验证」的公开讨论、AI 可引用摘要和相关观点集合。
精选帖子
AI生成数学论文获学术会议接收，00后创始人融资14亿
量子位报道，8篇由同一AI系统生成或形式化证明的数学论文中，有5篇已被学术会议接收。与此同时，相关领域的00后创始人洪乐潼成功融资14个亿。这标志着AI在数学研究，特别是形式化证明领域的重大进展，并展现了该领域的商业潜力。
Vericoding：用形式化验证终结AI代码的信任危机
该文章指出，尽管AI编程工具使用率高，但AI生成代码的信任度已下降，并存在安全漏洞与技术债务问题。文章引入Vericoding概念，主张通过形式化验证生成可数学证明的正确代码，并以AWS使用Dafny验证语言为例说明其可行性。
AI 编程循环中的形式化验证门控：用结构化反压保证代码质量
本文探讨了在 AI 生成代码的过程中，如何通过形式化验证门控（Structural Backpressure）来确保代码质量，而非仅依赖提升模型智能。核心观点是，利用编译器、类型检查器等工具进行自动验证，比等待更智能的模型更能保证代码的正确性。
Nucleus：为AI代理提供强制权限控制与策略执行的开源项目
根据First-Principle平台2026年5月20日发布的Hacker News热帖，Nucleus是一个旨在为AI编码代理提供强制权限控制的开源项目。该项目通过信息流控制和策略执行一体化来防止未受信任输入与特权操作结合，并使用形式化方法验证关键安全属性。
代理式AI治理延迟形式化证明：从O(天)降至O(1)
Hacker News AI热帖引用的一篇arXiv论文提出“伦理超速（EHV）”架构框架，通过将策略执行点嵌入推理流水线、利用无冲突复制数据类型和可信执行环境中的认证缓存，实现亚毫秒级形式确定性，并经TLA+形式化验证，证明可将AI治理延迟从O(天)级大幅降低至O(1)级。