erdos741ii-lean4-opus-traces

该数据集名为“Erdős #741(ii) — Lean 4 Opus Agent Traces”，包含39个由Claude Opus模型生成的智能体会话轨迹，用于在Lean 4定理证明器中解决Erdős问题#741(ii)。这是一个G1级别任务，要求根据自然语言构造描述构建证明，具体目标是证明存在一个整数集，它同时满足加法基性质（每个大于等于4的整数可表示为该集合中两个元素之和）和不可分割性质（该集合的任意划分都有一半是非syndetic的），构造方法基于5的幂的塔。每个数据样本代表一个完整的智能体会话，包含消息列表（如用户提示、工具调用、预言机反馈和修复步骤的交替序列）、奖励标签（1.0表示会话最后一次真实的预言机运行得分为1.0，即Lean编译成功且无未完成证明占位符sorry，否则为0.0；共有31个轨迹奖励为1.0）、预言机审计字段（如运行次数、最后得分、是否曾得1.0）、模型标识（claude-opus-4-8）和会话统计（如回合数和工具调用数）。工具调用以特定标记内联，思考块被保留。数据集的核心信号是硬验证奖励，完全由Lean编译器接受或拒绝决定，无模糊评分，轨迹清晰地展示了智能体在形式化证明中典型的编辑、编译、诊断和修复的迭代循环过程。该数据集适用于定理证明、形式化方法、强化学习（RL）和智能体行为分析等研究场景，尤其可用于分析智能体如何克服形式化语言障碍并完成复杂数学证明。The dataset is named Erdős #741(ii) — Lean 4 Opus Agent Traces and contains 39 agent session trajectories generated by the Claude Opus model, aimed at solving Erdős problem #741(ii) in the Lean 4 theorem prover. This is a G1-level task that requires constructing proofs based on natural language descriptions, specifically to prove the existence of an integer set that simultaneously satisfies the additive basis property (every integer greater than or equal to 4 can be expressed as the sum of two elements in the set) and the indivisibility property (any partition of the set has a half that is non-syndetic), with a construction method based on towers of powers of 5. Each data sample represents a complete agent session, including a message list (such as alternating sequences of user prompts, tool calls, oracle feedback, and repair steps), a reward label (1.0 indicates that the last real oracle run of the session scored 1.0, meaning Lean compilation succeeded without incomplete proof placeholders sorry, otherwise 0.0; there are 31 trajectories with a reward of 1.0), oracle audit fields (such as run count, final score, and whether it ever scored 1.0), model identifier (claude-opus-4-8), and session statistics (such as turn count and tool call count). Tool calls are inlined with specific markers, and thought blocks are preserved. The core signal of the dataset is hard validation rewards, entirely determined by acceptance or rejection from the Lean compiler, with no ambiguous scoring; the trajectories clearly demonstrate the iterative cycle of editing, compiling, diagnosing, and repairing typical in formal proof processes. This dataset is suitable for research scenarios such as theorem proving, formal methods, reinforcement learning (RL), and agent behavior analysis, particularly for analyzing how agents overcome formal language barriers and complete complex mathematical proofs.

原始信息汇总

数据集概览

该数据集包含 39 条 Claude Opus 智能体会话轨迹，旨在尝试在 Lean 4 中证明 Erdős 问题 #741(ii)（G1 层级：基于自然语言构造描述构建证明）。

任务描述

证明存在一个整数集合，它同时满足：

• 加法基：每个 n ≥ 4 都可以表示为该集合中两个元素的和。
• 不可分割性：对该集合的任意划分，其中一半集合都不是 syndetic 集。
• 构造方法：基于 5 的幂的塔式构造。

数据内容

每条记录代表一个完整的智能体会话，包含以下字段：

• messages：一系列 {role, content} 交互记录（用户提示、工具调用、编译器反馈、修复）。
• reward：1.0 表示会话最终的编译器运行得分为 1.0（Lean 编译通过，0 个未证明目标），否则为 0.0。经修正后，31/39 条轨迹 成功完成证明。
  • 其余 8 条中，6 条从未运行编译器（会话容量限制/API 错误），2 条运行但未达到 1.0。
• n_oracle_runs：编译器运行次数。
• last_oracle_score：最后一次编译器运行得分。
• ever_scored_1：是否曾达到 1.0 分。
• model：claude-opus-4-8。
• n_turns、n_tool_calls：会话统计信息。
• 工具调用内联标记为 <tool_call> / <tool_result>。
• 思考过程保留在 <thinking> 标签中。

奖励信号

使用 硬验证奖励 — Lean 编译器直接接受或拒绝，无模糊评分。轨迹展示了编辑→编译→诊断→修复的循环过程，用于消除形式化语言中的摩擦。

许可证

Apache-2.0

使用示例

python from datasets import load_dataset ds = load_dataset("vincentoh/erdos741ii-lean4-opus-traces", split="train") proved = ds.filter(lambda x: x["reward"] == 1.0) # 31 traces

搜集汇总

数据集介绍

构建方式

