标签
Basis 研究人员利用 LLM 为一门小型编程语言编写形式化语义，并使用 Lean 证明编译到 RISC-V 后解释器符合这些规则。他们将现有解释器作为基准真值，以克服验证式软件中的规范瓶颈。
Lean v4.35.0 现已内置多个经验证的内核，包括 con-leche（首个拥有形式化一致性证明、由 Claude 实现的 Lean 编写内核）及其 Rust 优化版本 con-ron，以及新增的 `lake check` 命令，用于在外部重新检查开发成果。此举源于 AI 发现的内核健全性漏洞，旨在消除实现层面的不健全性，同时不带来性能损失。
西蒙斯基金会、Anthropic 和 OpenAI 宣布联合发起一项总额为 1500 万美元的计划，帮助数学家适应人工智能，资助研讨会、公开征集项目提案，并为研究人员提供人工智能工具和算力资源。
开发者用 Lean 4 完整实现了 RealWorld（Medium 克隆）参考应用，前后端全部使用 Lean 编写，并借助社区库（HTTP 服务器、Postgres 驱动、JWT、HTML 渲染等）通过官方 API 与网站测试套件。文章以数学论文风格呈现，部分关键性质以定理形式在 Lean 中形式化验证。
Creusot 0.14.0 发布，这是 Rust 的形式化验证工具，新增了对偏序（partial orders）的支持以及为快照（snapshots）生成验证条件（VCs）的功能。
作者们提出 Choir——一个用于分布式多智能体自动形式化的开放、模块化协议，将项目拆解为基于 GitHub 的任务，并通过确定性的信任门验证机制进行审核，支持 Lean 4、Isabelle 和 Rocq；该项目包含一篇预印本以及一个由 DARPA expMath 项目资助的开源代码仓库。
与 Lean 和 Z3 的创造者 Leonardo de Moura 的访谈节目，讨论 Lean 的工作原理、LLM 在形式化验证中的作用，以及 AI 辅助证明如何改变软件开发和数学。
The Incredible Proof Machine 是一款可视化工具，通过拖拽并连接模块来在各种逻辑中进行证明。它旨在让定理证明变得既易于理解又有趣，无需传统证明工具的语法。
一份使用Lean证明助手进行形式验证的教程，具体验证一次性密码本协议。面向刚接触形式验证的密码学工程师。
马特·帕克的视频探讨了近期AI（包括ChatGPT）帮助解决未解的Erdős问题的案例，彰显了AI辅助数学发现的新时代。
本文报告了一个验证流水线的经验，该流水线使用AI证明器（Aristotle和Aleph）结合符号提取工具和形式化密码学库，为Lean 4中的Rust密码学代码生成机器检查的正确性证明，并提供了来自以太坊基金会zkEVM项目的案例研究。
Mistral AI 发布 Leanstral 1.5，一个拥有 6B 激活参数的模型，用于 Lean 4 证明工程，在多个形式化验证基准测试中取得最先进成果，并发现了真实世界中的错误，完全开源，采用 Apache-2.0 许可。
本文提出了一个再形式化的案例研究，使用大型语言模型（LLMs）在证明助手之间（从 Mizar 到 Lean、从 HOL Light 到 Lean 以及从 HOL Light 到 Agda）转移 Jordan Curve Theorem，并分析了实际再形式化任务中的流水线设计选择。
本文应用VGPT-RSI人工智能系统生成与黎曼假设相关的形式化验证的部分结果，包括边界证书和有限Lagarias不等式，同时明确识别剩余数学障碍。
Google新论文提出LEAP框架，将数学问题拆解为目标树，利用Lean验证器反馈进行学习，使LLM在数学竞赛题上的正确率从10%提升至70%，解决了Putnam 2025全部12题，并在IMO基准上超越专用金牌级系统。
本文描述了Lean 4中一个形式化验证的金融数学库，包含200多个定理，涵盖从测度论基础到衍生品定价的内容，并包含一个保真度审计，根据Lean语句与所声称数学之间的关系对结果进行分类。