标签
介绍 IneqAgent，一个将大语言模型推理与符号计算结合的智能体框架，用于 Lean 4 中的不等式形式化证明，采用引理级蒙特卡洛树搜索协调引理构造与符号后端选择，在四个基准上达到 94.09% 的成功率。
QuixiAI 开源了 Sovereign Protocol Language (SPL)，一个基于 Lean 4 的形式化库，为"主权代理协议"(Protocol of Sovereign Agency) 提供规范性语义，核心包括 Duty、Power、Immunity 等原语以及 Law 3 非干扰实验，全部定理经内核验证、无公理依赖。
Materialize 介绍了它如何重构 `persist` 元数据存储，使用 PostgreSQL 的 READ COMMITTED 隔离级别而非 SERIALIZABLE 来构建可线性化日志，在一次亚稳态延迟事件后将写入吞吐量提升了三倍，并通过在 Lean 4 中对 PostgreSQL 的行为建模来证明可线性化，验证了正确性。
一位研究者称自己花了三个月时间用 Claude Code 和 Codex 攻关 Erdős 第 993 号问题（树的独立集序列的单峰性），却在今天得知 Tong Zhang 和 Wei Li 上周已发布了完整证明，同时还有两份声称可成功构建的 Lean 4 形式化代码。该结果尚未经过同行评审。
一个研究团队对 OpenAI 的 Lean 4 三维 Navier-Stokes 爆炸形式化证明进行了审计，发现该解在数学上虽完全成立，但在原子尺度上会物理失效（流体在 0.7 纳米处汽化）——这是一种典型的规格博弈（specification gaming）。他们提出为神经符号 AI 系统增加一个物理边界层，并开源了其验证脚本。
本文提出了一种用于Lean 4中形式定理证明的三角色蒙特卡洛树搜索框架，将编译器作为奖励预言机以提高样本效率，并通过内核级证明审计揭示奖励黑客问题。
本文提出了一种用于Lean 4上下文依赖定理证明的编译器引导自适应证明搜索框架，利用跨模型协同来提高证明成功率并降低计算成本。
MathForm引入了一个利用知识检索和验证引导优化的数学自动形式化框架，产生了FormalVerse数据集和一个8B模型，该模型在性能上优于专业基线模型。
PULSE is a new executable contract language for spatiotemporal knowledge graph engineering, providing a typed runtime with role-based write effects, safety properties verified in Lean 4, and trace parity across large datasets.
OpenAI使用内部模型Astra解决了十个停滞了十多年的数学问题，每个问题花费不到2000美元，并发布了Lean 4形式化证明及一篇论文。这些结果引发了对AI在数学中作用的反思。
本文揭示了图神经网络top-k解释中的一个根本问题：输入图中的自同构导致解释不唯一，因为模型无法区分对称元素。作者提出了一个检测这种任意性的标准，并利用Lean 4中的自动推理对其进行了验证，表明该问题在分子数据集中广泛存在。
一种基于 Google Zanzibar 的 datalog 语言开发的 Lean4 DSL，用于表示和评估知识库，可在 git 下管理，无需重型外部依赖。
一个在 Lean 4 中实现的形式化验证的3D网格交集算法，只需审查93行规范，信任 Lean 检查器而非1000多行AI生成的代码。它展示了一种减少人工审查工作同时确保正确性的新颖方法。
本文介绍了为ARCH HDL（一种面向AI模型生成的硬件描述语言）设计并端到端形式化验证IEEE-754 binary32和bfloat16算术。这些算子通过结合穷举SMT等价性检查和Lean 4证明的混合方法，被证明具有正确的舍入，并输出可综合的SystemVerilog。
本文介绍了Demonstrandum，一个验证优先的多智能体AI数学流水线，能够生成机械可验证的制品，包括通过Lean 4内核验证的反例和猜想证明。
OpenProver 是一个开源系统，利用 Lean 4 进行 LLM 驱动的自动定理证明，采用规划器-工作器-验证器架构，并支持自主和交互两种模式。它实现了数学证明搜索中的可重复评估和人机协同。
本文报告了一个验证流水线的经验，该流水线使用AI证明器（Aristotle和Aleph）结合符号提取工具和形式化密码学库，为Lean 4中的Rust密码学代码生成机器检查的正确性证明，并提供了来自以太坊基金会zkEVM项目的案例研究。
介绍 Leanstral 1.5，一个119B参数（6B活跃）的开放模型，用于Lean 4的形式化证明工程，在miniF2F上达到100%，在PutnamBench和FATE基准测试上达到最先进分数，并发现了开源仓库中先前未知的漏洞。
自动化定理证明正从像 Lean 4 这样的小众工具演变为借助机器学习来帮助解决实际数学问题的系统，例如验证一个对 Erdős 猜想的反例。