标签
ATS 是一种静态类型编程语言，它将实现与形式化规范统一起来，支持函数式、命令式、并发和模块化编程，并利用依赖类型和线性类型实现高效和安全。
Gilad Bracha 设想了一个未来，软件工程师使用AI将非正式需求转化为形式化规范并加以审查，而AI则实现代码并用定理证明器验证其是否符合规范。人类负责确保形式化规范正确，他们仅需编写自然语言。
LEAP是一种代理框架，使通用LLMs能够在Lean中实现形式定理证明的最新性能，解决了2025年普特南竞赛的全部12个问题，并在新基准（Lean-IMO-Bench）上将形式化证明率从低于10%提升至70%，超越了专门系统。
提出反馈蒸馏（Feedback Distillation），一种利用来自LLM的token级监督来改进复杂推理的训练方法，在Lean 4定理证明上进行了评估。该方法比GRPO更好地保持了多样性，且两种方法互补。
陶哲轩评论 AI 使得大规模生产数学成为可能，将证明写作转化为可搜索的问题：从目标生成数千个迷你引理，然后用廉价检查器过滤掉大部分，只保留少数有效的。
Galois 宣布，SAW 现在支持从 Cryptol 规范生成 Isabelle 理论，将 Cryptol 和 SAW 的易用性与 Isabelle 等交互式定理证明器的表达能力相结合，从而实现对加密协议的半自动化验证。
分享在Yang Zhang实验室组会上的AI loop经验，包括自动化定理证明、多机器协作、蒸馏私人经验库等，并提及Fields奖得主使用AI解决数学难题的例子。
研究人员引入了自导自对弈（Self-Guided Self-Play, SGS），这是一种用于LLM的自我对弈算法，通过使用指引角色（Guide）对合成问题进行评分来防止奖励作弊（reward hacking）。应用于Lean4中的定理证明时，SGS超越了强化学习基线，并使7B模型胜过671B模型。
Aleph，一个全自主的AI智能体系统，用于形式验证，在包括PutnamBench、VeriSoftBench和Verina在内的主要定理证明基准测试中取得了顶尖性能。
FormalSLT是一个Lean 4库，它形式化证明了有限样本统计学习理论结果（ERM、VC界、Rademacher界、PAC-Bayes等），附带显式假设且零sorry语句，为机器学习理论提供机器可验证的基础。
本文介绍了 AI 协作者数学家（AI Co-Mathematician），这是一个利用代理式 AI 支持数学家进行构思和定理证明等开放式研究任务的工作台。早期测试表明，该系统在困难的问题解决基准测试中取得了最先进的结果，包括在 FrontierMath Tier 4 中获得了 48% 的得分。
# Bolzano：LLM辅助数学研究的案例研究 来源：[https://arxiv.org/html/2604.16989](https://arxiv.org/html/2604.16989) Jan Grebík1、Pavel Hubáček1,2、Martin Koutecký1、Matěj Kripner3、Václav Rozhoň1、Robert Šámal1、Adrián Zámečník1 1 布拉格查理大学计算机科学研究所 2 捷克科学院数学研究所 3 布拉格查理大学形式与应用语言学研究所 ###### 摘要 我们报告了在数学与理论计算机科学领域六个问题上取得的新成果……
Verus 是一款针对 Rust 的静态验证工具，利用 SMT 求解在不引入运行时检查的前提下，证明底层系统代码的完整功能正确性。
本论文提出了DeepInsightTheorem，一个分层数据集和渐进式多阶段有监督微调训练策略，通过教导大语言模型识别和应用核心技术来改进其非形式化定理证明能力。
Google DeepMind 的高级 Gemini 配合 Deep Think 在 2025 年国际数学奥林匹克竞赛中达到金牌标准，在竞赛时间限制内以自然语言端到端操作，解答了 6 道题目中的 5 道，获得 35 分——相比去年的银牌成绩取得了重大进步。
# 解决（部分）形式化数学奥林匹克问题 来源：[https://openai.com/index/formal-math/](https://openai.com/index/formal-math/) 我们在 [miniF2F](https://arxiv.org/abs/2109.00110) 基准测试上实现了新的最先进成果（41.2% vs 29.3%），这是一个具有挑战性的高中奥林匹克问题集合。我们的方法称为*语句课程学习*，包括手动收集一组难度级别不同的陈述（不含证明）
OpenAI 推出 GamePad，一个用于在 Coq 证明助手中应用机器学习进行定理证明的学习环境，可实现证明综合以及为策略预测和位置评估任务训练基准模型。