Datasetpublic

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.

sourceHugging Faceapache-2.0updated 4mo agoView on Hugging Face

1likes21downloads

settings

This repository belongs to vincentoh on Hugging Face.

CoolFace never edits a repository it does not host. Visibility, licence, collaborators and gating are all managed at the source.

nameerdos741ii-lean4-opus-traces

visibilitypublic

licenceapache-2.0

gatedno

ownervincentoh

Account settings