proof-assistant

与 Lean 和 Z3 的创造者 Leonardo de Moura 的访谈节目，讨论 Lean 的工作原理、LLM 在形式化验证中的作用，以及 AI 辅助证明如何改变软件开发和数学。

The Incredible Proof Machine 是一款可视化工具，通过拖拽并连接模块来在各种逻辑中进行证明。它旨在让定理证明变得既易于理解又有趣，无需传统证明工具的语法。

一份使用Lean证明助手进行形式验证的教程，具体验证一次性密码本协议。面向刚接触形式验证的密码学工程师。

在Lean 4中对组合博弈论的形式化，涵盖游戏、nimbers和超现实数，基于Conway的工作。

马特·帕克的视频探讨了近期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，并分析了实际再形式化任务中的流水线设计选择。

一篇详细的博客文章，展示了在Agda中经过全面注释的算术基本定理证明，面向证明助手的中级学习者。

本文应用VGPT-RSI人工智能系统生成与黎曼假设相关的形式化验证的部分结果，包括边界证书和有限Lagarias不等式，同时明确识别剩余数学障碍。

hax是一个将Rust代码翻译成F*、Rocq和Lean等正式语言以进行高保障验证的工具。

Google新论文提出LEAP框架，将数学问题拆解为目标树，利用Lean验证器反馈进行学习，使LLM在数学竞赛题上的正确率从10%提升至70%，解决了Putnam 2025全部12题，并在IMO基准上超越专用金牌级系统。

本文描述了Lean 4中一个形式化验证的金融数学库，包含200多个定理，涵盖从测度论基础到衍生品定价的内容，并包含一个保真度审计，根据Lean语句与所声称数学之间的关系对结果进行分类。