本数据集源自39次Claude Opus智能体会话，旨在于Lean 4定理证明器中证明Erdős问题#741(ii)——即构建一个同时为加法基且不可分割的整数集合。数据构建遵循G1阶梯范式：智能体基于自然语言构造性描述生成形式化证明。每条记录为一个完整会话，包含消息序列（角色与内容交替）、奖励标签（基于最终甲骨文评分）、甲骨文审计字段（运行次数、最终评分、是否曾达满分）、模型标识（claude-opus-4-8）以及会话统计（轮次、工具调用次数）。工具调用与思维过程分别以<tool_call>/<tool_result>和<thinking>标记内联记录。数据经v2修正，奖励锚定于工具结果中行级甲骨文输出，确保31条被判定为证明成功。

特点

该数据集最突出的特性在于其硬性可验证奖励机制——Lean编译器直接接受或拒绝证明，杜绝模糊评分，为强化学习提供明确反馈信号。数据真实捕捉了形式化验证中迭代编码、编译、诊断、修复的完整循环，弥合自然语言与形式化语言之间的摩擦。所有会话均采用严格角色交替结构，移除了空<thinking>块，保证了数据质量。会话长度的多样性（工具调用次数、轮次差异）反映了不同证明路径的复杂度。39条轨迹中31条最终获得满分，展现了在复杂数学构造下智能体与验证环境交互的真实动态。

使用方法

数据集可通过HuggingFace Datasets库便捷加载：调用`load_dataset("vincentoh/erdos741ii-lean4-opus-traces", split="train")`获取完整数据。研究者可利用`filter`方法按奖励筛选，例如`ds.filter(lambda x: x["reward"] == 1.0)`获取31条证明成功轨迹。每条轨迹的messages字段包含完整的提示词、工具调用与甲骨文反馈序列，可用于监督学习、模仿学习或强化学习中的奖励建模。甲骨文审计字段（n_oracle_runs、last_oracle_score等）支持细粒度分析会话进展与失败模式。数据采用Apache-2.0许可，适合学术研究与模型开发。

背景与挑战

背景概述

该数据集名为“erdos741ii-lean4-opus-traces”，由研究团队于2026年6月10日更新创建，聚焦于利用大语言模型（如Claude Opus）在形式化证明系统Lean 4中解决数学问题。核心研究问题在于探索AI代理如何通过自然语言描述构造形式化证明，具体针对Erdős #741(ii)问题——证明存在一个整数集合同时具备加法基性质与不可分割性。该数据集记录了39次完整代理会话，涵盖从编辑、编译到诊断和修复的闭环过程，为强化学习与形式化方法交叉领域提供了宝贵资源。其对相关领域的影响力体现在，通过硬可验证奖励机制（Lean编译器接受或拒绝）衡量模型表现，避免了模糊评分，推动了AI在数学定理证明中的自动化进程。

当前挑战

数据集相关挑战主要包括两个方面。在领域问题层面，其核心挑战在于将自然语言描述的数学构造（如基于5的幂的塔式构造）转化为严格的Lean 4形式化证明，这要求模型具备高精度逻辑推理与形式化语言理解能力，以应对整数集合双重性质的复杂性。在构建过程中，挑战表现为数据标注的准确性修复（如最初奖励标注错误，需根据行锚定的真实Oracle输出校正）、会话结构规范化（严格角色交替、移除空思考块）以及处理不完整会话（如因API错误或会话上限导致的6次未运行Oracle），最终确保31个成功证明的可靠性，同时容纳8个未完全成功的案例以供分析失败模式。

常用场景

经典使用场景

在定理证明与形式化验证领域，该数据集为研究大语言模型在交互式定理证明器Lean 4中的自主推理能力提供了珍贵的素材。具体而言，它记录了Claude Opus模型在解决Erdős #741(ii)组合数论难题时的完整轨迹，涵盖了从自然语言构造描述出发、逐步构建形式化证明的完整流程。研究者可借此分析语言模型如何在循环编辑、编译、诊断与修复的反馈迭代中，逐步逼近无懈可击的数学证明。

实际应用

在实际应用层面，该数据集可直接服务于自动化形式化数学助理系统的开发与评估。开发者可利用其中31条成功轨迹训练智能体，使其学习如何在Lean 4环境中高效执行证明搜索与修复操作。此外，该数据集的硬验证奖励信号（Lean编译器的接受或拒绝）天然适用于强化学习微调，可用于构建能够自主推理并生成形式化证明的数学辅助工具，显著降低人类数学家在大规模形式化项目中的工作负担。

衍生相关工作

该数据集衍生出的经典工作包括但不限于：基于它的奖励信号进行监督微调与强化学习对齐的模型训练基准，用于评估不同语言模型在形式化证明任务上的能力；针对证明轨迹的结构化分析工作，如建模编辑-编译-诊断-修复循环的决策模式，提炼高效证明策略；以及利用其失败案例（8条未证明轨迹）开展失败模式分析，识别语言模型在形式化推理中的典型瓶颈，进而推动更鲁棒的交互式证明框架设计。