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.
Conversations for this repository live on Hugging Face.
CoolFace shows imported repositories read-only. Posting into someone else’s repository from here would need an authorised integration and the account holder’s consent, so the link goes to the source instead.
Open discussions on Hugging Face