Papers.Data.Code
Dataset

openai/math as Harbor environments

FineEnvs

Contains 369 Harbor tasks for proving openai/math Lean 4 theorems in a sandbox, where agents replace sorrys with complete proofs.

Hugging Face ↗Oct 8, 2026Code ↗

  • rl
  • theorem-proving
  • lean4
  • rl-environment
cover
cover

What it is

369 Harbor theorem-proving environments ported from openai/math, each with a verified Lean 4 statement and strict binary proof checker. 369 validated Harbor environments from 405 openai/math Lean statements, spanning 214 result families and 17 fields, with Lean 4 + Mathlib sandboxes, exact-statement grading, and verified official proofs as hidden oracles.

Key results

  • 369 validated environments from 405 formalized results
  • 214 result families across 17 mathematical fields
  • Apache-2.0 packaging; Lean statements copied from openai/math

Useful for benchmarking RL or code agents on strict, end-to-end verified Lean theorem proving.

One useful ML email a week.

More from Oct 12 – Oct 18

The whole week →

Picked Oct 16

Picked Oct 15

  • Repo
    ziplab/ATAS

    Adds explicit scene and event memory with validated world updates, targeting spatial revisit and event recapture beyond standard multi-shot generation.

    GitHubOct 12, 2026
    →
  • Dataset
    HelenPeng/ExeWorldBench

    Targets executable Blender world construction, scoring functional correctness instead of visual similarity alone.

    Hugging FaceOct 9, 2026
    →

Picked Oct 14

  • Dataset
    ScaleAI/HSS

    Makes intuitive visual reasoning measurable with criterion-level grading; humans hit 93.1% vs 53.6% for the best tested model.

    Hugging FaceOct 1, 2026
    →

Worth your time, not all of your time.

We track new ML work across papers, code, and data, then keep only the pieces worth a closer look. Selected, not collected.

Papers.Data.Code

The Weekly ML Signal

Selected, not collected.

One useful ML email a week: the papers, repos and datasets worth your attention.

Worth your time, not all of your time.