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… See the full description on the dataset page: https://huggingface.co/datasets/vincentoh/erdos741ii-lean4-opus-traces.