ReuF2F in cmu-l3/reuf2f is a benchmark that evaluates coding agents by formalizing, in Lean, conjectures and explicitly open problems found in papers and reports from undergraduate research programs. The repository contains 244 such problems. No separate version or release information was given.
The model produces a patch that either proves a theorem or proves its complete negation, based on the Lean file containing the open problem. Because answers are graded by checking the formalized proof, evaluation is based on whether the problem is proven rather than on similarity to a natural-language answer. The execution harness uses Docker, a pinned elan toolchain, and Python 3.11 or later. Results are cached per run_id, model name, and instance_id; re-running with the same run_id reuses the stored report.
Because the evaluation executes untrusted Lean code, there is a warning to use an ephemeral host without credentials. The shared image requires roughly 15 GB, and the runtime environment needs at least 60 GB of free space; since the image is for linux/amd64, it runs under emulation on M-series Macs. The license is listed as NOASSERTION, and the repository itself presents no performance comparison results, so differences in agent performance are difficult to judge from this material alone.