vincentoh/erdos741ii-lean4-opus-traces

Erdős #741(ii) — Lean 4 Opus Agent Traces

39 Claude Opus agent sessions attempting Erdős problem #741(ii) in Lean 4 (G1 rung: build the proof from an NL construction description).

v2 (2026-06-10) — label correction. The original upload labeled all 39 traces reward=1.0; the labeler matched the text SCORE=1.0 anywhere in the conversation, including the worker prompt. Rewards are now anchored to genuine oracle output (line-anchored SCORE= adjacent to SORRY_COUNT:/BUILD_EXIT:/STATUS: inside a tool result), with reward = 1.0 iff the session's last oracle score is 1.0. Corrected: 31 of 39 proved; of the other 8, 6 never ran the oracle (session cap / API errors) and 2 ran it but never reached 1.0. Chat structure normalized (strict role alternation, empty <thinking> removed).

Task

Prove that there exists a set of integers that is both an additive basis (every n≥4 is a sum of two elements) and unsplittable (every partition has a non-syndetic half). Construction: tower on powers of 5.

Traces

Each row is one complete agent session:

• —messages: list of {role, content} turns (user prompt + tool calls + oracle feedback + fixes)
• —reward: 1.0 = session's final genuine oracle run scored 1.0 (Lean compiled, 0 sorry), else 0.0 — 31/39
• —n_oracle_runs, last_oracle_score, ever_scored_1: oracle audit fields
• —model: claude-opus-4-8
• —n_turns, n_tool_calls: session stats
• —Tool calls inlined as <tool_call> / <tool_result> markers
• —Thinking blocks preserved as <thinking>

Signal

Hard verifiable reward — Lean compiler accepts or rejects, no fuzzy grading. Traces show the edit→compile→diagnose→fix loop that amortizes formal-language friction.

Usage

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