★ 3
ReuF2F：244 道本科科研开放题 Lean 4 基准发布
研究者推出 ReuF2F，收录 244 道来自本科生科研项目（REU）的 Lean 4 形式化开放问题，用于端到端评测编码智能体的开放问题求解能力。基于 mini-SWE-agent 构建 Leanimum-agent 统一评测框架，结果显示最强模型仅解出约 40% 的题目。
arXiv cs.AI12 天前
#形式化数学
共 4 篇相关资讯，按重要度与时间排序，每 3 小时更新。
★ 3
陶哲轩撰文谈 Lean 定理证明器的可靠性与 AI
数学家陶哲轩在其博客发文，向数学界介绍 Lean 定理证明器，重点讨论其可靠性问题以及与 AI 的结合。文章探讨了形式化证明工具在数学研究中的价值，以及 AI 辅助证明带来的可信度挑战。
Hacker News – AI23 天前
★ 3
研究：让大模型发现有趣数学定理
论文提出以「证明长度与命题长度之比」定义定理的内在趣味性，并证明其与下游实用性高度相关。作者训练了一个 27B 模型来预测给定前提下的证明难度，其准确度超过前沿通用模型。优化该指标后，模型生成的定理与 Mathlib 的重叠率从 91.9% 降至 30.6%，展示了构建自扩展、机器可验证数学库的路…
arXiv cs.LG38 天前
★ 2
Lean Pool：AI维护的形式化数学档案库
Lean Pool是一个形式化数学仓库，由AI智能体负责其增长、维护与优化。该工作展示了AI智能体在形式化数学知识库长期自主运营上的应用方向。
arXiv cs.AI40 天前